Détails sur le séminaire

Abstract: Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. Therefore, in the context of the formal development and verification of such systems, an in-depth study of these interactions makes sense, especially when it comes to decomposition an substitutability. There are two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. On the other hand, asynchronous communication, which we focus on, splits the transmission into an emission and a reception. This makes the interleaving of other events possible and leads to new behaviours that may or may not be desirable. Furthermore, contrary to synchronous communication, the asynchronous world encompasses multiple models characterised by various communication properties such as message ordering policies.
We consider classic asynchronous message-ordering communication models from the literature as well as a few additional variations. We highlight differences that are sometimes overlooked, especially when it comes to the many FIFO models that ensure some messages are received in the order of their emission. First, we propose an abstract, axiomatic, and homogeneous (properties on distributed executions) formalisation of the communication models and we establish a hierarchy, based on the degree of constraint enforced by the models, that extends existing results to additional models and multicast communication.
Then, we propose a mechanised framework for the compatibility checking of compositions of peers. It relies on the TLA+ specification language along with its model checker TLC and is designed in a highly modular and extensible fashion: the communicating peers, the temporal compatibility properties, and the communication models are specified independently.
In most existing approaches, a communication model consists in a monolithic description of the rules and properties of the communication. In our tool, they can be fine tuned through assembly of individual properties on the communication including whether the communication is point-to-point or multicast, ordering policies, bounds on the number of messages in transit, applicative properties, and so on. Among these properties, we describe a generic specification of multicast communication that encompasses point-to-point and one-to-all communication as special cases.
As for the ordering policies we mainly focus on, we rely on a set of uniform operational specifications based on the concept of message histories. We identify and prove the conditions under which they conform to the axiomatic definitions and thus certify the validity of our tool in those cases and point-to-point communication. In parallel, we extend the hierarchy to the operational models and we also consider concrete implementations (e.g. with counters, queues, or vector clocks). We use refinement to draw a map of point-to-point communication models along two axes of comparison: the strength of the ordering property and the level of abstraction of the specification. It may be used when developing correct-by-construction distributed systems where model decomposition exposes the communication component. The proofs are all mechanised in Event-B (and partially with the TLA+ Proof System).