Bridging the gap between single- and multi-model predictive runtime verification
Journal article
Authors | Angelo Ferrando, Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Fabio Papacchini, Michael Fisher and Viviana Mascardi |
---|---|
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. |
Keywords | Predictive Runtime Verification (PRV) paradigm; Mars Curiosity rover simulation; Multi-Model PRV |
Year | 2022 |
Journal | Formal Methods in System Design |
Journal citation | 59, p. 44–76 |
Publisher | Springer |
ISSN | 0925-9856 |
1572-8102 | |
Digital Object Identifier (DOI) | https://doi.org/10.1007/s10703-022-00395-7 |
Web address (URL) | http://dx.doi.org/10.1007/s10703-022-00395-7 |
Output status | Published |
Publication dates | 18 Aug 2022 |
Publication process dates | |
Accepted | 05 Jul 2022 |
Deposited | 31 Jan 2023 |
https://repository.derby.ac.uk/item/9w939/bridging-the-gap-between-single-and-multi-model-predictive-runtime-verification
19
total views0
total downloads0
views this month0
downloads this month