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 :
Theses
Complete list of metadatas

Cited literature [155 references]  Display  Hide  Download

https://hal.inria.fr/tel-01752149
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Monday, January 18, 2016 - 9:39:33 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Tuesday, April 19, 2016 - 12:40:43 PM

Identifiers

  • HAL Id : tel-01752149, version 2

Citation

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⟩

Share

Metrics

Record views

471

Files downloads

613