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:

Timed patterns : TCOZ to timed automata.

Dong, J. S. and Hao, P. and Qin, S. and Sun, J. and Wang, Y. (2004) 'Timed patterns : TCOZ to timed automata.', in Formal methods and software engineering : 6th International Conference on Formal Engineering Methods, ICFEM 2004, 8-12 November 2004, Seattle, WA, USA. ; proceedings. Berlin: Springer , pp. 483-498. Lecture notes in computer science. (3308).

Abstract

The integrated logic-based modeling language, Timed Communicating Object Z (TCOZ), is well suited for presenting complete and coherent requirement models for complex real-time systems. However, the challenge is how to verify the TCOZ models with tool support, especially for analyzing timing properties. Specialized graph-based modeling technique, Timed Automata (TA), has powerful mechanisms for designing real-time models using multiple clocks and has well developed automatic tool support. One weakness of TA is the lack of high level composable graphical patterns to support systematic designs for complex systems. The investigation of possible links between TCOZ and TA may benefit both techniques. For TCOZ, TAs tool support can be reused to check timing properties. For TA, a set of composable graphical patterns can be defined based on the semantics of the TCOZ constructs, so that those patterns can be re-used in a generic way. This paper firstly defines the composable TA graphical patterns, and then presents sound transformation rules and a tool for projecting TCOZ specifications into TA. A case study of a railroad crossing system is demonstrated.

Item Type:Book chapter
Keywords:Modeling and specification formalisms.
Full text:PDF - Accepted Version (210Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/b102837
Publisher statement:The original publication is available at www.springerlink.com
Record Created:20 Nov 2009 16:50
Last Modified:24 Feb 2012 09:55

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