Talk "Derivation of correct by construction distributed algorithms: the Dijsktra-Scholten algorithm"

by Dominique Méry

Wed, 04 March 2026 at 11:58 am in Torino, Italy

Abstract: The Event-B language, with its refinement, provides a framework for developing distributed algorithms that are correct by construction, and this work is part of the modelling and construction of distributed algorithms. The objectives of this work are, on the one hand, to enrich the practical method of designing distributed algorithms based on refinement and to illustrate this method in the case of controlling the termination of distributed algorithms, in particular the Dijkstra-Scholten algorithm and associated algorithms. Beyond the development of the algorithm, we address the localisation of events and the transformation of the local Event-B machine into a distributed algorithm . In particular, we aim for the algorithmic form generally used in the literature (such as G. Tel or L. Lamport) and we enrich the description of the algorithm by giving the required properties of the algorithm. A service is gradually transformed on the one hand into a machine containing local events simulating the algorithm and on the other hand into a machine with a single event simulating the algorithm. The development paradigm of sequential algorithms starting from a contract and refined into a single event is adapted to the service refined into a distributed algorithm that responds by construction to the property of correctness.