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

Bernadette Charron-Bost and Stephan Merz

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.

© International Journal on Systems and Informatics, 2009

Available as: PDF

Typeset Isabelle proof script: PDF

Reference

@Article{charron:formal,
  author =       {Bernadette Charron-Bost and Stephan Merz},
  title =        {Formal Verification of a {C}onsensus Algorithm in the {H}eard-{O}f Model},
  journal =      {Intl. J. Software and Informatics},
  volume =       3,
  number =       {2-3},
  pages =        {273--304},
  year =         2009,
}