Seminar by Luca Aceto

SCHEDULE: 21th Nov 2017, 14:30, Room B

SPEAKER: Luca Aceto (GSSI and School of Computer Science, Reykjavik University)

TITLE: Theoretical Foundations for Runtime Monitoring

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, 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. In this talk, I will assume no prior knowledge of runtime verification.

The talk is based on joint work with Antonis Achilleos (Reykjavik University), Duncan Paul Attard (University of Malta), Ian Cassar (University of Malta), Adrian Francalanza (University of Malta) and Anna Ingólfsdóttir ((Reykjavik University), carried out within the framework of the project “Theoretical Foundations for Monitorability” (http://icetcs.ru.is/theofomon/).