Runtime Verification is a lightweight formal verification technique used to verify whether a system behaves as expected at runtime. Expected behaviour is typically formally specified using properties, which are used to automatically synthesise monitors. Properties that can be verified at runtime by a monitor are called monitorable, while those that cannot are termed non-monitorable. In this paper, we revisit the notion of monitorability and demonstrate how non-monitorable properties can still be used to generate partial monitors. We tackle this from two different perspectives: (i) by recognising that a monitor can give up on monitoring the property under analysis if it recognises that the monitoring will never conclude the satisfaction or violation of the property; (ii) by recognising that a monitor can give up on events that are not necessary for successful monitoring of the property under analysis. By considering these two aspects, we present how to achieve partial monitoring of Linear Temporal Logic properties by building upon the standard monitor construction. Finally, we present a prototype implementation of our approach and its application to a remote inspection case study, as well as a set of evaluation experiments to stress test our approach using synthetic properties.

Towards partial monitoring: Never too early to give in / Ferrando, Angelo; Cardoso, Rafael C.. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 240:(2025), pp. 1-42. [10.1016/j.scico.2024.103220]

Towards partial monitoring: Never too early to give in

Angelo Ferrando;
2025

Abstract

Runtime Verification is a lightweight formal verification technique used to verify whether a system behaves as expected at runtime. Expected behaviour is typically formally specified using properties, which are used to automatically synthesise monitors. Properties that can be verified at runtime by a monitor are called monitorable, while those that cannot are termed non-monitorable. In this paper, we revisit the notion of monitorability and demonstrate how non-monitorable properties can still be used to generate partial monitors. We tackle this from two different perspectives: (i) by recognising that a monitor can give up on monitoring the property under analysis if it recognises that the monitoring will never conclude the satisfaction or violation of the property; (ii) by recognising that a monitor can give up on events that are not necessary for successful monitoring of the property under analysis. By considering these two aspects, we present how to achieve partial monitoring of Linear Temporal Logic properties by building upon the standard monitor construction. Finally, we present a prototype implementation of our approach and its application to a remote inspection case study, as well as a set of evaluation experiments to stress test our approach using synthetic properties.
2025
17-ott-2024
240
1
42
Towards partial monitoring: Never too early to give in / Ferrando, Angelo; Cardoso, Rafael C.. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 240:(2025), pp. 1-42. [10.1016/j.scico.2024.103220]
Ferrando, Angelo; Cardoso, Rafael C.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0167642324001436-main.pdf

Open access

Tipologia: VOR - Versione pubblicata dall'editore
Dimensione 1.03 MB
Formato Adobe PDF
1.03 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1361526
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact