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 if an acceptable behavior exists based on whether said intersection is a non-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 if an acceptable behavior exists based on whether said intersection is a non-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, wherein one or more of said steps are preformed by a processor. - 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 if an acceptable behavior exists based on whether said intersection is a non-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