Method for designing and placing check sets based on control flow analysis of programs

Proposes a formal approach for adding fault detection to software. An assertion-based formalism is used to represent algorithm specifications. This representation is then used to generate a flowgraph or decision-to-decision graph (ddgraph), which is used to construct an execution path tree. The information gained from this algorithm representation is used to aid in the design of software-based fault tolerance techniques. Algorithm-based fault tolerance (ABFT) techniques are used to detect data structure-corrupting faults and checks are added to detect program flow errors. Flowgraph and ddgraph representations provide information to predict future program flow from the current flow. During execution, the current program location is recorded, along with the expected flow. Checks are placed to verify that the program flow follows the predicted flow. Fault coverage has been estimated through experiments with SOFIT (SOftware-based Fault Injection Tool), and the data is presented to demonstrate the effectiveness of the method