Revisiting Timed Specification Theories: A Linear-Time Perspective
Chris Chilton, Marta Kwiatkowska, and Xu Wang
In Marcin Jurdzinski and Dejan Nickovic, editors, Proc. 10th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'12), Lecture Notes in Computer Science, vol. 7595, pp. 75-90. Springer-Verlag, 2012.
Downloads: 
pdf 
bib
Abstract: 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.