Number SRI-CSL-89-3R.
Computer Science Laboratory, SRI International, Menlo Park, CA.
February, 1989.

We describe a formal specification and mechanically checked verification of the Interactive Convergence Clock Synchronization Algorithm of Lamport and Melliar-Smith. In the course of this work, we discovered several technical flaws in the analysis given by Lamport and Melliar-Smith, even though their presentation is unusually precise and detailed. As far as we know, these flaws (affecting the main theorem and four of its five lemmas) were not detected by the ``social process'' of informal peer scrutiny to which the paper has been subjected since its publication. We discuss the flaws in the published proof and give a revised presentation of the analysis that not only corrects the flaws in the original, but is also more precise and, we believe, easier to follow. This informal presentation was derived directly from our formal specification and verification. Some of our corrections to the flaws in the original require slight modifications to the assumptions underlying the algorithm and to the constraints on its parameters, and thus change the external specification of the algorithm.

The formal analysis of the Interactive Convergence Clock Synchronization Algorithm was performed using the Ehdm formal specification and verification environment. This application of Ehdm provides a demonstration of some of the capabilities of the system.

Note: This second edition of the report presents a revised version of the formal specification and verification that exploits some of the features introduced into Ehdm since the original verification was performed, and also improves the substance of the verification in three respects.

@techreport{csl-89-3r,
    AUTHOR = {John Rushby and Friedrich von Henke},
    TITLE = {Formal Verification of the Interactive Convergence Clock Synchronization Algorithm},
    INSTITUTION = {Computer Science Laboratory, {SRI} International},
    YEAR = {1989},
    NUMBER = {{SRI-CSL-89-3R}},
    ADDRESS = {Menlo Park, {CA}},
    MONTH = {feb},
    NOTE = {Revised August 1991},
    URL = {http://www.csl.sri.com/papers/csl-89-3/}
}

• csl-89-3r.dvi.gz
• csl-89-3r.ps.gz