Verified First-Order Monitoring with Recursive Rules
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Dokumenter
- Fulltext
Forlagets udgivne version, 442 KB, PDF-dokument
First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.
Originalsprog | Engelsk |
---|---|
Titel | Tools and Algorithms for the Construction and Analysis of Systems : 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings |
Redaktører | Dana Fisman, Grigore Rosu |
Vol/bind | 2 |
Forlag | Springer |
Publikationsdato | 2022 |
Sider | 236-253 |
ISBN (Trykt) | 9783030995263 |
DOI | |
Status | Udgivet - 2022 |
Begivenhed | 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022 - Munich, Tyskland Varighed: 2 apr. 2022 → 7 apr. 2022 |
Konference
Konference | 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022 |
---|---|
Land | Tyskland |
By | Munich |
Periode | 02/04/2022 → 07/04/2022 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 13244 LNCS |
ISSN | 0302-9743 |
Bibliografisk note
Funding Information:
Acknowledgments We thank David Basin for supporting this work and the anonymous TACAS reviewers for their helpful comments. Dmitriy Traytel is supported by a Novo Nordisk Fonden Start Package Grant (NNF20OC0063462).
Publisher Copyright:
© 2022, The Author(s).
ID: 307749350