Theoretical Foundations for Runtime Monitoring

Runtime Verification is a lightweight technique that complements other verification methods in a multi-pronged approach towards ensuring software correctness. The technique poses novel questions to software engineers: it is not easy to see which specifications are amenable to runtime monitoring, and it is not clear which monitors perform the required runtime analysis correctly. In this talk, I will present a theoretical framework that can be used to provide answers to those questions. Our approach uses the classic Hennessy-Milner with recursion as a specification logic that is agnostic of the adopted verification method and is general enough to embed commonly used specification logics. I also present an operational semantics for an elemental framework that describes the runtime analysis carried out by monitors. This allows us to establish a correspondence between the property satisfactions in the logic and the verdicts reached by the monitors carrying out the analysis. I will show how this correspondence is used to identify which subsets of the logic can be adequately monitored for, to study the power of deterministic monitors and to define various notions of monitor correctness. I will also discuss very recent work on the relationships between runtime monitorability in a branching-time and in a linear-time setting. The talk will assume no prior knowledge of runtime verification. It is based on joint work with Antonis Achilleos (Reykjavik University), Duncan Paul Attard (University of Malta and Reykjavik University), Ian Cassar (University of Malta and Reykjavik University), Adrian Francalanza (University of Malta), Anna Ingólfsdóttir (Reykjavik University) and Karoliina Lehtinen (Christian-Albrechts University of Kiel), carried out within the framework of the project "Theoretical Foundations for Monitorability" (http://icetcs.ru.is/theofomon/).