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

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.

Access the full-text of this item by clicking on the Open Access link.

Official URL: http://dx.doi.org/10.1007/s10703-022-00395-7

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:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3163858