Timed Automata Patterns

Dong, J.S.; Hao, P.; Qin, S.; Sun, J.; Wang, Y.

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 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.

Citation

Dong, J., Hao, P., Qin, S., Sun, J., & Wang, Y. (2008). Timed Automata Patterns. IEEE Transactions on Software Engineering, 34(6), 844-859. https://doi.org/10.1109/tse.2008.52

• Journal Article Type: Article
• Publication Date: Nov 1, 2008
• Deposit Date: Nov 23, 2009
• Publicly Available Date: Dec 9, 2009
• Journal: IEEE Transactions on Software Engineering
• Print ISSN: 0098-5589
• Electronic ISSN: 1939-3520
• Publisher: Institute of Electrical and Electronics Engineers
• Peer Reviewed: Peer Reviewed
• Volume: 34
• Issue: 6
• Pages: 844-859
• DOI: https://doi.org/10.1109/tse.2008.52
• Public URL: https://durham-repository.worktribe.com/output/1529604