Symbolic Fault Injection

Fault tolerance mechanisms are a key ingredient of dependable systems. In particular, software-implemented hardware fault tolerance (SIHFT) is gaining in popularity, because of its cost efficiency and flexibility. Fault tolerance mechanisms are often validated using fault injection, comprising a variety of techniques for introducing faults into a system. Traditional fault injection techniques, however, lack coverage guarantees and may fail to activate enough injected faults. In this paper we present a new approach called symbolic fault injection which is targeted at validation of SIHFT mechanisms and is based on the concept of symbolic execution of programs. It can be seen as the extension of a formal technique for formal program verification that makes it possible to evaluate the consequences of all possible faults (of a certain kind) in given memory locations for all possible system inputs. This makes it possible to formally prove properties of fault tolerance mechanisms.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Daniel Larsson, Reiner Hähnle
• Keywords: Automated Reasoning, CADE 2007, Fault Tolerance Mechanisms, Hardware Fault Tolerance, Symbolic Fault Injection