Thomas Chatain's
habilitation defense

I defended my habilitation on Friday, December 13, 2013 at ENS Cachan.


Concurrency in Real-Time Distributed Systems, from Unfoldings to Implementability


Formal methods offer a way to deal with the complexity of information systems. They are adapted to a variety of domains like design, verification, model-checking, test and supervision. But information systems are also more and more often distributed, first because of the generalization of information networks, but also because inside a single device, like a computer, the numerous components run concurrently. The problem is that concurrency is known to be a major difficulty for the use of formal methods because it causes a combinatorial explosion of the state space of the systems. This difficulty comes sometimes with another one due to time when it plays an important role in the behaviour of the systems, for instance when the execution time is a critical parameter. These two difficulties, concurrency and real-time, have guided my research works. Sometimes I have tackled one of these two aspects separately, but in many of my works, I have dealt with the problems that arise when one studies systems that are both concurrent and real-time.

In my habilitation thesis, I give an overview of my recent research works on dependencies between events in real-time distributed systems and on implementability issues for these systems.


Download the thesis


About LSV