Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms

Manamiary Bruno Andriamiarina 1, 2 Dominique Méry 1 Neeraj Kumar Singh 1, 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 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
Abstract : The verification of distributed algorithms is a challenge for formal techniques supported by tools, such as model checkers and proof assistants. The difficulties lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms. In this paper, we present a methodology based on the general concept of refinement that is used for developing distributed algorithms satisfying a given list of safety and liveness properties. The methodology is a recipe for reusing the old ingredients of the classical temporal approaches, which are illustrated through standard example of routing protocols. More precisely, we show how the state-based models can be developed for specific problems and how they can be simply reused by controlling the composition of state-based models through the refinement relationship. The service-as-event paradigm is introduced for helping users to describe algorithms as a composition of simple services and/or to decompose them into simple steps. Consequently, we obtain a framework to derive new distributed algorithms by developing existing distributed algorithms using correct-by-construction approach. The correct-by-construction approach ensures the correctness of developed distributed algorithms.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-00819256
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Tuesday, April 30, 2013 - 3:34:08 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Identifiers

  • HAL Id : hal-00819256, version 1

Collections

Citation

Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. ⟨hal-00819256⟩

Share

Metrics

Record views

328