J.S. Dong
The Semantics and Tool Support of OZTA
Dong, J.S.; Hao, P.; Qin, S.; Zhang, X.
Authors
P. Hao
S. Qin
X. Zhang
Abstract
In this work, we firstly enhance OZTA, a combination of Object-Z and Timed Automata, by introducing a set of timed patterns as language constructs that can specify the dynamic and timing features of complex real-time systems in a systematic way. Then we present the formal semantics in Unifying Theories of Programming for the enhanced OZTA. Furthermore, we develop an OZTA tool which can support editing, type-checking of OZTA models as well as projecting OZTA models into TA models so that we can utilize TA model checkers, e.g., Uppaal for verification.
Citation
Dong, J., Hao, P., Qin, S., & Zhang, X. (2005). The Semantics and Tool Support of OZTA. In Formal methods and software engineering : 7th International Conference on Formal Engineering Methods, ICFEM 2005, 1-4 November, 2005, Manchester, UK ; proceedings (66-80). https://doi.org/10.1007/11576280_6
Conference Name | Formal Methods and Software Engineering : 7th International Conference on Formal Engineering Methods (ICFEM 2005) |
---|---|
Conference Location | Manchester, UK |
Start Date | Nov 1, 2005 |
End Date | Nov 4, 2005 |
Publication Date | Nov 1, 2005 |
Deposit Date | Nov 17, 2009 |
Publicly Available Date | Dec 10, 2009 |
Pages | 66-80 |
Series Title | Lecture notes in computer science |
Series Number | 3785 |
Series ISSN | 0302-9743,1611-3349 |
Book Title | Formal methods and software engineering : 7th International Conference on Formal Engineering Methods, ICFEM 2005, 1-4 November, 2005, Manchester, UK ; proceedings. |
ISBN | 9783540297970 |
DOI | https://doi.org/10.1007/11576280_6 |
Keywords | Timed patterns, Semantics, Tool and verification. |
Files
Accepted Conference Proceeding
(147 Kb)
PDF
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/11576280_6
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