Methods and apparatus for generating passive testers from properties
First Claim
1. A method for testing a software system U, comprising:
- (a) defining a formal specification of a logical property P that system U is required not to satisfy;
(b) generating a passive testing module T based upon property P to monitor system U;
(c) invoking a function F at specific invocation points during the execution of system U to compute an abstract representation of the state of system U at the current point of execution;
(d) passing the abstract representation computed by function F to passive testing module T in order to determine whether the abstract representation of the execution of system U to the current point matches illegal property P;
(e) declaring a "fail" result if the abstract representation matches illegal property P and declaring a "pass" result if the abstract representation of the execution of system U to the current point does not match illegal property P.
3 Assignments
0 Petitions
Accused Products
Abstract
Techniques and testers for testing a system U including the steps of (a) defining a formal specification of a logical property P that system U is required not to satisfy; (b) generating a passive testing module T based upon property P to monitor system U; (c) invoking a function F at specific invocation points during the execution of system U to compute an abstract representation of the state of system U at the current point of execution; (d) passing the abstract representation computed by function F to passive testing module T in order to determine whether the abstract representation of the execution of system U to the current point matches illegal property P; and (e) declaring a "fail" result if the abstract representation of the execution of system U to the current point matches illegal property P and declaring a "pass" result if the abstract representation of the execution of system U to the current point does not match illegal property P.
9 Citations
20 Claims
-
1. A method for testing a software system U, comprising:
-
(a) defining a formal specification of a logical property P that system U is required not to satisfy; (b) generating a passive testing module T based upon property P to monitor system U; (c) invoking a function F at specific invocation points during the execution of system U to compute an abstract representation of the state of system U at the current point of execution; (d) passing the abstract representation computed by function F to passive testing module T in order to determine whether the abstract representation of the execution of system U to the current point matches illegal property P; (e) declaring a "fail" result if the abstract representation matches illegal property P and declaring a "pass" result if the abstract representation of the execution of system U to the current point does not match illegal property P. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
-
-
12. A tester for testing a software system U, comprising:
-
a passive testing module T that is based upon a formal specification of a logical property P that system U is required not to satisfy; a state descriptor generator that receives, or has access to, current state data from software system U and computes an abstract representation of the state of system U at the current point of execution, a passive testing module T that is based upon a formal specification of a logical property P that system U is required not to satisfy, the passive testing module receiving as an input the abstract representation to the passive testing module in order to determine whether the abstract representation of the execution of system U to the current point matches illegal property P; means for declaring a "fail" result if the abstract representation of the execution of system U to the current point matches illegal property P and declaring a "pass" result if the abstract representation of the execution of system U to the current point does not match illegal property P. - View Dependent Claims (13, 14, 15, 16, 17, 18, 19, 20)
-
Specification