Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates

Automatic test case generation from a pre-post 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. In this paper, 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 then extend the discussion to variables of compound types such as set, sequence, and composite types. Finally, case studies are presented to assess the feasibility and effectiveness of our approach.