Progress-preserving refinements of CTA
Massimo Bartoletti
;BOCCHI, LAURA
;Maurizio Murgia
2018-01-01
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 a ecting 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.File | Size | Format | |
---|---|---|---|
main.pdf Solo gestori archivio
Description: Articolo principale
Type: versione pre-print
Size 678.43 kB
Format Adobe PDF
|
678.43 kB | Adobe PDF | & nbsp; View / Open Request a copy |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.