Skip to main content
Kent Academic Repository

Progress-preserving Refinements of CTA

Bartoletti, Massimo, Bocchi, Laura, Murgia, Massimo (2018) Progress-preserving Refinements of CTA. In: Leibniz International Proceedings in Informatics. LIPIcs–Leibniz International Proceedings in Informatics. Leibniz International Proceedings in Informatics (LIPIcs) . pp. 1-19. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Saarbrücken, Germany ISBN 978-3-95977-087-3. (doi:10.4230/LIPIcs.CONCUR.2018.40) (KAR id:67556)

Abstract

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)
DOI/Identification number: 10.4230/LIPIcs.CONCUR.2018.40
Projects: Time-sensitive protocol design and implementation Project Application
Uncontrolled keywords: protocol implementation, communicating timed automata, message passing
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Engineering and Physical Sciences Research Council (https://ror.org/0439y7842)
Depositing User: Laura Bocchi
Date Deposited: 03 Jul 2018 10:59 UTC
Last Modified: 12 Jul 2022 10:41 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/67556 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.