Formal Design and Verification of a Reliable Computing Platform for Real-TimeControl (Phase 3 Results)

摘要

In this paper the design and formal verification of the lower levels of theReliable Computing Platform (RCP), a fault-tolerant computing system for digital flight control applications, are presented. The RCP uses NMR-style redundancy to mask faults and internal majority voting to flush the effects of transient faults. Two new layers of the RCP hierarchy are introduced: the Minimal Voting refinement (DAminv) of the Distributed Asynchronous (DA) model and the Local Executive (LE) Model. Both the DAminv model and the LE model are specified formally and have been verified using the Ehdm verification system. All specifications and proofs are available electronically via the Internet using anonymous FTP or World Wide Web (WWW) access.