Timed Automata Patterns

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.