Optimization of model checking-based test generation

Constructing test cases from the counterexamples generated by a model checker is an important means to perform test automation. The fact that multiple goals in the set of test goals may be covered by the same counterexample, however, leads to some redundant calls to the model checker in the process of test generation, and redundant test cases in test suite such that decrease seriously testing performance. An optimization approach to test generation based on dynamic monitoring is proposed. After a new test case is generated by model checking for a selected test goal, temporal logic formula rewriting technique is employed to reduce the set of test goals, those goals covered by the new test case are picked out. Meanwhile, the new test case is winnowed by the test suite to eliminate the redundancy when it is merged into the test suite. Experimental results illustrate that the proposed method is effective for reducing the numbers of calls to the model checker and the test suite.