The formal basis for our language is a dynamic version of extended automata.
We focus on systems composed from several components, hereafter called processes, running in parallel and interacting through point-to-point message-passing. The number of processes may change over time: they may be created and destroyed dynamically using specific actions, during the system execution.
Each process is an extended timed automaton. They have unique process identifier (pid) values and local memory consisting of variables (including clocks), control state and a queue of pending messages (received and not yet consumed). As usual, processes move from one control state to another by executing transitions. In a control state, transitions are trigerred by the presence of some message in the input queue and/or some (possibly timed) condition on variables. In addition, transition bodies are sequential programs consisting of elementary actions such as variable assignments, clock settings, message sending, process creation/destruction, etc.
The semantics of the extended automata model is given by the graph of its executions. This graph is obtained by the interleaved execution of processes, that is, one process is executing a transition at a time, while the others are waiting. In other words, we consider process transitions to define atomic, non-interruptive, execution steps.
The semantics of time is as for timed automata: time may progress only in states (i.e, all running processes wait in some state before selecting and executing some transition) and transitions take 0 time to be executed. In order to control the time progress, or equivalently, the waiting time in states, we rely on transition urgencies - explicit deadlines attached to them defining when these transitions must be executed.