Consistency Testing of C Programs

Software testing is today the primary tool used by software designers to eliminate errors and thus improve the quality of the software. However, no accepted systematic methods exists today which can help the designer to construct efficient tests (a small set of inputs) or to evaluate the quality of the given test, i.e., a measure of how well the software has been tested. Testing serves at least two purposes. One is to check the functionality, i.e., that the program behaves as the programmer is expecting. Another purpose is to check the robustness of the program, i.e., that it does not crash on extreme inputs. A program that is well-behaved (does not crash) for all inputs, although it might not compute the right result, is called a consistent program.

Model checking is a formal verification technique that exhaustively tries all possible executions. The technique has been developed for hardware and is used extensively by the industry. Its key advantage over other verification techniques like theorem provers is that it is completely automatic, thus eliminates the need for human verification experts.

This project will investigate the use of model checking as a tool to guide the construction of input sequences for testing the consistency of software. Through the use of predicates inserted by the programmer (assert-statements in C) consistency testing can also be used to check certain functional properties of the program. To make the consistency testing practical, only a subset of the C programming language is considered. Part of the project is to identify and eliminate programming constructs which drastically decreases the testability of the software.

The potential of the developed test generation technique will be evaluated through extensive experiments with academic benchmarks and real examples obtained from industrial contacts, among others DDC International.