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 | |
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.
Keywords
- Multi-model
- Predictive runtime verification
- Robotics
- Runtime verification