Symbolic Fault Injection

Computer systems are vulnerable to a number of different faults that may affect their ability to produce what is expected from them. These faults include: defect hardware components, electro-magnetic interference and ionizing radiation that change the content of memory cells and registers, specification/design/implementation mistakes concerning both hardware and software. In order to build computer systems that are dependable, we must make the systems tolerate these kind of faults. We must have mechanisms in our systems that detect faults and recover from these faults.

The most common method to evaluate fault tolerance mechanisms is fault
injection: a collection of techniques for deliberately introducing faults in computer systems in order to test their fault-tolerance capabilities. One big problem with conventional fault injection techniques is the coverage issue. For all systems of any size it is impossible to inject all possible faults into the system; they are simply too many. In other words, we cannot test our system for all faults that could occur (we cannot achieve 100% coverage).

The topic of this thesis is symbolic fault injection. The main objective with this approach is to address the coverage problem just mentioned. The idea of symbolic fault injection is based on the concept of symbolic
execution of source code. To execute a program symbolically means to simulate its execution using variables as input instead of concrete values. The program state and output will therefore be in the form of expressions involving the input variables instead of concrete values. This makes it possible to investigate the properties of a program - not just for a particular indata but for all possible indata. Symbolic execution is for example used in tools for formal verification to prove properties about programs. Typically, some kind of logical formalism is then used to represent both the program and the specification of the program, and to symbolically execute the program.

Symbolic fault injection includes injection of symbolic faults in the program state and symbolic execution of the program to investigate the consequences of these faults. A symbolic fault is then a representation, in a logical formalism, of a whole class of real faults, i.e. faults that can appear in real systems.

The thesis consists of a theoretical investigation of the concept of symbolic fault injection and experiments with a tool for formal verification. This tool (the KeY tool) has the properties needed to experiment with symbolic fault injection.

Prerequisite: Some knowledge in logic/formal methods.

Contact Daniel Larsson ([email protected]) at Department of Computer
Science and Engineering, Chalmers University of Technology.