APPARATUS AND METHOD FOR TESTING COMPUTER PROGRAM IMPLEMENTATION AGAINST A DESIGN MODEL

摘要

A method of testing a computer program implementation according to a predefined design model, the program implementation having at least one method under test, employs a computer to generate a post-method corresponding to the method under test. A computer is further used to automatically generate a set of test cases. Then, using the automatically generated set of test cases, the computer explores different execution paths of the computer program implementation, by applying those test cases to both the method under test and the generated post-method, to reveal behavior that is not consistent with the behavior specified by the design model.

主权项

1. A method of testing a computer program implementation according to a predefined design model, the design model being of the type having a static model component and a dynamic model component, comprising:
identifying a method under test from within the computer program implementation; using a computer to extract the dynamic model component and generate a post-method corresponding to the method under test; using a computer to store an initial test case value having a corresponding initial input parameter set comprising at least one parameter; using a computer to instrument for symbolic execution both the method under test and the post-method; using a computer to run the instrumented method under test and to build a first symbolic memory representation corresponding to a first execution path condition of the method under test, the first symbolic memory representation being stored in non-transitory computer-readable memory as a path condition (PC); using a computer to run the instrumented post-method, and using the first symbolic memory representation to build a second symbolic memory representation corresponding to the post-method, the second symbolic memory representation being stored in non-transitory computer-readable memory as a post-method path condition (PCpost); using a computer to test the returned Boolean state of the post-method path condition and store an indication in computer memory that an error has been detected if the returned Boolean state is FALSE and to perform the following steps if the returned Boolean state is TRUE; using a computer to execute a satisfiability (SAT) solver algorithm to analyze whether all members of the input parameter set satisfying the path condition PC also satisfy the post-path condition PCpost and thereby determine that PC and PCpost correspond to a tautology relationship; using a computer to further evaluate the relationship between PC and PCpost as follows: if a tautology relationship is found, generate a second test case value, different from the initial test case value and run the instrumented method under test and post-method again using an execution path for the method under test that is different from the first execution path condition; if a tautology relationship is not found, generate a third test case value, having a parameter set different from the initial parameter set.