Incrementally Predictive Runtime Verification

Ferrando, A ORCID: 0000-0002-8711-4670 and Delzanno, G ORCID: 0000-0001-7030-1050
(2021) Incrementally Predictive Runtime Verification. .

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


Runtime Verification is a lightweight formal verification technique used to verify the runtime behaviour of software (resp. hardware) systems. Given a formal property, one or more monitors are synthesised to verify the latter against a system execution. A monitor can only conclude the violation of a property when it observes such a violation. Unfortunately, in safety-critical scenarios, this might happen too late for the system to react properly. In such scenarios, it is advised to use Predictive Runtime Verification, where monitors are capable of anticipating (by using a model of the system) future events before actually observing them. In this work, instead of assuming such a model is given, we describe a runtime verification workflow where the model is learnt and incrementally refined by using process mining techniques. We present the approach and the resulting prototype tool.

Item Type: Conference or Workshop Item (Unspecified)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 25 May 2022 13:40
Last Modified: 18 Jan 2023 21:01
Open Access URL: