Proof rules for fault tolerant distributed programs

AbstractProving the properties of a program which must execute on a distributed system whose nodes may fail is a complex task. Such proofs must take into account the effects of hardware failures at all possible points in the execution of individual processes. The difficulty in accomplishing this is compounded by the need to cater also for the simultaneous failure of two or more processing nodes. In this paper, we consider programs written in a version of Hoare's CSP and define a set of axioms and inference rules by which proofs can be constructed in three steps: proving the properties of each process when its communicants are prone to failure, establishing the effects of failure of each process, and combining these two steps to determing the fault tolerant properties of the whole program. The proof system is thus compositional, in the sense that proofs can be constructed in a modular way