Improving Model-Checkers for Software Testing

In recent years, automated test-case generation with model-checkers has seen increasing attention in the research community. The use of model-checkers for testing offers full automation, a choice of different methods to derive test-suites, and is efficient under certain preconditions. Model-checkers, however, were not originally intended for this task. Therefore, there are several drawbacks that a tester has to cope with. If model-checkers were designed or adapted to take into account the needs that result from the application to software testing, this could lead to significant improvements with regard to test-suite quality and performance. In this paper, we discuss the drawbacks of current model-checkers when used for testing, and suggest ten ways in which model-checkers could be enhanced to be better suited for the task of test-case generation.