Home > Research > Publications & Outputs > Bridging the gap between single- and multi-mode...


Text available via DOI:

View graph of relations

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

Research output: Contribution to Journal/MagazineJournal articlepeer-review

  • A. Ferrando
  • R.C. Cardoso
  • M. Farrell
  • M. Luckcuck
  • F. Papacchini
  • M. Fisher
  • V. Mascardi
<mark>Journal publication date</mark>18/08/2022
<mark>Journal</mark>Formal Methods in System Design
Issue number1-3
Number of pages33
Pages (from-to)44-76
Publication StatusPublished
Early online date18/08/22
<mark>Original language</mark>English


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.