SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model
 by Dr. Patrick Lincoln & Dr. John Rushby.

Lecture Notes in Computer Science, Volume 697.
From Computer-Aided Verification, CAV '93.
Edited by Costas Courcoubetis.
Springer-Verlag, Elounda, Greece.
June/July, 1993.
Pages 292–304.


Abstract

Modern verification systems such as PVS are now reaching the stage of development where the formal verification of critical algorithms is feasible with reasonable effort. This paper describes one such verification in the field of fault tolerance. The distribution of single-source data to replicated computing channels (Interactive Consistency or Byzantine Agreement) is a central problem in this field. The classic Oral Messages (OM) algorithm solves this problem under the assumption that all channels are either nonfaulty or arbitrarily (Byzantine) faulty. Thambidurai and Park have introduced a ``hybrid'' fault model that distinguishes additional fault modes, along with a modified version of OM. They gave an informal proof that their algorithm withstands the same number of arbitrary faults, but more ``nonmalicious'' faults than OM.

We detected a flaw in this algorithm while undertaking its formal verification using PVS. The discipline of mechanically-checked formal verification helped us to develop a corrected version of the algorithm. Here we describe the formal specification and verification of this new algorithm. We argue that formal verification systems such as PVS are now sufficiently effective that their application to critical fault-tolerance algorithms should be considered routine.

BibTEX Entry
@inproceedings{cav93-hybrid,
    AUTHOR = {Patrick Lincoln and John Rushby},
    TITLE = {The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model},
    BOOKTITLE = {Computer-Aided Verification, {CAV} '93},
    YEAR = {1993},
    EDITOR = {Costas Courcoubetis},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {697},
    PAGES = {292--304},
    ADDRESS = {Elounda, Greece},
    MONTH = {June/July},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cav93-hybrid/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy