Progress-preserving Refinements of CTA

Bartoletti, Massimo and Bocchi, Laura and Murgia, Massimo (2018) Progress-preserving Refinements of CTA. In: 29th International Conference on Concurrency Theory (CONCUR 2018), 4--7 September 2018, Beijing, China, 4--7 September 2018, Beijing, China. (In press) (doi:https://doi.org/10.4230/LIPIcs.CONCUR.2018.40) (Full text available)

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)
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: 06 Aug 2018 15:22 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/67556 (The current URI for this page, for reference purposes)
Bocchi, Laura: https://orcid.org/0000-0002-7177-9395
  • Depositors only (login required):

Downloads

Downloads per month over past year