Colloquium J. Morgenstern - Luca Aceto (Univ. Reykajavik) - 10/09 - 11h - Inria - Sophia Antipolis

Inria, site de Sophia Antipolis - Amphithéâtre - Bâtiment Kahn

Luca Aceto(Univ. Reykajavik)

"Theoretical Foundations for Runtime Monitoring"

Résumé / 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 my collaborators in the project Theoretical Foundations for Monitorability.

La présentation sera faite en anglais.

Retrouvez l'intégralité du programme de l'année sur le site du colloquium