Ferrando, Angelo ORCID: 0000-0002-8711-4670, Cardoso, Rafael C, Farrell, Marie, Luckcuck, Matt ORCID: 0000-0002-6444-9312, Papacchini, Fabio, Fisher, Michael and Mascardi, Viviana
(2021)
Bridging the gap between single- and multi-model predictive runtime verification.
FORMAL METHODS IN SYSTEM DESIGN, 59 (1-3).
pp. 44-76.
Abstract
<jats:title>Abstract</jats:title><jats:p>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 <jats:italic>Multi-Model</jats:italic> 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 <jats:italic>centralised</jats:italic> or a <jats:italic>compositional</jats:italic> 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.</jats:p>
Item Type: | Article |
---|---|
Uncontrolled Keywords: | Runtime verification, Predictive runtime verification, Multi-model, Robotics |
Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
Depositing User: | Symplectic Admin |
Date Deposited: | 08 Sep 2022 09:07 |
Last Modified: | 22 Nov 2023 11:36 |
DOI: | 10.1007/s10703-022-00395-7 |
Open Access URL: | https://doi.org/10.1007/s10703-022-00395-7 |
Related URLs: | |
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3163858 |