Methods and apparatus for passive mid-stream monitoring of real-time properties
First Claim
1. A method for determining whether a system is faulty, comprising:
- obtaining a real-time correctness property of said system;
obtaining a passively monitored mid-stream observation of said system;
constructing a timed correctness property from said passively monitored mid-stream observation that includes substantially all possible behaviors of said system prior to said passively monitored mid-stream observation;
determining an intersection of said real-time correctness property and said timed correctness property; and
determining whether said intersection is an empty set.
5 Assignments
0 Petitions
Accused Products
Abstract
Methods and apparatus are provided for passive mid-stream monitoring of real-time properties. A passive mid-stream monitoring process is disclosed that determines whether a system is faulty. The passive mid-stream monitoring process obtains a real-time correctness property and a passively monitored mid-stream observation of the system. A timed correctness property, Aσ, is constructed from the passively monitored mid-stream observation. An intersection of the real-time correctness property and the timed correctness property is then determined to determine if the system is faulty. A passively testable determination process is also disclosed that determines whether a real-time correctness property for a system is passively testable. A determination is made as to whether (i) a set of all timed traces that are correct according to the real-time correctness property is timed prefix and timed suffix closed; and (ii) a system would satisfy the real-time correctness property if all timed-trace behaviors of the system would be included in the set.
-
Citations
23 Claims
-
1. A method for determining whether a system is faulty, comprising:
-
obtaining a real-time correctness property of said system;
obtaining a passively monitored mid-stream observation of said system;
constructing a timed correctness property from said passively monitored mid-stream observation that includes substantially all possible behaviors of said system prior to said passively monitored mid-stream observation;
determining an intersection of said real-time correctness property and said timed correctness property; and
determining whether said intersection is an empty set. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9)
-
-
10. A method for determining whether a real-time correctness property for a system is passively testable, comprising:
-
determining whether a set of all timed traces that are correct according to said real-time correctness property is timed prefix and timed suffix closed; and
determining that a system would satisfy said real-time correctness property if all timed-trace behaviors of said system would be included in said set. - View Dependent Claims (11, 12, 13, 14)
-
-
15. An apparatus for determining whether a system is faulty, the apparatus comprising:
-
a memory; and
at least one processor, coupled to the memory, operative to;
obtain a real-time correctness property of said system;
obtain a passively monitored mid-stream observation of said system;
construct a timed correctness property from said passively monitored mid-stream observation that includes substantially all possible behaviors of said system prior to said passively monitored mid-stream observation;
determine an intersection of said real-time correctness property and said timed correctness property; and
determine whether said intersection is an empty set. - View Dependent Claims (16, 17, 18, 19, 20)
-
-
21. An apparatus for determining whether a real-time correctness property for a system is passively testable, the apparatus comprising:
-
a memory; and
at least one processor, coupled to the memory, operative to;
determine whether a set of all timed traces that are correct according to said real-time correctness property is timed prefix and timed suffix closed; and
determine that a system would satisfy said real-time correctness property if all timed-trace behaviors of said system would be included in said set. - View Dependent Claims (22, 23)
-
Specification