Increasing Diversity in Coverage Test Suites Using Model Checking

Automated test case generation often results in test suites containing significant redundancy such as test cases that are duplicates, prefixes of other test cases, or cover the same test requirements. In this paper we consider the fact that items described by a coverage criterion can be covered in different ways. We introduce a technique where each created test case is guaranteed to cover a test requirement in a new way, even if it has previously been covered. This increases the diversity of how test objectives are satisfied, thus reducing the redundancy in test suites, improving their fault detection ability, and usually also decreasing the number of test cases generated. This approach is based in a scenario of specification based testing using model checkers as test case generation tools, and evaluation is performed on three different case study specifications.