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

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.

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.