Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

National Key Research and Development Program of China (2018AAA0101100); National Natural Science Foundation of China (61822201, U1811463, 62076017); the CCF-Huawei Database System Innovation Research Plan (CCF-HuaweiDBIR2020008B); State Key Laboratory of Software Development Environment (Beihang University) Open Program (SKLSDE-2020ZX-07)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

Bernadette Charron-Bost, Stephan Merz. Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM. International Journal of Software and Informatics, 2009,3(2):273~303

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 05,2009
  • Revised:August 06,2009
  • Adopted:August 10,2009
  • Online: March 28,2022
  • Published: