Upcoming paper: Progress-preserving Refinements of CTA

Post date: 08-Jun-2018 08:44:39

Upcoming paper (to be presented at CONCUR 2018)

Progress-preserving Refinements of CTA

Massimo Bartoletti, Laura Bocchi, Maurizio Murgia

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 throughseries of experiments, supported by an open-source tool which implements our verification techniques.