Title :
A provably correct design of a fault-tolerant clock synchronization circuit
Author :
Miner, Paul S. ; Padilla, Peter A. ; Torres, Wilfredo
Author_Institution :
NASA Langley Res. Center, Hampton, VA, USA
Abstract :
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
Keywords :
CAD; aerospace computing; fault tolerant computing; formal specification; redundancy; synchronisation; timing circuits; Byzantine resilient clock synchronization; aerospace; convergence functions; correlated transient failures; fault-tolerant clock synchronization; fly-by-light; fly-by-wire; formal specification; formal theory; four-clock implementation; simulation; synchronisation; transient faults; Algorithm design and analysis; Analytical models; Clocks; Fault tolerance; Fault tolerant systems; Formal specifications; Logic; Performance analysis; Prototypes; Synchronization;
Conference_Titel :
Digital Avionics Systems Conference, 1992. Proceedings., IEEE/AIAA 11th
Conference_Location :
Seattle, WA
Print_ISBN :
0-7803-0820-4
DOI :
10.1109/DASC.1992.282133