Design strategy for a formally verified reliable computing platform

Abstract

A high-level design is given for a reliable computing platform for real-time control applications. The design tradeoffs and analysis related to the development of a formally verified reliable computing platform are discussed. The design strategy advocated requires the use of techniques that can be completely characterized mathematically as opposed to more powerful or more flexible algorithms whose performance properties can only by analyzed by simulation and testing. The need for accurate reliability models that can be related to the behavior models is also stressed. Tradeoffs between reliability and voting complexity are explored. In particular, the transient recovery properties of the system are found to be fundamental to both the reliability analysis and the correctness models.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>