Patent ID: 7865339

Claim:
A method for test case generation to produce test cases from counterexamples produced by a formal analysis system relative to a model of a system under test comprising steps of: submitting the model and at least one predicate characterizing test targets to the formal analysis system with an assertion that none of the predicates is satisfiable; identifying one or more of the test targets that are satisfied by a first test case; eliminating one or more portions of the model that cannot contribute to a satisfaction of one or more of the test targets not satisfied by the first test case, wherein the eliminating results in a reduced model, and wherein the eliminating is performed each time at least one of the test targets is satisfied; obtaining a new counterexample from the formal analysis system in accordance with the reduced model, wherein the new counterexample is an extension to at least a part of a previously known counterexample from which the first test case is extracted, wherein the formal analysis system uses a processor to adapt a non-initial state of the previously known counterexample as an initial state from which to calculate the new counterexample; extracting a new test case from the new counterexample to cause the one or more of the test targets that cannot be satisfied by the first test case to be reached by the system under test; and forming a set of test cases, wherein the set of test cases includes the first test case and the new test case.