Creating Test-Cases Incrementally with Model-Checkers

Abstract: Test-case generation with model-checkers is a promising field of research in software testing. Model-checker based approaches offer many advantages: They are fully automated, they are flexible due to different concrete techniques, and under certain conditions they are also efficient. There are still many issues that need to be resolved in order to achieve widespread acceptance in the industry. Because model-checkers were not originally designed with test-case generation in mind, a large per-centage of the test-cases produced are duplicates. Many of the remaining test-cases share identical prefixes that do not contribute to the overall fault sensitivity of a test-suite. Some test criteria also result in large test-suites of rather short test-cases. In this paper, we address these problems and suggest to create test-cases incrementally instead of separately for each test requirement. For this, heuristics based on an es-timated distance between a state and a temporal logic formula are presented, which allows to chose which test-case to extend with regard to which test requirement.