Communicating systems, distributed systems, real-time systems, model-checking, communicating finite state machines, timed automata.
Process control is one of the most critical tasks realized by embedded software. The synchronous programming paradigm has successfully allowed the rigorous development of complex and large process control software. It relies on the proof that the synchronous abstraction is, indeed, safe with respect to real-time constraints, e.g., periodic or aperiodic sollicitations.
Modern complex systems are no more synchronous, but "Globally Asynchronous Locally Synchronous (GALS)". Typically, an embedded system is made of tens or hundreds of interconnected subsystems. Each computing unit can be viewed as synchronous component but the whole system is asynchronous.
Timed automata [1] are widely used to model real-time systems and for model-checking real-time specifications. Timed automata are a perfect fit for verifying a synchronous component. However, they lack the features needed to model and verify asynchronous networks of synchronous systems.
In the untimed world, asynchronous systems have been well studied. It is for instance well-known that communicating finite state machines [2] are Turing powerful. However, decidability may be recovered by considering unreliable communication channels [3, 4], or restrictions on the communication architecture [5].
Several modeling formalisms for real-time systems with asynchronous features (communication or disribution) have already been introduced: time(d) Petri nets [6, 7], timed automata with unbounded FIFO channels [8, 9], etc. The combination of time and unbounded channels yields undecidability even for simple communication architectures [8]. However, this result relies on a synchronous notion of time: all processes share the same global clock. It is more likely that the components in GALS are slightly desynchronized (see, e.g., [10]). The goal here is to define and study models with both communication and time asynchronous features: