DocumentCode
1711995
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
fYear
1992
Firstpage
132
Lastpage
137
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Digital Avionics Systems Conference, 1992. Proceedings., IEEE/AIAA 11th
Conference_Location
Seattle, WA
Print_ISBN
0-7803-0820-4
Type
conf
DOI
10.1109/DASC.1992.282170
Filename
282170
Link To Document