Fail-stop processors

Abstract

A methodology that facilitates the design of fault-tolerant computing systems is presented. It is based on the notion of a failstop processor. Such a processor automatically halts in response to any internal failure and does so before the effects of that failure become visible. The problem of implementing processors that, with high probability, behave like fail-stop processors is addressed. Axiomatic program verification techniques are described for use in developing provably correct programs for failstop processors. The design of a process control system illustrates the use of our methodology. Categories and Subject Descriptors: C.2.4 [Computer-Communications Networks]: Distributed Systems--network operating systems; C.3 [Special-Purpose and Application-Based Systems]--real-time systems; D.4.5 [Operating Systems]: Reliability--verification; F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs. General Terms: Reliability, Verification. ###...