Colloquium Jacques Morgenstern
Colloquium : Theoretical Foundations for Runtime Monitoring
Luca Aceto, professeur à l'université de Reykjavik, présentera le 10 septembre 2019 ses travaux lors du prochain colloquium J. Morgenstern : "Theoretical Foundations for Runtime Monitoring"
- Date : 10/09/2019
- Lieu : Inria, Sophia Antipolis, Amphithéâtre, Bâtiment Kahn
- Intervenant(s) : Luca Aceto, Université de Reykjavik
- Organisateur(s) : Comité Colloquium Jacques Morgenstern
Titre, résumé et présentation sont exclusivement en anglais.
Runtime monitoring/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. I will view monitorability as a spectrum: the fewer monitor guarantees are required, the more properties become monitorable. I will then present a monitorability hierarchy and provide operational characterisations for its levels. Existing monitorability definitions are mapped into the proposed hierarchy, providing a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.
The talk is based on joint work with my collaborators in the project "Theoretical Foundations for Monitorability" (http://icetcs.ru.is/theofomon/).