Specification-based test generation and optimization using model checking

The capability of model checkers to construct counterexamples provides a basis for automated test generation. However, many model checking-based testing approaches just focus on generating test sets with respect to some coverage criteria. Such test sets generally are large and inefficient because of much redundancy. We propose an on-the-fly approach that performs test generation and redundancy elimination by turns. Our approach employs a test-tree to pick out and represent a subset of tests with equal coverage for a test criterion and no redundancy. Along with model checking for a property, a new test sequence is derived from the counterexample and is used to detect redundant properties, and then is winnowed by the test-tree as well. We demonstrate the approach by applying some small examples to our prototyped algorithm.