Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms

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.
Type de document :
Communication dans un congrès
iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00819256
Contributeur : Manamiary Bruno Andriamiarina <>
Soumis le : mardi 30 avril 2013 - 15:34:08
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24

Identifiants

  • 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. 2013. 〈hal-00819256〉

Partager

Métriques

Consultations de la notice

282