Validation of a fault-tolerant clock synchronization system
Ricky W. Butler, Stephen C. Johnson · NASA STI Repository (National Aeronautics and Space Administration) · 1984
A validation method for the synchronization subsystem of a fault tolerant computer system is investigated. The method combines formal design verification with experimental testing. The design proof reduces the correctness of the clock synchronization system to the correctness of a set of axioms which are experimentally validated. Since the reliability requirements are often extreme, requiring the estimation of extremely large quantiles, an asymptotic approach to estimation in the tail of a distribution is employed.