A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness pro...

Descripción completa

Detalles Bibliográficos
Autores principales: Basin, David, Dardinier, Thibault, Heimes, Lukas, Krstić, Srđan, Raszyk, Martin, Schneider, Joshua, Traytel, Dmitriy
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324294/
http://dx.doi.org/10.1007/978-3-030-51074-9_25
Descripción
Sumario:Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.

Ejemplares similares