Runtime Verification
Definition
Runtime verification checks whether an execution trace satisfies a specification while the system is running or after the trace has been produced.
Why It Matters
It offers a pragmatic middle ground between full formal verification and purely empirical testing, especially when systems are complex, learned, or partially unknown.
Formalism / Key Objects
- execution traces
- monitors
- specifications, often temporal or automata-based
- verdicts such as satisfaction, violation, or inconclusive status
- finite bad prefixes for safety properties
Connections
- Closely linked to Linear Temporal Logic as a source of specifications.
- Safety and Co-Safety Properties explains why runtime monitors can conclusively detect some violations or satisfactions after finite traces.
- Adjacent to Shielding because both depend on detecting unsafe trajectory prefixes.
- A core subfield inside Formal Methods.
- Adjacent to Probabilistic Model Checking: model checking verifies modeled behavior ahead of time, while runtime verification monitors realized traces.
Common Confusions
- Runtime verification is narrower than full verification.
- Monitoring a trace does not by itself prevent unsafe behavior unless coupled to intervention.