A compositional framework for fault tolerance by specification transformation (Q1330423)

A program can be converted into a fault-tolerant version by incorporation of a recovery algorithm into the given program. The properties of the recovery algorithm itself appear only as a fixed part of any application of this transformation on a formulae, expressed in temporal logic. The converted, fault-tolerant program has accordingly other specification than the basic one. The paper introduces a framework in which such program transformations are accompanied by a corresponding specification transformation. The paper shows that it is not necessary to prove separately; the correctness of each transformed program, if the specification transformation has been carried out correctly. The paper presents a verification method for proving the correctness of the specification transformation. The introduced specification transformation can also be used for other applications of program superposition, such as for deadlock detection.