Test Case Generation from Conjunctions of Predicates with Model Checking

Automatic test case generation from a prepost style formal specification must deal with the issue of how to generate test cases from a conjunction of atomic predicate expressions, but unfortunately this problem has not been effectively solved due to its intrinsic difficulty. We describe a practical approach to tackling this problem by utilizing the model checking technique. An algorithm that converts test case generation from a conjunction of atomic predicate expressions into model checking is proposed. We discuss how the algorithm deals with atomic predicate expressions involving only variables of numeric types, and extend the discussion to variables of compound types such as set, sequence, and composite types. Case studies are presented to assess the feasibility and effectiveness of our approach.