NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
A formally verified algorithm for interactive consistency under a hybrid fault modelConsistent distribution of single-source data to replicated computing channels is a fundamental problem in fault-tolerant system design. The 'Oral Messages' (OM) algorithm solves this problem of Interactive Consistency (Byzantine Agreement) assuming that all faults are worst-cass. Thambidurai and Park introduced a 'hybrid' fault model that distinguished three fault modes: asymmetric (Byzantine), symmetric, and benign; they also exhibited, along with an informal 'proof of correctness', a modified version of OM. Unfortunately, their algorithm is flawed. The discipline of mechanically checked formal verification eventually enabled us to develop a correct algorithm for Interactive Consistency under the hybrid fault model. This algorithm withstands $a$ asymmetric, $s$ symmetric, and $b$ benign faults simultaneously, using $m+1$ rounds, provided $n is greater than 2a + 2s + b + m$, and $m\geg a$. We present this algorithm, discuss its subtle points, and describe its formal specification and verification in PVS. We argue that formal verification systems such as PVS are now sufficiently effective that their application to fault-tolerance algorithms should be considered routine.
Document ID
19940006716
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Lincoln, Patrick
(SRI International Corp. Menlo Park, CA, United States)
Rushby, John
(SRI International Corp. Menlo Park, CA, United States)
Date Acquired
September 6, 2013
Publication Date
July 1, 1993
Subject Category
Computer Programming And Software
Report/Patent Number
NASA-CR-4527
NAS 1.26:4527
Accession Number
94N11188
Funding Number(s)
CONTRACT_GRANT: NAS1-18969
PROJECT: RTOP 505-64-10-13
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available