Runtime verification

Runtime verification is the discipline of checking whether the observed execution of a system satisfies a formal specification. Unlike static techniques such as model checking or theorem proving, which analyze a model of the system before deployment, runtime verification monitors the actual behavior of a running system against a specification expressed in temporal logic or similar formalisms. It trades the completeness of exhaustive analysis for the scalability of observing only what actually happens, making it indispensable for large distributed systems and cyber-physical systems where static analysis is intractable.

The central challenge in runtime verification is monitor synthesis: automatically generating an efficient monitor from a formal specification. A monitor must detect property violations in real time, often under strict memory and latency constraints, and must handle the gap between the abstract specification and the concrete observables of the system. The field also touches on runtime enforcement, where the monitor not only detects violations but actively prevents them by modifying system behavior.

Runtime verification is not a lesser cousin of static verification. It is a distinct paradigm that acknowledges a fundamental truth: some systems are too complex to model exhaustively, and for these systems, observation is the only honest form of analysis.