We present HyperMonitor a Python prototype of a novel runtime verification method specifically designed for predicting race conditions in multithread programs. Our procedure is based on the combination of Inductive Process Mining, Petri Net Tranformations, and verification algorithms. More specifically, given a trace log, the Hyper Predictive Runtime Verifier (HPRV) procedure first exploits Inductive Process Mining to build a Petri Net that captures all traces in the log, and then applies semantic-driven transformations to increase the number of concurrent threads without re-executing the program. In this paper, we present the key ideas of our approach, details on the HyperMonitor implementation and discuss some preliminary results obtained on classical examples of concurrent C programs with semaphors.
HyperMonitor: {A} Python Prototype for Hyper Predictive Runtime Verification / Ferrando, Angelo; Delzanno, Giorgio. - 14235 LNCS:(2023), pp. 171-182. (Intervento presentato al convegno 17th International Conference on Reachability Problems, RP 2023 tenutosi a Nice, fra nel 11-13 October 2023) [10.1007/978-3-031-45286-4_13].
HyperMonitor: {A} Python Prototype for Hyper Predictive Runtime Verification
Angelo Ferrando;
2023
Abstract
We present HyperMonitor a Python prototype of a novel runtime verification method specifically designed for predicting race conditions in multithread programs. Our procedure is based on the combination of Inductive Process Mining, Petri Net Tranformations, and verification algorithms. More specifically, given a trace log, the Hyper Predictive Runtime Verifier (HPRV) procedure first exploits Inductive Process Mining to build a Petri Net that captures all traces in the log, and then applies semantic-driven transformations to increase the number of concurrent threads without re-executing the program. In this paper, we present the key ideas of our approach, details on the HyperMonitor implementation and discuss some preliminary results obtained on classical examples of concurrent C programs with semaphors.
Pubblicazioni consigliate
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris
