Formal Verification of a Consensus Algorithm in the Heard-Of Model

Abstract : Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.
Type de document :
Article dans une revue
International Journal of Software and Informatics (IJSI), ISCAS, 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303. 〈http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=273&flag=1〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00426388
Contributeur : Stephan Merz <>
Soumis le : lundi 26 octobre 2009 - 08:52:46
Dernière modification le : jeudi 12 avril 2018 - 01:46:36

Identifiants

  • HAL Id : inria-00426388, version 1

Collections

Citation

Bernadette Charron-Bost, Stephan Merz. Formal Verification of a Consensus Algorithm in the Heard-Of Model. International Journal of Software and Informatics (IJSI), ISCAS, 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303. 〈http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=273&flag=1〉. 〈inria-00426388〉

Partager

Métriques

Consultations de la notice

201