Blending Timed Formal Models with Clock Transition Systems

International audienceIn this paper, we propose a new model for the design of safe communicating real-time systems. This model, called Clock Transition System (CTS), supersedes both Networks of Timed Automata (NTA) and Time Petri Nets (TPN) which are usually used for this purpose. It incorporates the advantages of the structure of Petri nets, while intro- ducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency may be introduced by a separate de- scription of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational se- mantics and provide (syntactic) translations. We demonstrate the actual usefulness of CTS on a case study and discuss the analysis techniques that can be lifted to this more general model. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate the- oretical and practical model to factor out the upcoming developments in the TPNs and the NTA scientific communities