Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.


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 (Copyright agreement prohibits open access to the full-text) - Accepted Version
Publisher-imposed embargo
(144Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/11576280_6
Record Created:17 Nov 2009 12:35
Last Modified:09 Oct 2014 10:43

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