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

Angelo Ferrando; Rafael C. Cardoso; Marie Farrell; Matt Luckcuck; Fabio Papacchini; Michael Fisher; Viviana Mascardi

doi:10.1007/s10703-022-00395-7

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

Angelo Ferrando^* (Corresponding Author)
, Rafael C. Cardoso
, Marie Farrell
, Matt Luckcuck
, Fabio Papacchini
, Michael Fisher
, Viviana Mascardi

^*Corresponding author for this work

University of Genoa
Maynooth University
University of Manchester
Lancaster University Leipzig

Research output: Contribution to journal › Article › peer-review

6 Citations (Scopus)

5 Downloads (Pure)

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.

Original language	English
Pages (from-to)	44-76
Number of pages	33
Journal	Formal Methods in System Design
Volume	59
Issue number	1-3
Early online date	18 Aug 2022
DOIs	https://doi.org/10.1007/s10703-022-00395-7
Publication status	Published - 18 Aug 2022

Bibliographical note

Funding Information:
Open access funding provided by Università degli Studi di Genova within the CRUI-CARE Agreement. Research at Manchester was supported by both the Royal Academy of Engineering, under the Chairs in Emerging Technologies scheme, and the UKRI’s TAS Node in Verifiability (EP/V026801).

Data Availability Statement

Data availability: Not applicable.

Code availability: The GitHub repository containing the implementation of the tool is publicly available at https://github.com/AngeloFerrando/MultiModelPredictiveRuntimeVerifcation.

Funding

Open access funding provided by Università degli Studi di Genova within the CRUI-CARE Agreement. Research at Manchester was supported by both the Royal Academy of Engineering, under the Chairs in Emerging Technologies scheme, and the UKRI’s TAS Node in Verifiability (EP/V026801).

Keywords

Multi-model
Predictive runtime verification
Robotics
Runtime verification

Access to Document

10.1007/s10703-022-00395-7Licence: CC BY

Ferrando_etal_FMSD_Bridging_The_Gap_VoR
This article is licensed under a Creative Commons Attribution International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Final published version, 2 MBLicence: CC BY

Cite this

@article{ca619c25ae504e74a2a6b35ad6902d72,

title = "Bridging the gap between single- and multi-model predictive runtime verification",

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 = "Multi-model, Predictive runtime verification, Robotics, Runtime verification",

author = "Angelo Ferrando and Cardoso, \{Rafael C.\} and Marie Farrell and Matt Luckcuck and Fabio Papacchini and Michael Fisher and Viviana Mascardi",

note = "Funding Information: Open access funding provided by Universit{\`a} degli Studi di Genova within the CRUI-CARE Agreement. Research at Manchester was supported by both the Royal Academy of Engineering, under the Chairs in Emerging Technologies scheme, and the UKRI{\textquoteright}s TAS Node in Verifiability (EP/V026801). ",

year = "2022",

month = aug,

day = "18",

doi = "10.1007/s10703-022-00395-7",

language = "English",

volume = "59",

pages = "44--76",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "1-3",

}

TY - JOUR

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

AU - Ferrando, Angelo

AU - Cardoso, Rafael C.

AU - Farrell, Marie

AU - Luckcuck, Matt

AU - Papacchini, Fabio

AU - Fisher, Michael

AU - Mascardi, Viviana

N1 - Funding Information: Open access funding provided by Università degli Studi di Genova within the CRUI-CARE Agreement. Research at Manchester was supported by both the Royal Academy of Engineering, under the Chairs in Emerging Technologies scheme, and the UKRI’s TAS Node in Verifiability (EP/V026801).

PY - 2022/8/18

Y1 - 2022/8/18

N2 - 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.

AB - 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.

KW - Multi-model

KW - Predictive runtime verification

KW - Robotics

KW - Runtime verification

UR - https://www.scopus.com/pages/publications/85137231245

U2 - 10.1007/s10703-022-00395-7

DO - 10.1007/s10703-022-00395-7

M3 - Article

AN - SCOPUS:85137231245

SN - 0925-9856

VL - 59

SP - 44

EP - 76

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 1-3

ER -

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

Abstract

Bibliographical note

Data Availability Statement

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this