Timed I/O automata

Abstract

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 complete 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 on top of an engine for timed games, Uppaal-tiga, and illustrated with a small case study.