  We consider the setting of component-based design for real-time systems with
critical timing constraints. Based on our earlier work, we propose a
compositional specification theory for timed automata with I/O distinction,
which supports substitutive refinement. Our theory provides the operations of
parallel composition for composing components at run-time, logical
conjunction/disjunction for independent development, and quotient for
incremental synthesis. The key novelty of our timed theory lies in a weakest
congruence preserving safety as well as bounded liveness properties. We show
that the congruence can be characterised by two linear-time semantics,
timed-traces and timed-strategies, the latter of which is derived from a
game-based interpretation of timed interaction.
