Technical Summary: A Unified Framework for Runtime Verification and Model-Based Diagnosis in Lola

Problem Statement

Safety-critical systems require not only the detection of failures but also the localization of their root causes to enable effective mitigation. While Runtime Verification (RV) is effective for detecting deviations from specified behavior during execution, and Model-Based Diagnosis (MBD) is a principled framework for identifying faulty components, these two techniques have historically operated in isolation. Traditional RV monitors analyze system behavior over potentially unbounded state sequences to detect violations, whereas MBD typically operates at a single, unspecified point in time after a fault has been detected. Furthermore, existing integrations often fail to map detected failure actions directly to abnormal components in the MBD sense or lack the ability to handle uncertain inputs and temporal fault dynamics within a unified, stream-based reasoning framework.

Methodology

The paper proposes a unified framework that integrates stream-based RV and MBD within Lola, a synchronous stream-based specification language. The core methodology involves encoding both verification and diagnostic information as specialized streams, allowing for continuous observation and symbolic reasoning under uncertainty.

1. Unified Encoding in Lola

The authors map a diagnosed system $S = (sd, comps)$ to a Lola System $(\phi, comps)$:

• System Description ($sd$): Encoded into the assumption stream ($\alpha$), which is true by definition. This stream contains the behavioral knowledge (e.g., $\neg ab(c) \to beh_c$) and general knowledge of the system.
• Components ($comps$): Each component $c$ is represented by an internal Boolean stream where true indicates the component is abnormal ($ab(c)$).
• Observations: Observable system variables (inputs/outputs) are modeled as input streams, which can be certain (deterministic) or uncertain (non-deterministic intervals or sets).
• Unobservable Variables: Internal system values not directly measured are modeled as internal streams.
• Diagnosis Problem Instance (DPI): A tuple $(\phi, comps, \Psi)$, where $\Psi$ represents the history of input constraints up to the current time.

2. Symbolic Reasoning and Diagnosis Computation

The framework utilizes a symbolic monitor that maintains a constraint set $[\phi]_{\Psi}^{\leq t}$ representing all possible system behaviors consistent with observations up to time $t$.

• Constraint Solving: An SMT solver (e.g., Z3) is used to check consistency and derive entailments.
• Diagnosis Derivation: A diagnosis is an assumption about the state (normal/abnormal) of components that makes the system description consistent with observations. The framework computes minimal diagnoses by identifying minimal conflicts (sets of components that cannot all be normal) and calculating their minimal hitting sets.
• Pruning: To ensure constant-time and constant-space monitoring, pruning strategies rewrite constraints to bound the size of the constraint set, retaining only necessary historical information.

3. Diagnostic Scenarios

The framework supports three distinct diagnostic modes based on the temporal nature of component faults:

• Multi-Instant Diagnosis: Assumes component states are static over a window of $k$ past instants ($t-k$ to $t$). A $k$-instant diagnosis explains all observations within this window. The paper proves that for atemporal specifications, $k$-instant diagnoses are equivalent to aggregating single-instant diagnoses, but for temporal specifications (with non-zero offsets), they provide more focused results.
• Temporal Diagnosis: Allows component states to change over time. A $k$-temporal diagnosis is a set of pairs $(c, t')$ indicating that component $c$ is abnormal specifically at time $t'$. This is critical for identifying transient failures (e.g., overheating) or faults that manifest later due to propagation.
• Extended Settings: The framework naturally incorporates background knowledge (forcing components to be normal), strong fault models (specifying specific faulty behaviors), and abstract modeling.

Key Contributions

1. Unified Encoding: A method to express system descriptions and diagnostic assumptions as specialized streams in Lola, implicitly representing all valid diagnoses for observed behavior.
2. Multi-Instant Diagnosis Theory: A generalized theory for diagnosing time-invariant faults over a sliding window of observations, which subsumes standard multi-observation diagnosis as a special case.
3. Temporal Diagnosis: Support for time-varying abnormality, enabling the identification of when a fault occurs, not just which component is faulty.
4. Flexible Diagnostic Scenarios: The ability to elegantly handle background knowledge, abstract modeling, and various fault types (persistent vs. transient) within a single stream-based framework.
5. Implementation and Evaluation: A prototype implementation integrating the HS-Tree algorithm, QuickXplain, and Z3, validated on ISCAS85 and ISCAS89 benchmarks.

Results

The authors evaluated the framework on two Boolean circuits:

• c17 (ISCAS85): A purely combinational circuit with 6 components.
• s27 (ISCAS89): A sequential circuit with 14 components.

Findings:

• Feasibility: The framework successfully identified actual injected faults (stuck-at-false) in both circuits.
• Temporal Accuracy: For the sequential circuit (s27), the framework correctly localized faults only when the observation window ($k$) was large enough to cover the fault's origin and propagation time.
• Performance:
  • Runtime increased with larger $k$ values. For c17, $k$-instant diagnosis took up to 246 ms ($k=0$) and 775 ms ($k=31$) per instant.
  • Temporal diagnosis was significantly more expensive due to the combinatorial explosion of treating $(c, t')$ as distinct components. For c17, temporal diagnosis took up to 8.7 seconds per instant for $k=5$ and 136 seconds for $k=12$.
  • Despite the computational cost, the authors note that with constant $k$, runtimes remained independent of the total trace length, confirming the viability of the pruning strategies.

Significance and Claims

The paper claims to provide a compact, well-founded integration of Runtime Verification and Model-Based Diagnosis. Its significance lies in bridging the gap between automated fault detection (RV) and systematic fault localization (MBD) within a single, stream-based framework.

The authors emphasize that this approach:

• Supports uncertain inputs and environmental assumptions, allowing for refined inference based on expert knowledge.
• Enables online diagnosis by leveraging symbolic reasoning to produce verdicts at each time point.
• Offers a synergistic combination where the strengths of RV (efficient, continuous monitoring) and MBD (principled root cause analysis) are unified.
• Provides a sound framework where the symbolic monitor ensures that deduced values are consistent with all possible worlds defined by the constraints.

The work is presented as a proof-of-concept that demonstrates the feasibility of using Lola for complex diagnostic tasks, offering a theoretical foundation for future practical applications in safety-critical systems.