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
_version_ 1783551910376112128
author Basin, David
Dardinier, Thibault
Heimes, Lukas
Krstić, Srđan
Raszyk, Martin
Schneider, Joshua
Traytel, Dmitriy
author_facet Basin, David
Dardinier, Thibault
Heimes, Lukas
Krstić, Srđan
Raszyk, Martin
Schneider, Joshua
Traytel, Dmitriy
author_sort Basin, David
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324294
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242942020-06-30 A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic Basin, David Dardinier, Thibault Heimes, Lukas Krstić, Srđan Raszyk, Martin Schneider, Joshua Traytel, Dmitriy Automated Reasoning Article 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. 2020-05-30 /pmc/articles/PMC7324294/ http://dx.doi.org/10.1007/978-3-030-51074-9_25 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Basin, David
Dardinier, Thibault
Heimes, Lukas
Krstić, Srđan
Raszyk, Martin
Schneider, Joshua
Traytel, Dmitriy
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title_full A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title_fullStr A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title_full_unstemmed A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title_short A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
title_sort formally verified, optimized monitor for metric first-order dynamic logic
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324294/
http://dx.doi.org/10.1007/978-3-030-51074-9_25
work_keys_str_mv AT basindavid aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT dardinierthibault aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT heimeslukas aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT krsticsrđan aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT raszykmartin aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT schneiderjoshua aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT trayteldmitriy aformallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT basindavid formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT dardinierthibault formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT heimeslukas formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT krsticsrđan formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT raszykmartin formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT schneiderjoshua formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic
AT trayteldmitriy formallyverifiedoptimizedmonitorformetricfirstorderdynamiclogic

Ejemplares similares