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

• US 20070124456A1
• Filed: 11/29/2005
• Published: 05/31/2007
• Est. Priority Date: 11/29/2005
• Status: Active Grant

• Current Assignee: WSOU Investments, LLC (WSOU Holdings, LLC)
• Original Assignee: Alcatel-Lucent USA, Inc. (Nokia Corporation)
• Inventors: Jagadeesan, Lalita, Viswanathan, Ramesh
• Granted Patent: US 7,599,688 B2
• Time in Patent Office: Days
• US Class Current: 709/224
• CPC Class Codes: G06Q 50/32 Post and telecommunications franking apparatus G07B17/00
• CPC Class Codes: G06Q 50/60 Business processes related to postal services shipping G06Q10/083; franking apparatus G07B17/00
• CPC Class Codes: H04L 41/06 Management of faults, events, alarms or notifications
• CPC Class Codes: H04L 43/00 Arrangements for monitoring or testing data switching networks
• CPC Class Codes: H04L 43/10 Active monitoring, e.g. heartbeat, ping or trace-route
• CPC Class Codes: H04L 43/50 Testing arrangements

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.

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.

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 a 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.

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 whether said intersection is an 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 a 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.