Real-Time Specifications

Alexandre David (1) , Kim Guldstrand Larsen (1) , Axel Legay (2) , Ulrik Nyman (1) , Louis-Marie Traonouez (2) , Andrzej Wasowski (3)

1 AAU - Aalborg University [Denmark]
2 ESTASYS - Efficient STAtistical methods in SYstems of systems
3 ITU - IT University of Copenhagen

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -- all indispensable ingredients of a compositional design methodology.The theory is implemented in the new tool Ecdar. We present symbolic versions of the algorithms used in Ecdar, and demonstrate the use of the tool using a small case study in compositional verification.

Mots clés: Real-time systems; Stepwise-Refinement; Compositional Verification; Timed I/O Automata

Domaines: Théorie et langage formel [cs.FL]

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, et al.. Real-Time Specifications. International Journal on Software Tools for Technology Transfer, 2015, 17 (1), pp.29. ⟨10.1007/s10009-013-0286-x⟩. ⟨hal-01087799⟩