Thomas Chatain (LIAFA, Paris 7LSV, ENS Cachan)

Formal models for real-time distributed systems, like time Petri nets and networks of timed automata have proved their interest for the verification of real-time systems. On the other hand, the question of using these models as specifications for designing real-time systems raises several difficulties. Here we focus on the ones that are related to the distributed nature of the system. Implementing a model may be possible at the cost of some transformations, which make it suitable for the target device. In this talk, I present two transformations which preserve both the timed semantics and the distribution of actions. Their correctness is expressed in terms of adapted behavioral comparisons.

Last modified: Mon Mar 24 15:09:56 CET 2014