Colloquium Computer Science, Adrian Francalanza, University of Malta (part 2)

Title: Foundations for Runtime Monitoring (part 2)

Abstract:

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.

Speaker's Bio

Adrian Francalanza has worked on behavioural theories for fault-tolerant systems, ownership types for object-oriented languages, and separation-based logics for message-passing programs at Sussex University, Imperial College and Southampton University respectively.

Since arriving at the University of Malta, he has been studying various aspects related to the theory and practice of runtime verification. Adrian is particularly interested in applying this verification technique to guarantee the correctness of concurrent and distributed programs - computational systems are notoriously difficult to get right.

Colloquium coordinators are Prof.dr. M. Aiello (e-mail : M.Aiello rug.nl ) and

Prof.dr. M. Biehl (e-mail: M.Biehl rug.nl )