Abstract
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.
[download the pdf file] [DOI]