Cookies

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).

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.

Item Type:Book chapter
Keywords:Timed patterns, Semantics, Tool and verification.
Full text:PDF - Accepted Version (144Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/11576280_6
Publisher statement:The original publication is available at www.springerlink.com
Record Created:17 Nov 2009 12:35
Last Modified:29 Nov 2011 17:05

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