Skip to Main content Skip to Navigation

Développement d'algorithmes répartis corrects par construction

Manamiary Bruno Andriamiarina 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : The subject of this thesis is the formal development and verification of distributed algorithms. We are interested in this topic, because proving that a distributed algorithm satisfies given specification and properties is a difficult task. We choose to use the Event B method (refinement, safety properties) and the temporal logic TLA (fairness, liveness properties) for modelling the distributed algorithms. There are several existing approaches for formalising distributed algorithms, and we choose to focus on the "correct-by-construction" paradigm, which is characterised by the use of model refinement, proof of properties (safety, liveness) and reuse of formal models/proofs/properties, developments (~ design patterns) for modelling distributed algorithms. Our works introduce a paradigm which allows us to describe an algorithm with a set of services/functionalities, which are then expressed using liveness properties. These properties guide us in developing the formal Event B models of the studied algorithms. Inference rules from TLA allow to decompose the liveness properties, therefore detailing the services and guiding the refinement process. This paradigm, called "service-as-event" is also characterized by (assertions) diagrams, which allow to graphically represent liveness properties (with respect to fairness hypotheses) and detail the mecanisms and functioning of the studied distributed algorithms. The "service-as-event" paradigm allowed us to develop and verify the following algorithms : routing algorithms, such as Anycast RP (Cisco Systems), XY for Networks-on-Chip (NoC), snapshot and self-* algorithms.
Document type :
Complete list of metadata

Cited literature [155 references]  Display  Hide  Download
Contributor : Manamiary Bruno Andriamiarina Connect in order to contact the contributor
Submitted on : Monday, January 18, 2016 - 9:39:33 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM
Long-term archiving on: : Tuesday, April 19, 2016 - 12:40:43 PM


  • HAL Id : tel-01752149, version 2


Manamiary Bruno Andriamiarina. Développement d'algorithmes répartis corrects par construction. Modélisation et simulation. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0181⟩. ⟨tel-01752149v2⟩



Les métriques sont temporairement indisponibles