Questions: Runtime Verification

Question 1

An LTL property 'G(request -> F grant)' (every request is eventually granted) is monitored over a finite execution trace that ends with an ungranted request. What does the monitor report?

• A. Violation: the property is definitively false
• B. Satisfaction: the property is definitively true
• C. Inconclusive: the trace neither satisfies nor violates the property because the grant may still occur in a future extension of the trace
• D. Error: LTL cannot be monitored at runtime

Answer: (C)

LTL semantics are defined over infinite traces. A finite trace with a pending request has not yet violated G(request -> F grant) because a future extension could still provide the grant. It has not satisfied it either, because the trace might end without granting. This is the fundamental challenge of runtime verification: finite observations of potentially infinite behaviors. Three-valued LTL (LTL3) extends classical LTL with a third truth value 'inconclusive' (or 'unknown') for exactly these cases. A property is violated only when NO possible extension of the current trace can satisfy it; it is satisfied only when ALL extensions satisfy it.

Question 2

Runtime verification can detect all violations of safety properties (nothing bad happens) on a single execution trace, but cannot definitively verify liveness properties (something good eventually happens) from a finite prefix.

• T. True
• F. False

Answer: True

Safety properties have the characteristic that any violation occurs at a finite prefix: if 'nothing bad happens' is violated, there is a specific finite point where the bad thing occurred, and no future extension can undo it. A runtime monitor can detect this immediately. Liveness properties (G(request -> F grant), for example) require something to happen eventually -- a finite trace where it has not yet happened is always potentially satisfiable by a future extension. A monitor can report 'not yet violated' but never 'definitely satisfied' for an unrestricted liveness property. This safety/liveness distinction is fundamental to understanding what runtime verification can and cannot guarantee.

Question 3

Explain the difference between offline and online runtime verification, and describe one advantage of each approach.

Model answer: Online runtime verification instruments the running system and checks properties incrementally as events occur, enabling immediate reaction to violations (triggering recovery, logging, or shutdown). Its advantage is real-time detection and response. Offline runtime verification analyzes recorded execution logs after the fact, checking properties against complete trace files. Its advantage is zero runtime overhead on the monitored system and the ability to use more expensive analysis algorithms since timing constraints are relaxed. Online monitors must be extremely efficient (often constant time per event) to avoid perturbing system timing; offline monitors can afford multi-pass algorithms over the complete trace.

The choice depends on the application domain. Safety-critical systems (avionics, medical devices) typically use online monitoring for immediate hazard detection. Performance analysis, debugging, and compliance auditing typically use offline monitoring. Hybrid approaches log events in a low-overhead buffer and process them in a separate thread or on a separate machine, combining the benefits of both.

Question 4

Specification mining (or trace-based invariant inference) derives formal specifications from observed execution traces rather than checking given specifications. How does this relate to runtime verification?

Model answer: Specification mining is the dual of runtime verification: instead of checking a given property against traces, it infers likely properties from traces. Tools like Daikon infer likely invariants (e.g., 'x > 0 at this program point') from observed variable values; other tools mine temporal patterns (e.g., 'lock is always acquired before accessing shared data'). The mined specifications can then be used as inputs to runtime verification monitors in future executions, or fed back to developers for review and formal verification. This creates a feedback loop: observed behavior generates candidate specifications, which are then monitored and refined. The limitation is that mined properties are hypotheses based on observed behavior, not proven invariants -- they may be coincidences of the observed traces.

Specification mining addresses the specification bottleneck -- the difficulty of writing formal specifications for complex systems. In practice, many teams adopt runtime verification without complete formal specs by mining specifications from test suite runs, then monitoring production executions against these mined properties. Anomalies (violations of mined properties) become bug reports. This pragmatic approach has been adopted in industry, notably by Amazon (for AWS service monitoring) and Google (for distributed system invariant checking).

Question 5

A runtime verification monitor for a concurrent system observes a single interleaving of events. Can it detect property violations that would occur in alternative interleavings that were not observed?

• A. No -- runtime verification can only check the observed trace, never alternative interleavings
• B. Yes -- predictive runtime verification techniques analyze the observed trace to infer violations in feasible alternative interleavings by computing a partial order of events and checking all consistent total orders
• C. Yes -- runtime verification always checks all possible interleavings
• D. Only if the monitor uses model checking internally

Answer: (B)

Predictive runtime verification goes beyond checking the single observed trace. It extracts a partial order of events from the trace (using happens-before relations from locks, thread joins, etc.) and checks whether any linearization of this partial order consistent with the program's synchronization semantics violates the property. This dramatically increases the coverage of a single execution. Tools like RV-Predict and Java PathFinder's runtime analysis use SMT solvers or specialized algorithms to explore the space of feasible reorderings. The cost is higher analysis time per trace, but the coverage approaches that of systematic concurrency testing while requiring only a single execution.