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

Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization
 by Dr. Natarajan Shankar.

Lecture Notes in Computer Science, Volume 571.
From Formal Techniques in Real-Time and Fault-Tolerant Systems.
Edited by J. Vytopil.
Springer-Verlag, Nijmegen, The Netherlands.
January, 1992.
Pages 217–236.

Schneider generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. We present a mechanical verification of Schneider's protocol leading to several significant clarifications and revisions. The verification was carried out with the Ehdm system developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm satisfies the requirements of Schneider's protocol. Our mechanical verification raises a number of issues regarding the verification of fault-tolerant, distributed, real-time protocols that are germane to the design of a special-purpose logic for such problems.
BibTEX Entry
    AUTHOR = {Natarajan Shankar},
    TITLE = {Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization},
    BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
    YEAR = {1992},
    EDITOR = {{J.} Vytopil},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {571},
    PAGES = {217--236},
    ADDRESS = {Nijmegen, The Netherlands},
    MONTH = {jan},
    PUBLISHER = {Springer-Verlag},
    URL = {}


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