Publication Type
Journal Article
Version
publishedVersion
Publication Date
6-2008
Abstract
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 composable patterns for high-level system design. Specification languages like Timed Communicating Sequential Process (CSP) and Timed Communicating Object-Z (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 time-enriched process algebras. The patterns facilitate the 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.
Keywords
Timed Automata, timed patterns, TCOZ, UPPAAL
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
IEEE Transactions on Software Engineering
Volume
34
Issue
6
First Page
844
Last Page
859
ISSN
0098-5589
Identifier
10.1109/TSE.2008.52
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Citation
DONG, Jin Song; HAO, Ping; QIN, Shengchao; SUN, Jun; and YI, Wang.
Timed automata patterns. (2008). IEEE Transactions on Software Engineering. 34, (6), 844-859.
Available at: https://ink.library.smu.edu.sg/sis_research/5046
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/TSE.2008.52
