Login New user?  
01-Applied Mathematics & Information Sciences
An International Journal


Volumes > Volume 9 > No. 1L


Reduction of Model Checking-based Test Generation using Satisfiability

PP: 89-96
Gongzheng Lu, Huaikou Miao, Honghao Gao,
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.

  Home   About us   News   Journals   Conferences Contact us Copyright naturalspublishing.com. All Rights Reserved