Coverage Criteria for State Transition Testing and Model Checker-Based Test Case Generation

State Transition Testing is an important category of software testing. Our work focuses on coverage criteria which adopt the notion of pair-wise testing. We propose an approach that uses model checking tool NuSMV to generate test cases that satisfy these coverage criteria from a given state chart specification. We also propose to use an algorithm for the set covering problem to reduce the number of test cases.