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:       | Export: EndNote, Zotero | BibTex |
| Usage statistics | Look up in GoogleScholar | Find in a UK Library |
![[Feed]](/images/RSSwebsmall.jpg)
![[Tweets]](/images/Twitterwebsmall.png)
