Abstract. We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata. Our notion of refinement is compositional (i.e., the refinement of a system is obtained by refining its components independently) and decidable.We 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 though a series of experiments, supported by an open-source tool which implements our verification techniques.
The technical report with proofs is available here
The tool is available here