Using Model-Checkers for Mutation-Based Test-Case Generation, Coverage Analysis and Specification Analysis

Automated software testing is an important measure to improve software quality and the efficiency of the software development process. We present a model-checker based approach to automated test-case generation applying muta-tion to behavioral models and requirements specifications. Unlike previous related approaches, the requirements spec-ification is at the center of this process. A property cover-age criterion is used to show that resulting test-cases suffi-ciently exercise all aspects of the specification. A test-suite derived from the specification can only be as good as the specification itself. We demonstrate that analysis of the test-case generation process reveals important details about the specification, such as vacuity and how much of the model it covers, without requiring additional costly computations. 1