I am currently a postdoctoral researcher at Université Sorbonne Paris Nord, LIPN (Villetaneuse) in LoVe team, affiliated to the ANR project
I'm working on opacity for parametric timed automata.
I did a Ph.D. in Computer Science
on verification of distributed systems
in Université Côte d'Azur, under the supervision of
Pr. Etienne Lozes
Dr. Cinzia Di Giusto
My main interests are modelling and formal methods.
Download my CV here
Title: Synchronizability for distributed systems
Download my thesis here
A very short explanation: Participation to "Ma thèse en 180 secondes"
Distributed systems are ubiquitous and their implementation is complex and error-prone.
In order to check for errors, they can be modeled as systems of communicating automata,
where each automaton represents the behavior of an element of the system. Verification
problems such as reachability are undecidable in such a model. Indeed, a system of
communicating automata is Turing-equivalent. For that, the use of approximations is
necessary. k-synchronizability is one of these techniques. A system is k-synchronizable if,
for all executions, there is an equivalent execution that can be divided into phases
containing k messages. These phases are called k-exchanges. In this thesis, we analyse
k-synchronizable systems: we show that reachability is decidable and we are interested
in the membership problem, that is: given a system, decide whether it is k-synchronizable.
We study both the case where k is an input of the problem, and the case where we have to
guess a k such that the system is k-synchronizable. We study them according to the type
of communication of the system. Either the system is in mailbox and so each process
has only one buffer to store all received messages, or the system is in peer-to-peer,
and each process has a buffer for each sender. Both problems are decidable when the system
is communicating in mailbox. When the system is communicating in peer-to-peer, the first one
is decidable and the second remains open. Finally, we point out some counter-intuitive cases
of k-synchronizable systems that lead us to propose some variations to the definition of
k-synchronizability. A comparative study of the state-of-art classes of systems and our new
classes concludes our work.