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

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

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

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Bridging the gap between single- and multi-model predictive runtime verification. / Ferrando, A.; Cardoso, R.C.; Farrell, M. et al.
In: Formal Methods in System Design, Vol. 59, No. 1-3, 18.08.2022, p. 44-76.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Ferrando, A, Cardoso, RC, Farrell, M, Luckcuck, M, Papacchini, F, Fisher, M & Mascardi, V 2022, 'Bridging the gap between single- and multi-model predictive runtime verification', Formal Methods in System Design, vol. 59, no. 1-3, pp. 44-76. https://doi.org/10.1007/s10703-022-00395-7

APA

Ferrando, A., Cardoso, R. C., Farrell, M., Luckcuck, M., Papacchini, F., Fisher, M., & Mascardi, V. (2022). Bridging the gap between single- and multi-model predictive runtime verification. Formal Methods in System Design, 59(1-3), 44-76. https://doi.org/10.1007/s10703-022-00395-7

Vancouver

Ferrando A, Cardoso RC, Farrell M, Luckcuck M, Papacchini F, Fisher M et al. Bridging the gap between single- and multi-model predictive runtime verification. Formal Methods in System Design. 2022 Aug 18;59(1-3):44-76. Epub 2022 Aug 18. doi: 10.1007/s10703-022-00395-7

Author

Ferrando, A. ; Cardoso, R.C. ; Farrell, M. et al. / Bridging the gap between single- and multi-model predictive runtime verification. In: Formal Methods in System Design. 2022 ; Vol. 59, No. 1-3. pp. 44-76.

Bibtex

@article{12fc5347e7464c7da0926101cf73220e,
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, Formal modeling, Model predictive, Multi-modelling, Multiple-modeling, Node-based, Property-based, Run-time verification, Single models",
author = "A. Ferrando and R.C. Cardoso and M. Farrell and M. Luckcuck and F. Papacchini and M. Fisher and V. Mascardi",
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",
number = "1-3",

}

RIS

TY - JOUR

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

AU - Ferrando, A.

AU - Cardoso, R.C.

AU - Farrell, M.

AU - Luckcuck, M.

AU - Papacchini, F.

AU - Fisher, M.

AU - Mascardi, V.

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

KW - Formal modeling

KW - Model predictive

KW - Multi-modelling

KW - Multiple-modeling

KW - Node-based

KW - Property-based

KW - Run-time verification

KW - Single models

U2 - 10.1007/s10703-022-00395-7

DO - 10.1007/s10703-022-00395-7

M3 - Journal article

VL - 59

SP - 44

EP - 76

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 1-3

ER -