Predicate-based test coverage and generation
First Claim
1. 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, 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 oath is feasible.
2 Assignments
0 Petitions
Accused Products
Abstract
Techniques and tools for achieving improved test coverage in a finite program state space are described, such as a technique for selecting a set of predicates, calculating a set of possible predicate values, calculating a subset of the set of possible predicate values, and generating a test for the computer program based at least in part on the subset. The subset comprises an approximation (e.g., an under-approximation) of reachable states in the program. A superset of the set of possible predicate values also can be calculated; the superset comprises an over-approximation of the reachable states in the program. In another aspect, a Boolean abstraction of a program is generated, reachability analysis is performed based at least in part on the Boolean abstraction, and symbolic execution is performed to generate test data. The reachability analysis can include computing lower and/or upper bounds of reachable observable states.
296 Citations
23 Claims
-
1. 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, 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 oath is feasible. - View Dependent Claims (2, 3, 4, 5, 6)
-
-
7. 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.
-
-
8. 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.
-
-
9. 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.
-
-
10. 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. - View Dependent Claims (11, 12, 13, 14, 15, 16, 17, 19, 20, 21, 22, 23)
-
-
18. 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.
-
Specification