The design verification of a quadruply redundant processor element for high-integrity embedded applications is described. The system, based on the INMOS Transputer, is modeled formally and mathematically proved to be tolerant to any single fault. This was accomplished by formally specifying the correct behavior of the system, as a buffer, and modeling its correct behavior with a composite of the correct behaviors of each of its components. The complete model is demonstrably a refinement of the specification, i.e., better and more ordered.<>
Formal verification of a fault tolerant computer
1992-01-01
544892 byte
Conference paper
Electronic Resource
English
Formal Verification of a Fault-Tolerant Computer
British Library Conference Proceedings | 1992
|Formal Verification for Fault-Tolerant Architectures/PVS Design
British Library Conference Proceedings | 1995
|Fault-tolerant computer system
NTRS | 1979
|Fault Tolerant Spaceborne Computer
NTIS | 1984
|