Title :
Formal verification of a fault tolerant computer
Author :
Brock, Neil A. ; Jackson, David M.
Author_Institution :
Charles Stark Draper Lab. Inc., Cambridge, MA, USA
Abstract :
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
Keywords :
Occam; aircraft instrumentation; fault tolerant computing; formal verification; parallel architectures; redundancy; transputers; INMOS Transputer; buffer; design verification; fault tolerant computer; formal verification; high-integrity embedded applications; modeling; quadruply redundant processor; Computer architecture; Europe; Failure analysis; Fault tolerance; Fault tolerant systems; Filters; Formal verification; Laboratories; Mathematical model; Mathematics;
Conference_Titel :
Digital Avionics Systems Conference, 1992. Proceedings., IEEE/AIAA 11th
Conference_Location :
Seattle, WA
Print_ISBN :
0-7803-0820-4
DOI :
10.1109/DASC.1992.282170
