Predicate-based test coverage and generation

A tangible computer-readable storage medium having stored thereon computer-executable instructions for performing a method of performing test generation for a computer program, the method comprising:

• generating a Boolean abstraction of the computer program, wherein the generating comprises selecting a set of predicates in the computer program and calculating a set of possible predicate values for plural statements in the computer program, wherein at least one of the predicates is derived from a conditional statement of the computer program;
• performing a state reachability analysis of the computer program, wherein performing the state reachability analysis comprises identifying a subset of the set of possible predicate values for the plural statements in the computer program, wherein the subset comprises an approximation of reachable states in the computer program, and outputting a set of paths that covers states in the approximation of reachable states;
• and
• performing symbolic execution, wherein the symbolic execution determines whether the paths are feasible and generates inputs for the computer program to cover a path when the path is feasible.

In a computer system, a method of performing test generation for a computer program, the method comprising:

• generating a Boolean abstraction of the computer program, comprising selecting a set of predicates in the computer program, and calculating a set of possible predicate values for plural statements in the computer program;
• performing a state reachability analysis of the computer program, wherein the state reachability analysis comprises finding a set of reachable states of the computer program, the state reachability analysis based at least in part on the Boolean abstraction of the computer program;
• and
• performing symbolic execution to generate test data for testing the computer program;
• wherein the state reachability analysis further comprises computing an upper bound of reachable observable states of the computer program, comprising states with valid correlations between the predicates in the set of predicates;
• wherein the state reachability analysis further comprises computing a lower bound of reachable observable states of the computer program, the lower bound comprising states reachable from states with valid correlations between the predicates in the set of predicates;
• wherein the state reachability analysis further comprises outputting a set of paths that covers states in the upper bound of reachable states;
• and
• wherein the symbolic execution comprises determining whether the paths are feasible and generates inputs for the computer program to cover a path when the path is feasible.

A tangible computer-readable storage medium having stored thereon computer-executable instructions for performing a method of performing test generation for a computer program, the method comprising:

• generating a Boolean abstraction of the computer program, comprising selecting a set of predicates in the computer program, and calculating a set of possible predicate values for plural statements in the computer program;
• performing a state reachability analysis of the computer program, wherein the state reachability analysis comprises finding a set of reachable states of the computer program, the state reachability analysis based at least in part on the Boolean abstraction of the computer program;
• and
• performing symbolic execution to generate test data for testing the computer program;
• wherein the state reachability analysis further comprises computing an upper bound of reachable observable states of the computer program, comprising states with valid correlations between the predicates in the set of predicates;
• wherein the state reachability analysis further comprises computing a lower bound of reachable observable states of the computer program, the lower bound comprising the states reachable from states with valid correlations between the predicates in the set of predicates;
• wherein the state reachability analysis further comprises outputting a set of paths that covers states in the upper bound of reachable states;
• and
• wherein the symbolic execution comprises determining whether the paths are feasible and generates inputs for the computer program to cover a path when the path is feasible.

In a computer system, a method of modeling behavior of a computer program:

• generating a Boolean abstraction of the computer program, wherein the generating comprises deriving an initial plurality of predicates;
• wherein a predicate is derived from at least one of a conditional statement, an assertion, or a run-time safety check of the computer program;
• performing a state reachability analysis of the computer program, wherein performing the state reachability analysis comprises defining an upper bound for a set of reachable observable states in the computer program wherein the reachable observable states comprise an evaluation of a state of the predicate at a statement in the computer program;
• defining a lower bound for the set of reachable observable states in the computer program;
• using the upper bound and the lower bound to form a static coverage metric of the computer program, which measures an amount of test coverage;
• forming a behavior model of the computer program using the upper and lower bound, wherein forming the behavior model comprises outputting a set of oaths that covers states in the lower bound for the set of reachable observable states in the computer program;
• performing symbolic execution, wherein the symbolic execution determines whether the paths are feasible and generates inputs for the computer program to cover a path out of the paths when the path is feasible and comprises performing test generation of reachable states based at least in part on the behavior model wherein a percentage of reachable observable states are covered by a generated test;
• and
• adding new predicates to the initial plurality of predicates to increase percentage of reachable observable states covered by a generated test.

A tangible computer-readable storage medium having stored thereon computer-executable instructions for performing a method of modeling behavior of a computer program:

• generating a Boolean abstraction of the computer program, wherein the generating comprises deriving an initial plurality of predicates;
• wherein a predicate is derived from at least one of a conditional statement, an assertion, or a run-time safety check of the computer program;
• performing a state reachability analysis of the computer program, wherein performing the state reachability analysis comprises defining an upper bound for a set of reachable observable states in the computer program wherein the reachable observable states comprise an evaluation of a state of the predicate at a statement in the computer program;
• defining a lower bound for the set of reachable observable states in the computer program;
• using the upper bound and the lower bound to form a static coverage metric of the computer program, which measures an amount of test coverage;
• forming a behavior model of the computer program using the upper and lower bound, wherein forming the behavior model comprises outputting a set of paths that covers states in the lower bound for the set of reachable observable states in the computer program;
• performing symbolic execution, wherein the symbolic execution determines whether the paths are feasible and generates inputs for the computer program to cover a path out of the paths when the path is feasible and comprises performing test generation of reachable states based at least in part on the behavior model wherein a percentage of reachable observable states are covered by a generated test;
• and
• adding new predicates to the initial plurality of predicates to increase percentage of reachable observable states covered by a generated test.