Design, verification, and validation of self-checking software components

We propose a formal approach for adding fault detection to software. An assertion-based formalism is used to represent specifications and verify completeness and consistency. This specification is used to generate a flow graph, which is used to construct an exemplar-path tree. This representation is then used to generate an input set to exercise and verify the implementation. Previous software fault-tolerance (SFT) techniques emphasized algorithm-based fault tolerance (ABFT) which focused on detecting hardware faults that corrupted data structure contents. We propose a method that also detects hardware faults, which cause program flow errors. Our technique embeds two types of software checks. The first is based on the ABFT techniques described in the literature. The second type of check is used to detect faults that cause program flow errors. The exemplar-path tree provides information that can be used to predict a future program location, given the current location. During execution, program locations are recorded, along with expected locations, as determined from the exemplar-path tree. This information then is used to verify, that the future location is executed as expected. Hardware fault coverage has been estimated through experiments with the fault injection tool, SOFIT. Faults of differing durations were injected into memory, address bus, data bus, and CPU registers. The data presented, demonstrate the effectiveness of the method for detecting hardware faults