Methods and apparatus for passive mid-stream monitoring of real-time properties

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.

2. The method of claim 1 , wherein said system is expressively sufficient.

3. The method of claim 1 , wherein said real-time correctness property is expressed as a timed automaton.

4. The method of claim 1 , wherein said passively monitored mid-stream observation is rejected if and only if there is no correct system model that could exhibit the observed passively monitored mid-stream observation.

5. The method of claim 1 , wherein said intersection of said real-time correctness property and said timed correctness property includes behavior that satisfies both correctness properties.

6. The method of claim 1 , wherein said intersection of said real-time correctness property and said timed correctness property includes substantially all acceptable behavior according to said real-time correctness property that ends in said passively monitored mid-stream observation.

7. The method of claim 1 , wherein an empty set indicates that there is no acceptable behavior before said mid-stream observation that ends with said mid-stream observation.

8. The method of claim 1 , wherein said non-empty set indicates that there is an acceptable behavior before said mid-stream observation that ends with said mid-stream observation.

9. The method of claim 8 , wherein said non-empty set prevents said mid-stream observation from being classified as faulty.

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.

11. The method of claim 10 , wherein a real-time correctness property that is passively testable can achieve complete fault coverage using passive testing.

12. The method of claim 10 , wherein a real-time correctness property that can achieve complete fault coverage using passive testing is passively testable.

13. The method of claim 11 , wherein every system violating said correctness property can be determined to be faulty through analysis of mid-stream observations.

14. The method of claim 10 , further comprising the step of determining if an observed behavior is in said set of all timed traces.

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.

16. The apparatus of claim 15 , wherein said real-time correctness property is expressed as a timed automaton.

17. The apparatus of claim 15 , wherein said passively monitored mid-stream observation is rejected if and only if there is no correct system model that could exhibit the observed passively monitored mid-stream observation.

18. The apparatus of claim 15 , wherein said intersection of said real-time correctness property and said timed correctness property includes behavior that satisfies both correctness properties.

19. The apparatus of claim 15 , wherein said intersection of said real-time correctness property and said timed correctness property includes substantially all acceptable behavior according to said real-time correctness property that ends in said passively monitored mid-stream observation.

20. The apparatus of claim 15 , wherein an empty set indicates that there is no acceptable behavior before said mid-stream observation that ends with said mid-stream observation and said non-empty set indicates that there is an acceptable behavior before said mid-stream observation that ends with said mid-stream observation.

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.

22. The apparatus of claim 21 , wherein every system violating said correctness property can be determined to be faulty through analysis of mid-stream observations.

23. The method of claim 21 , wherein said processor is further configured to determine if an observed behavior is in said set of all timed traces.