Informations pratiques sur cette ressource

Description de la ressource pédagogique

Description (résumé)

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

"Domaine(s)" et indice(s) Dewey

• logique symbolique (164)