A prototype fault-tolerant clock synchronization system is designed to a proven correct formal specification. The specification is derived from F.B. Schneider's (1987) general paradigm for Byzantine resilient clock synchronization. One addition to the formal theory is a mechanism for proven recovery from a bounded, number of transient faults. A description of a four-clock implementation which satisfies the requirements of the formal theory is presented. In addition, the design provides options for initialization which permit recovery from some correlated transient failures. Extra logic is included to provide experimental control of these options. Simulation results are presented Scenarios studied include achieving initial synchronization between clocks, resynchronization of a lost clock, and general behavior during upset or in the presence of a faulty clock. The simulation estimates of the times required from power-on to achievement of initial synchronization and to resynchronize a lost clock corroborate the initial analysis of the algorithms and meet the performance criteria and constraints of the theory.<>
A provably correct design of a fault-tolerant clock synchronization circuit
1992-01-01
547294 byte
Conference paper
Electronic Resource
English
A Provably Correct Design of a Fault-Tolerant Clock Synchronization Circuit
British Library Conference Proceedings | 1992
|Fault-Tolerant Clock Synchronization for Safety-Critical Applications
British Library Conference Proceedings | 2004
|