We present a simple but elegant prototyping language for describing real-time systems including specific features as timeouts, ex- plicit locations, timed migration and timed communication. The parallel execution of a step is provided by multiset labelled transitions. In order to illustrate its features, we describe a railway control system. Moreover, we define some behavioural equivalences matching multisets of actions that could happen in a given range of time (up to a timeout). We define the strong time-bounded bisimulation and the strong open time-bounded bisimulation, and prove that the latter one is a congruence. By using var- ious bisimulations over the behaviours of real-time systems, we can check which behaviours are closer to an optimal and safe behaviour.
['Bogdan Aman', 'Gabriel Ciobanu']
Timed Mobility and Timed Communication for Critical Systems