Proof Rules for Fault-Tolerant Distributed Programs
Proving properties of fault tolerant distributed programs is a complex task as such proofs must take into account failures at all possible points in the execution of individual processes. The difficulty in accomplishing this is compounded by the need also to cater for simultaneous failures of two or more processes. 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 proofs to determine the fault tolerant properties of the whole program.