Runtime Verification: Monitoring, Knowledge, and Uncertainty (Lecture Notes)

TL;DR

This paper discusses runtime verification as a lightweight, observation-based approach to system monitoring, emphasizing its theoretical foundations, specification formalisms, and challenges in real-time settings.

Contribution

It provides a comprehensive overview of automata-theoretic, temporal, and epistemic foundations of runtime verification, including methods for monitor construction and handling uncertainty.

Findings

Introduces formal foundations for runtime verification techniques.

Explains how offline analysis aids in online monitor construction.

Discusses timed extensions and real-time challenges in runtime verification.

Abstract

Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model in advance. It is particularly useful for partially observable or black-box systems, where uncertainty can only be resolved through observation. These lecture notes present automata-theoretic, temporal-logical, and epistemic foundations of runtime verification. They cover specification formalisms, diagnosis, opacity, and monitorability, and explain how offline analysis can be used to construct monitors that operate online on observed executions. The notes also discuss timed extensions and the additional algorithmic and semantic challenges that arise in the real-time setting.