Oxford logo
[CKW12] C. Chilton, M. Kwiatkowska and X. Wang. Revisiting Timed Specification Theories: A Linear-Time Perspective. In M. Jurdzinski and D. Nickovic (editors), Proc. 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'12), volume 7595 of LNCS, pages 75-90, Springer. September 2012. [pdf] [bib]
Downloads:  pdf pdf (289 KB)  bib bib
Notes: A full version of this paper, with proofs, can be found in [CKW12b]. The original publication is available at link.springer.com.
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.