This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.

Bridging the gap between single- and multi-model predictive runtime verification / Ferrando, Angelo; Cardoso, Rafael C.; Farrell, Marie; Luckcuck, Matt; Papacchini, Fabio; Fisher, Michael; Mascardi, Viviana. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 59:1-3(2021), pp. 44-76. [10.1007/s10703-022-00395-7]

Bridging the gap between single- and multi-model predictive runtime verification

Angelo Ferrando;
2021

Abstract

This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.
2021
59
1-3
44
76
Bridging the gap between single- and multi-model predictive runtime verification / Ferrando, Angelo; Cardoso, Rafael C.; Farrell, Marie; Luckcuck, Matt; Papacchini, Fabio; Fisher, Michael; Mascardi, Viviana. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 59:1-3(2021), pp. 44-76. [10.1007/s10703-022-00395-7]
Ferrando, Angelo; Cardoso, Rafael C.; Farrell, Marie; Luckcuck, Matt; Papacchini, Fabio; Fisher, Michael; Mascardi, Viviana
File in questo prodotto:
Non ci sono file associati a questo prodotto.
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/1331883
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact