Transformation of programs for fault-tolerance
Zhiming Liu, Mathai Joseph · Formal Aspects of Computing · 1992
Abstract In this paper we describe how a program constructed for afault-freesystem can be transformed into afault-tolerantprogram for execution on a system which is susceptible to failures. A program is described by a set of atomic actions which perform transformations from states to states. We assume that a fault environment is represented by a programF. Interference by the fault environmentFon the execution of a programPcan then be described as afault-transformationℱ which transformsPinto a program ℱ(P). This is proved to be equivalent to the programP□PF, wherePFis derived fromPandF, and □ defines the union of the sets of actions ofPandFP. A recovery transformation ℛ transformsPinto a program ℛ(P) =P□Rby adding a set ofrecovery actions R, called arecovery program. If the system isfailstopand faults do not affect recovery actions, we have ℱ(ℛ(P))=ℱ(P)□R=P□PF□RWe illustrate this approach to fault-tolerant programming by considering the problem of designing a protocol that guarantees reliable communication from a sender to a receiver in spite of faults in the communication channel between them.