Erschienen:
Springer International Publishing, 2022
Erschienen in:
Tools and Algorithms for the Construction and Analysis of Systems (2022), Seite 236-253
Sprache:
Nicht zu entscheiden
DOI:
10.1007/978-3-030-99527-0_13
ISBN:
9783030995263;
9783030995270
ISSN:
1611-3349;
0302-9743
Entstehung:
Anmerkungen:
Beschreibung:
AbstractFirst-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.