International Journal of Software and Informatics
1673-7288
2009
3
2
273
303
article
Formal Veriﬁcation of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM
Distributed algorithms are subtle and error-prone. Still, very few of them have been formally veri?ed, 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 veri?cation 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 veri?cation of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.
formal veriﬁcation; theorem proving; distributed algorithm; Consensus; fault-tolerance
Bernadette Charron-Bost,Stephan Merz
Bernadette Charron-Bost, Stephan Merz
ijsi/article/abstract/273