I'm currently working as a graduate assistant in Université Paris-Est Créteil. My main research interests are formal verification and communications of distributed protocols. More recently, I started working on transducers. I did a PhD in computer science in Université Côte d'Azur, under the supervision of Étienne Lozes and Cinzia Di Giusto.
Most of the distributed systems we use nowadays are based on the message-passing paradigm where systems are structured into parties that interact only by sending and receiving messages asynchronously. Message-passing programming is largely employed in high performance computing (MPI, OpenMP, etc), event-driven applications built on top of actor-based languages (Scala, Erlang, etc), service-oriented architectures, peer-to-peer applications, etc.
Unfortunately, because of the variety of communication models (peer to peer, mailbox, etc), of the ambiguities of the specifications of the communication primitives, of a limited portability of the code, and of the difficulty of running representative tests, etc, it is error prone and therefore often reserved to experts.
Model-checking of communicating automata aims at analysing formal models of distributed systems and discovering bugs like message loss or deadlocks. Due to the asynchronous nature of the communications, this problem is undecidable in general, even with two machines only, and several restrictions have been considered to restore decidability.
We define a new one in this thesis: systems that are realisable with synchronous communications (RSC for short), that is the systems whose behaviours are equivalent to synchronous ones. We propose the class of RSC systems as a generalisation of half-duplex systems, which are system of two machines, where a machines does not send any message if it still has some pending messages to be received in its queue.
We study another formalism as well: choreographies, which provide a way to reason globally on a system. Choreographies describe synchronous executions, and one of the problems associated with it is checking whether the combination of all participants of the described communication will behave accordingly to the global description. We propose to rely on the properties of RSC systems to study this problem.