FAULT INJECTION FOR FORMAL TESTING OF FAULT-TOLERANCE

Summ & Conclusions - This study addresses the use of fault injection f or explicitly removing design/implementation faults in complex fault-t olerance algorithms & mechanisms (FTAM), viz, fault-tolerance deficien cy faults. A formalism is introduced to represent the FTAM by a set of assertions. This formalism enables an execution tree to be generated, where each path from the root to a leaf of the tree is a well-defined formula, The set of well-defined formulas constitutes a useful framew ork that fully characterizes the test sequence, The input patterns of the test sequence (fault & activation domains) then are determined to cover specific structural criteria over the execution tree (activation of proper sets of paths), This provides a framework for generating a functional deterministic test for programs that implement complex FTAM . This methodology has been used to extend a debugging tool aimed at t esting fault tolerance protocols developed by BULL France. It has been applied successfully to the injection of faults in the inter-replica protocol that supports the application-level fault-tolerance features of the architecture of the ESPRIT-funded Delta-4 project. The results of these experiments are analyzed in detail, In particular, even thoug h the target protocol had been independently verified formally, the ap plication of the proposed testing strategy revealed two fault-toleranc e deficiency faults.