Abstract. We develop a theory of refinement on timed asynchronous systems, in the formal setting of Communicating Timed Automata. In particular, we introduce three notions of refinement for systems of CTAs, which are compositional (i.e., the refinement of a system is obtained by refining its components) and decidable. We establish conditions under which our refinements preserve good behavioural properties of systems, like e.g. their global and local progress. We show that these preservation results still hold when passing from a standard semantics of CTAs to a semantics where receive actions are urgent, as in most common programming primitives. Our theory can be used to refine an abstract model into a concrete one, which can be directly implemented using the real-time primitives available in mainstream programming languages. Our preservation results guarantee that, under some decidable conditions, the properties of the abstract model will still hold in the concrete one.
The technical report with proofs is available here