A formally verified algorithm for clock synchronization under a hybrid fault model
John Rushby · 1994
A small modification to the interactive convergence clock synchronization algorithm allows it to tolerate a larger number of simple faults than the standard algorithm, without reducing its ability to tolerate arbitrary or "Byzantine" faults.Because the extended caseanalysis 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 distributed consensus: in addition to arbitrary faults, we also admit symmetr~c (i.e., consistent) and manifest (i.e., detect able) faults.With n processors, the modified algo-"