Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, Marius Bozga
Planning Based Semantics for Distributed Real-Time Systems (2017)
Planning Based Semantics for Distributed Real-Time Systems (2017)
TR-2017-1.pdf
Keywords: Distributed Real-Time Systems, Timed Automata,Planning, Compositional Verification
Abstract: Design, implementation and verification of distributed real- time systems is acknowledged to be a very hard task. Such systems are prone to different kind of delays, such as execution times of actions or communication delays implied by the distributed platform. The latter, in- creases considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies ensuring global consistency and satisfaction of timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multi-party interactions, and propose a method aiming to overcome the communication delays problem through planning ahead interactions. To be effective in a distributed context, planning an interaction should rely on (as much as possible) local information only, namely the state of the participating components. However, as shown in the paper local informa- tion is not always sufficient for correctly scheduling interactions as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the formal model. In this paper we investigate methods for analyzing such deadlock situations and for computing deadlock-free scheduling strategies when possible.
