Verified First-Order Monitoring with Recursive Rules
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Fulltext
Final published version, 442 KB, PDF document
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.
Original language | English |
---|---|
Title of host publication | 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 |
Editors | Dana Fisman, Grigore Rosu |
Volume | 2 |
Publisher | Springer |
Publication date | 2022 |
Pages | 236-253 |
ISBN (Print) | 9783030995263 |
DOIs | |
Publication status | Published - 2022 |
Event | 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, Germany Duration: 2 Apr 2022 → 7 Apr 2022 |
Conference
Conference | 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 | Germany |
By | Munich |
Periode | 02/04/2022 → 07/04/2022 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 13244 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:
© 2022, The Author(s).
- Formal verification, Monitoring, Rule-based specifications
Research areas
ID: 307749350