Formal Techniques for Synchronized Fault-Tolerant SystemsWe present the formal verification of synchronizing aspects of the Reliable Computing Platform (RCP), a fault-tolerant computing system for digital flight control applications. The RCP uses NMR-style redundancy to mask faults and internal majority voting to purge the effects of transient faults. The system design has been formally specified and verified using the EHDM verification system. Our formalization is based on an extended state machine model incorporating snapshots of local processors clocks.
DiVito, Ben L. (Vigyan Research Associates, Inc. Hampton, VA, United States)
Butler, Ricky W. (NASA Langley Research Center Hampton, VA, United States)
September 7, 2013
January 1, 1992
Aircraft Stability And Control
Meeting: Third IFIP International Working Conference on Dependable Computing for Critical Applications