12 Technology of Test-Case Generation

Model based test case generation deals with the generation of test cases based on test case specifications and a model of the system under test (SUT). Since the number of possible test cases is in general too large to be practically useful, test case specifications are used to select

interesting

test cases. Therefore, test case generation can be seen as the search problem of finding appropriate test cases. In the previous chapter, several kinds of test case specifications, in particular coverage criteria, have been presented. In the current chapter, we will show how techniques from various fields in computer science such as program analysis and formal methods can be applied to generate test cases that satisfy such specifications. The input part of each test case can then be fed into the SUT whose output is compared with the output part of the test case in order to detect errors. In particular, we will cover test case generation by

theorem proving

,

symbolic execution

, and

model checking

. Although these techniques are often used in combination, we will describe them separately in order to show their applicability and specific features from different points of view.