Issue No. 06 - November/December (2008 vol. 34)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2008.52
Jin Song Dong , National University of Singapore, Singapore
Ping Hao , National University of Singapore, Singapore
Shengchao Qin , Durham University, Durham
Jun Sun , National University of Singapore, Singapore
Wang Yi , North Eastern University, China, and Uppsala University, Sweden
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.
J. S. Dong, S. Qin, W. Yi, J. Sun and P. Hao, "Timed Automata Patterns," in IEEE Transactions on Software Engineering, vol. 34, no. , pp. 844-859, 2008.