Specifying and Verifying Ultra-reliability and Fault-tolerance Properties
Richard L. Schwartz, Peter Michael Melliar-Smith · NASA Technical Reports Server (NASA) · 1983
A methodology to rigorously verify ultrareliability and fault tolerance system properties is described. The methodology utilizes a hierarchy of formal mathematical specifications of system design and incremental design proof to prove the system has the desired properties. A small example of the approach is given, and the application of the methodology to the large scale proof of SIFT, a fault tolerant flight control operating system, is discussed.