Skip to Main content Skip to Navigation
Conference papers

Refinement-based Construction of Correct Distributed Algorithms

Dominique Méry 1, 2, 3
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants. The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms. Verification by construction can be achieved by using a formal framework in which models are constructed at different levels of abstrac- tion; each level of abstraction is refined by the one below, and this refinement relationships is documented by an abstraction relation namely a gluing invariant. The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to an implementation from which an efficient implementation can be derived automatically. We describe a method- ology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and liveness properties. We will show also how formal models can be used for producing distributed programs of a real programming language. The modelling methodology is defined in the Event-B modelling language using the Rodin Formal IDE.
Complete list of metadata
Contributor : Dominique Méry <>
Submitted on : Thursday, April 15, 2021 - 11:25:14 PM
Last modification on : Tuesday, May 11, 2021 - 3:31:43 PM


  • HAL Id : hal-03199808, version 1



Dominique Méry. Refinement-based Construction of Correct Distributed Algorithms. ICI2ST 2021 - The Second International Conference on Information Systems and Software Technologies, Mar 2021, Quito / Virtual, Ecuador. ⟨hal-03199808⟩



Record views