Fault injection for formal testing of fault tolerance

TLDR

The study investigates using fault injection to eliminate design and implementation faults in complex fault‑tolerance algorithms and mechanisms. A formalism based on assertions generates an execution tree whose paths define well‑specified formulas, forming a framework that characterizes test sequences and determines input patterns through structural criteria. The framework enables deterministic testing of programs implementing FTAM, was integrated into a BULL France debugging tool, successfully applied to the ESPRIT Delta‑4 inter‑replica protocol, and uncovered two previously unknown fault‑tolerance deficiency faults.

Abstract

This study addresses the use of fault injection for explicitly removing design/implementation faults in complex fault-tolerance algorithms and mechanisms (FTAM), viz, fault-tolerance deficiency 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 framework that fully characterizes the test sequence. The input patterns of the test sequence (fault and activation domains) then are determined to fewer 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 testing 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 though the target protocol had been independently verified formally, the application of the proposed testing strategy revealed two fault-tolerance deficiency faults.