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. 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 machines aims at analysing formal models of distributed systems and discovering bugs like message loss or deadlocks. This problem is undecidable in general, even with two machines only, and several restrictions have been considered to restore decidability. One of them is the hale-duplex hypothesis: in a system of two machines, it is always the case that a machines does not send any message if it still has some pending messages to be received in its queue.
The goal of this phD thesis is to define new classes of communicating machines for which model-checking is decidable, among other by extending the notion of half-duplex systems to systems of arbitrary number of machines. Possibly, this would involve to introduce a separation logic for communicating machines that captures these generalised half-duplex properties.
I taught in the second year of the computer science degree. I taught Mechanisms of Operating Systems and C language programming and datastructures.