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
01.01.1992
544892 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
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 Spaceborne Computer
NTIS | 1984
|Fault-tolerant computer system
NTRS | 1979
|