Fault injection for the formal testing of fault tolerance

The authors address the issue of the use of fault injection for explicitly removing design/implementation faults in fault tolerance algorithms and mechanisms. A formalism is introduced that represents the fault tolerance algorithms and mechanisms by means of a set of assertions. This formalism enables the execution tree to be presented, where each path from the root to a leaf of the tree is a well-defined formula. It provides a framework for the generation of a functional deterministic test for programs implementing complex fault tolerance algorithms and mechanisms. This methodology has been used to extend a debugging tool aimed at testing fault tolerance protocols developed by BULL France. It has been successfully applied to the injection of faults in the inter-replica protocol supporting the application-level fault tolerance features of the architecture of the ESPRIT-funded Delta-4 project. The results of these experiments are discussed and analyzed.<>