|
|
 |
| |
|
|
|
Reduction of Model Checking-based Test Generation using Satisfiability |
|
|
|
PP: 89-96 |
|
|
|
Author(s) |
|
|
|
Gongzheng Lu,
Huaikou Miao,
Honghao Gao,
|
|
|
|
Abstract |
|
|
| Constructing test cases from counterexamples generated by a model checker is an important method to perform test
automation. In fact, one counterexample may cover multiple test goals, which leads to unnecessary calls to the model checker, and
redundant test cases in test suite such that affect the testing performance. A method to test suite reduction based on satisfiability is
proposed. The kripke model is translated in conjunction with test goals (trap properties) into CNFs. And then test goal to generate
counterexample is selected according to the hardness of the corresponding CNF, after that, model checking the selected test goal to
generate counterexample. The generated counterexample is translated in conjunction with those uncovered test goals into CNFs. If the
corresponding CNF is unsatisfiable then the test goal is picked out from the set of test goals. Meanwhile, the new generated test case
is winnowed by test suite to reduce the redundancy before it is added into the test suite. Experimental results show that the method
proposed in this paper is effective for reducing the model checker calls and the length of the test suite. At the same time, the coverage
and error detection capability of the test suite are not declined. |
|
|
|
|
|
|
|
