We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

The semantics and tool support of OZTA.

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
Publisher Web site:
Publisher statement:The final publication is available at Springer via
Record Created:17 Nov 2009 12:35
Last Modified:31 Mar 2015 12:52

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library