An Evaluation of Specification Based Test Generation Techniques Using Model Checkers

Test case generation can be represented as a model checking problem, such that model checking tools automatically generate test cases. This has previously been applied to testing techniques such as coverage criteria, combinatorial testing, mutation testing, or requirements testing, and further criteria can be used similarly. However, little comparison between the existing techniques has been done to date, making it difficult to choose a technique. In this paper we define existing and new criteria in a common framework, and evaluate and compare them on a set of realistic specifications. Part of our findings is that because testing with model checkers represents the test case generation problem in a very flexible way best results can be achieved by combining several techniques from different categories. A best effort approach where test cases are only created for uncovered test requirements can create relatively small test suites that cover many or all different test techniques.