Progress-preserving Refinements of CTA

Bartoletti, Massimo and Bocchi, Laura and Murgia, Massimo (2018) Progress-preserving Refinements of CTA. In: Leibniz International Proceedings in Informatics. LIPIcs–Leibniz International Proceedings in Informatics. LIPICS ISBN 978-3-95977-087-3. (doi: (Full text available)


We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints—in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.

Item Type: Conference or workshop item (Paper)
Projects: Projects 1351 not found.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Laura Bocchi
Date Deposited: 03 Jul 2018 10:59 UTC
Last Modified: 11 Jan 2019 14:47 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bocchi, Laura:
  • Depositors only (login required):


Downloads per month over past year