J.S. Dong
Timed Patterns: TCOZ to Timed Automata
Dong, J.S.; Hao, P.; Qin, S.; Sun, J.; Wang, Y.; Davies, J.; Schulte, W.; Barnett, M.
Authors
P. Hao
S. Qin
J. Sun
Y. Wang
J. Davies
W. Schulte
M. Barnett
Abstract
The integrated logic-based modeling language, Timed Communicating Object Z (TCOZ), is well suited for presenting complete and coherent requirement models for complex real-time systems. However, the challenge is how to verify the TCOZ models with tool support, especially for analyzing timing properties. Specialized graph-based modeling technique, Timed Automata (TA), has powerful mechanisms for designing real-time models using multiple clocks and has well developed automatic tool support. One weakness of TA is the lack of high level composable graphical patterns to support systematic designs for complex systems. The investigation of possible links between TCOZ and TA may benefit both techniques. For TCOZ, TAs tool support can be reused to check timing properties. For TA, a set of composable graphical patterns can be defined based on the semantics of the TCOZ constructs, so that those patterns can be re-used in a generic way. This paper firstly defines the composable TA graphical patterns, and then presents sound transformation rules and a tool for projecting TCOZ specifications into TA. A case study of a railroad crossing system is demonstrated.
Citation
Dong, J., Hao, P., Qin, S., Sun, J., Wang, Y., Davies, J., …Barnett, M. (2004). Timed Patterns: TCOZ to Timed Automata. In Formal methods and software engineering : 6th International Conference on Formal Engineering Methods, ICFEM 2004, 8-12 November 2004, Seattle, WA, USA. ; proceedings (483-498). https://doi.org/10.1007/978-3-540-30482-1_39
Conference Name | Formal Methods and Software Engineering : 6th International Conference on Formal Engineering Methods (ICFEM 2004) |
---|---|
Conference Location | Seattle, USA |
Start Date | Nov 8, 2004 |
End Date | Nov 12, 2004 |
Publication Date | Jan 1, 2004 |
Deposit Date | Nov 20, 2009 |
Publicly Available Date | Dec 10, 2009 |
Pages | 483-498 |
Series Title | Lecture notes in computer science |
Series Number | 3308 |
Series ISSN | 0302-9743,1611-3349 |
Book Title | Formal methods and software engineering : 6th International Conference on Formal Engineering Methods, ICFEM 2004, 8-12 November 2004, Seattle, WA, USA. ; proceedings. |
ISBN | 9783540238416 |
DOI | https://doi.org/10.1007/978-3-540-30482-1_39 |
Keywords | Modeling and specification formalisms. |
Files
Accepted Conference Proceeding
(215 Kb)
PDF
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-30482-1_39
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search