|
A Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model
by Dr. John Rushby.
From Thirteenth ACM Symposium on Principles of Distributed Computing. Los Angeles, CA. August, 1994.
Also available as NASA Contractor Report 198289
Abstract
A simple modification to the Interactive Convergence clock synchronization algorithm allows it to
tolerate a larger number of certain kinds of faults than the standard algorithm, without reducing its
tolerance to arbitrary or Byzantine faults. Because the extended case-analysis required by the new
fault model complicates the already intricate argument for correctness of the algorithm, it has been
subjected to mechanically-checked formal verification.
The fault model examined is similar to the ``hybrid'' one previously used for the problem of
Interactive Consistency (Byzantine Agreement): in addition to arbitrary faults, we also admit
manifest (i.e., detectable) and symmetric (i.e., consistent) faults. With n channels, the modified
algorithm can withstand a arbitrary, s symmetric, and m manifest faults simultaneously, provided n >
3a + 2s + m. This is better than the bound achieved for the problem of interactive consistency under
the similar fault model. Unlike interactive consistency, we have been able to further extend the fault
model for clock synchronization to include link faults with bound n > 3a + 2s + m + l where l is the
maximum, over all pairs of channels, of the number of channels that have faulty links to one or other
of the pair.
The mechanically-checked formal verification of the modified algorithm was achieved by extending
one for the classical Interactive Convergence algorithm, and was accomplished in just a few days of
work. A mechanically-checked formal specification and verification is a reusable intellectual
resource whose initial cost is amply repaid by the support it provides for inexpensive and reliable
investigation of modified assumptions and algorithms such as those reported here.
BibTEX Entry
@inproceedings{Rushby94:icah,
AUTHOR = {John Rushby},
TITLE = {{A} Formally Verified Algorithm for Clock Synchronization Under a Hybrid Fault Model},
BOOKTITLE = {Thirteenth {ACM} Symposium on Principles of Distributed Computing},
YEAR = {1994},
ADDRESS = {Los Angeles, {CA}},
MONTH = {August},
NOTE = {Also available as {NASA} Contractor Report 198289},
URL = {http://www.csl.sri.com/papers/podc94/}
}
Files
|
|