Proving Distributed Algorithms by Combining Refinement and Local Computations

Dominique Méry 1, * Mohammed Mosbah 2, 3, * Mohammed Tounsi 2
* Auteur correspondant
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LaBRI - Laboratoire Bordelais de Recherche en Informatique
3 ENSEIRB - Ecole Nationale Supérieure d'Electronique, Informatique et Radiocommunications de Bordeaux
Abstract : Abstract: Our approach is directly related to the design of correct-by-construction programs. The main idea relies upon the development of distributed algorithms fol- lowing a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use the refinement for controlling the correctness of the resulting algorithm. It relies on a more fundamental question related to the notion of problem to solve. The methodology can be based on incremental proof-based developments. However, the link between the problem and the first model remains to be expressed and the refine- ment is a real help to justify in a very progressive way the choices of design. We propose in this work a framework combining local computations and refinement to prove the correctness of a large class of distributed algorithms.
Keywords : Distributed algorithm Proof-based pattern Event-B Local computation Distributed algorithm.
Type de document :
Communication dans un congrès
Jens Bendisposto, Michael Leuschel, Markus Roggenbach. AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Sep 2010, Dusseldorf, Germany. 2010
Liste complète des métadonnées
https://hal.inria.fr/inria-00547302
Contributeur : Dominique Méry <>
Soumis le : mercredi 15 décembre 2010 - 22:47:54
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

  • HAL Id : inria-00547302, version 1

Collections

INRIA | LABRI | UNIV-BORDEAUX | LORIA | UNIV-LORRAINE

Citation

Dominique Méry, Mohammed Mosbah, Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. Jens Bendisposto, Michael Leuschel, Markus Roggenbach. AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Sep 2010, Dusseldorf, Germany. 2010. 〈inria-00547302〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

180

Contact


archive-ouverte@inria.fr