Auditorium (Building IMAG)
31 October 2018 - 14h00
Formal Methods for Distributed Real-Time Systems (Phd Defense)
by Mahieddine DELLABANI from Verimag
Abstract: Nowadays, real-time systems are ubiquitous in several application domains. Such an emergence led to an increasing need of performance (resources, availability, concurrency, etc.) and initiated a shift from the use of single processor based hardware platforms, to large sets of interconnected and distributed computing nodes. This trend introduced the birth of a new family of systems that are intrinsically distributed, namely Networked Embedded Systems. Such an evolution stems from the growing complexity of real-time software embedded on such platforms (e.g. electronic control in avionics and automotive domains), and the need to integrate formerly isolated systems so that they can cooperate, as well as share resources improving thus functionalities and reducing costs. Undoubtedly, the design, implementation and verification of such systems are acknowledged to be very hard tasks since they are prone to different kinds of factors, such as communication delays, CPU(s) speed or even hardware imprecisions, which increases considerably the complexity of coordinating parallel activities. In this thesis, we propose a rigorous design flow intended for building distributed real-time applications.
We investigate timed automata based models, with formally defined semantics, in order to study the behavior of a given system with some imposed timing constraints when deployed in a distributed environment. Particularly, we study (i) the impact of the communication delays by introducing a minimum latency between actions executions and the effective date at which actions executions have been decided, and (ii) the effect of hardware imperfections, more precisely clocks imprecisions, on systems execution by breaking the perfect clocks hypothesis, often adopted during the modeling phase. Nevertheless, timed automata formalism is intended to describe a high level abstraction
of the behavior of a given application. Therefore, we use an intermediate representation of the initial application that, besides having “equivalent†behavior, explicitly expresses implementation mechanisms, and thus reduces the gap between the modeling and the concrete implementation. Additionally, we contribute in building such systems by (iii) proposing a knowledge based optimization method that aims to eliminate unnecessary computation time or exchange of messages during the execution.
We compare the behavior of each proposed model to the initial high level model and study the relationships between both. Then, we identify and formally characterize the potential problems resulting from these additional constraints. Furthermore, we propose execution strategies that allow to preserve some desired properties and reach a “similar†execution scenario, faithful to the original specifications.
