A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA
For developers of safety-critical systems, this work integrates two traditionally separate tasks into a single formalism, but the approach is incremental.
The paper presents a unified framework combining runtime verification and model-based diagnosis in LOLA, enabling continuous online fault localization alongside detection without separate toolchains.
We present an integrated framework that unifies runtime verification and model-based diagnosis within the stream specification language LOLA. By encoding system descriptions, component health states, and observations into a single stream-based formalism, the approach enables continuous, online fault localization directly alongside fault detection, without requiring separate toolchains. The framework supports both time-invariant and transient faults, and naturally accommodates nondeterministic observations.