Formally Verified Byzantine Agreement in Presence of Link Faults
Ulrich Schmid, Bettina Weiss, and
John Rushby
The 22nd International Conference on Distributed
Computing Systems (ICDCS '02), Vienna, Austria, July 2002.
Abstract
This paper shows that deterministic consensus in synchronous
distributed systems with link faults is possible, despite the
impossibility result of (Gray, 1978). Instead of using randomization,
we overcome this impossibility by moderately restricting the
inconsistency that link faults may cause system-wide. Relying upon a
novel hybrid fault model that provides different classes of faults for
both nodes and links, we provide a formally verified proof that the m
+ 1-round Byzantine agreement algorithm OMH (Lincoln & Rushby, 1993)
requires n < 2f_l^s + f_l^r + f_l^{ra} + 2(f_a + f_s) + f_o + f_m + m
nodes for transparently masking at most f_l^s broadcast and f_l^r
receive link faults (including at most f_l^{ra} arbitrary ones) per
node in each round, in addition to at most f_a, f_s, f_o, f_m
arbitrary, symmetric, omission, and manifest node faults, provided
that m <= f_a + f_o + 1. Our approach to modeling link faults is
justified by a number of theoretical results, which include tight
lower bounds for the required number of nodes and an analysis of the
assumption coverage in systems where links fail independently with
some probability p.
Paper available from IEEE Computer Society:
pdf
BibTeX Entry
@inproceedings{Schmid-etal:icdcs,
AUTHOR = {Ulrich Schmid and Bettina Weiss and John Rushby},
TITLE = {Formally Verified Byzantine Agreement in Presence of Link Faults},
BOOKTITLE = {The 22nd International Conference on Distributed
Computing Systems {(ICDCS '02)}},
ORGANIZATION = ieeecs,
ADDRESS = {Vienna, Austria},
PAGES = {608--616},
YEAR = 2002,
MONTH = jul
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page