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 mutation to behavioral models and requirements specifications. Unlike previous related approaches, the requirements specification is at the center of this process. A property coverage criterion is used to show that resulting test-cases sufficiently 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 testcase generation process reveals important details about the specification, such as vacuity and how much of the model it covers, without requiring additional costly computations.