Skip to main content

Research Repository

Advanced Search

The Semantics and Tool Support of OZTA

Dong, J.S.; Hao, P.; Qin, S.; Zhang, X.

The Semantics and Tool Support of OZTA Thumbnail


Authors

J.S. Dong

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





You might also like



Downloadable Citations