Abstract: The idea of runtime verification is to observe the executions of a system in order to derive information on its behaviour. By analysing executions rather than the system itself, it avoids the state-explosion problem associated with exhaustive verification techniques such as model-checking.
The cost of lower complexity is limited expressivity: while model-checking will always provide a definite answer to the question “does the system satisfy the specification”, runtime verification provides no such firm guarantees. However, depending on the specification, runtime verification can provide a range of weaker guarantees. Understanding the trade-offs between the complexity of specifications and the power of runtime verification is at the heart of this course.

The content in these slides was presented during the BehAPI 2019 Summer School in Leicester.