Timed I/O Automata: It is never too late to complete your timed specification theory

TL;DR

This paper develops a comprehensive, formal specification framework for real-time systems using Timed I/O Automata, enabling stepwise, compositional design with rigorous semantics and practical tool support.

Contribution

It introduces a complete specification theory for timed systems with new operators and semantics, backed by proofs and implemented in the ECDAR tool.

Findings

Framework supports refinement, consistency, composition, and quotient operations.

The theory is proven complete and sound.

Implementation in ECDAR demonstrates practical applicability.

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 backed by rigorous proofs and is being implemented in the open-source tool ECDAR.