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)

Additional URL

https://doi.org/10.1109/TSE.2008.52

Download

Share

COinS