
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 ComputerAided Verification, CAV '93. Edited by Costas Courcoubetis. SpringerVerlag, 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
singlesource 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 mechanicallychecked 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 faulttolerance algorithms should be considered
routine.
BibT_{E}X Entry
@inproceedings{cav93hybrid,
AUTHOR = {Patrick Lincoln and John Rushby},
TITLE = {The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model},
BOOKTITLE = {ComputerAided Verification, {CAV} '93},
YEAR = {1993},
EDITOR = {Costas Courcoubetis},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {697},
PAGES = {292304},
ADDRESS = {Elounda, Greece},
MONTH = {June/July},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/cav93hybrid/}
}
Files

