A.: Timed I/O Automata: A Complete Specification Theory for Real-time Systems

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 for-malism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refine-ment, consistency checking, logical and structural composi-tion, and quotient of specifications – all indispensable ingre-dients 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