Axiomatic Verification to Enhance Software Reliability

Techniques that facilitate the design of reliable software are described. Two distinct phenomena that can cause execution of a program to deviate from its specifications are considered. The first is the failure of the computing system on which the program is running. When this occurs, the system might not be capable of following the instructions specified by the program. The second phenomenon is that the program is written so that it will not execute consistently with its specifications, even on a failure-free computing system. A methodology is presented for designing programs that can cope with failures in the underlying system. It is based on the notion of a fail-stop processor - a processor with well-defined failure mode operating characteristics. Axiomatic program verification techniques are extended for use in developing provably correct programs for such processors. The problem of meeting response time goals in light of failures is discussed. Lastly, the problem of implementing processors that, with high probability, behave like fail-stop processors is addressed. Programming logics have already been developed to reason about sequential programs, and parallel programs that use shared memory or synchronous message-passing. That work is extended to facilitate reasoning about programs that use asynchronous message-passing. Two benefits accrue from this. The obvious one is that partial correctness proofs can be written for concurrent programs that use such primitives. This allows such programs to be understood as predicate transformers, instead of by contemplating all possible execution interleavings - often an intractible task. The other benefit is that these proof rules and their derivation shed light onto how this interference can be controlled. In particular, disciplines that make asynchronous message-passing primitives simple and safe to use are explored. A partial correctness proof of the two-phase commit protocol illustrates the application of the new techniques. This protocol, widely used in database applications, ensures that a specified action is performed either at all sites in a distributed system, or at no site, despite failures