Foundations for Runtime Monitoring

  • Date February 12, 2018
  • Hour 5 pm
  • Room GSSI Main Lecture Hall
  • Speaker Adrian Francalanza (University of Malta)


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, nor is it clear which monitors effect the required runtime analysis correctly. In this tutorial, we strive towards a foundational understanding of these questions. This enables us to distill core concepts that can be extrapolated to various runtime verification settings. Particularly, we consider a specification logic that is agnostic of the verification method used, and is general enough to embed commonly used specification logics. We 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. We show how this correspondence is used to identify which subsets of the logic can be adequately monitored for. The monitoring framework also serves as a basis for defining various notions of monitor correctness. In this exposition we shall assume no prior knowledge of the specification logic and the monitoring framework considered.