Real-Time Specifications

International audienceA 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