Dong, J. S. and Hao, P. and Qin, S. and 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. Berlin: Springer , pp. 66-80. Lecture notes in computer science. (3785).
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.
|Item Type:||Book chapter|
|Keywords:||Timed patterns, Semantics, Tool and verification.|
|Full text:||(AM) Accepted Manuscript|
Download PDF (144Kb)
|Publisher Web site:||http://dx.doi.org/10.1007/11576280_6|
|Publisher statement:||The final publication is available at Springer via http://dx.doi.org/10.1007/11576280_6|
|Record Created:||17 Nov 2009 12:35|
|Last Modified:||31 Mar 2015 12:52|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|