Dong, J. S. and Hao, P. and Qin, S. and Sun, J. and Wang, Y. (2008) 'Timed automata patterns.', IEEE transactions on software engineering., 34 (6). pp. 844-859.
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.
|Full text:||PDF - Published Version (2171Kb)|
|Publisher Web site:||http://dx.doi.org/10.1109/TSE.2008.52|
|Publisher statement:||©2009 IEEE. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.|
|Record Created:||23 Nov 2009 13:50|
|Last Modified:||02 Dec 2011 16:19|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Usage statistics||Look up in GoogleScholar | Find in a UK Library|