Projects:Bounded Exhaustive Testing with Contracts
From SEWiki
The basic goal of software testing is to apply limited resources to identify, create, and execute those test cases which are most likely to reveal faults. Testing all inputs, while attractive in theory, is not practically feasible. As a result, researchers employ input partitioning techniques, under the assumption that a single representative input is as likely as the other members of the partition to reveal a fault. Unfortunately, many faults in complex software systems involve subtle interactions and rare sequences or combinations of events. Developing test cases that can identify such faults is inherently difficult because such test cases violate the partition equivalence assumption.
Symbolic testing techniques exist for identifying inputs that can cause subtle interactions to occur in code, but they are difficult to apply in practice because they do not scale well. Black-box approaches, in contrast, are easy to apply and have been shown to achieve high code coverage at least for some types of systems. Our research investigates a particular black-box testing approach called bounded exhaustive testing, where all the the inputs within some bounded region of the program's input space are tested. As part of this effort, we investigate techniques for generation of structurally-complex test data.
Bounded exhaustive testing is inspired by the success of model checking, where the state space defined by a specification is explored in an exhaustive fashion, searching for a sequence of state transitions that fails to satisfy some property. This approach is successful in finding rare sequences that fail the property. A key assumption of model checking is that a counterexample can usually be found within some small initial segment of the state space. Importantly, abstraction techniques such as exploiting symmetry are rigorously correct, unlike less rigorous testing techniques such as input partitioning.
Daniel Jackson suggests that such an approach might work for code verification, calling it the "small scope hypothesis": most of the faults can be found by testing an exhaustive initial segment of the inputs. However, in the extreme full exhaustive testing is usually infeasible due to the "input space explosion problem", which is analogous to the state explosion problem faced by model checking. That is, exhaustive testing is exhaustive in the input space, treating the software as a block box.
Key research questions for bounded exhaustive testing are:
- What is the distribution of faults relative to input size (starting with the smallest)? i.e. Is Jackson's hypothesis true?
- How does exhaustive testing compare to random testing? i.e. What is the distribution of faults relative to input size (not starting with the smallest)?
- What is the correct bound? Can we predict the bound based on static analysis of the code? (i.e. Is there a correlation between the bound and the number of nodes in the control flow graph?) Can we know when to stop during testing?
- What sound partitioning approaches are there to reduce the input space? Can we validate these approaches empirically?
- How does this approach compare to traditional testing approaches in terms of testing efficiency, tester efficiency, percent of faults found, etc.?
In related work, we developed yagg, "yet another generator generator". This tool, when given a YACC-like grammar that specifies the input space, exhaustively generates inputs of increasing size. The tool supports context-sensitive constraints that allow us to generate inputs as structurally-complex as computer programs.
