HyperMonitor: A Python Prototype for Hyper Predictive Runtime Verification
Pages 171 - 182
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.
References
[1]
Augusto A et al. Automated discovery of process models from event logs: review and benchmark IEEE Trans. Knowl. Data Eng. 2019 31 4 686-705
[2]
Bartocci E, Falcone Y, Francalanza A, and Reger G Bartocci E and Falcone Y Introduction to runtime verification Lectures on Runtime Verification 2018 Cham Springer 1-33
[3]
Cheng A, Esparza J, and Palsberg J Shyamasundar RK Complexity results for 1-safe nets Foundations of Software Technology and Theoretical Computer Science 1993 Heidelberg Springer 326-337
[4]
Clarke EM Ramesh S and Sivakumar G Model checking Foundations of Software Technology and Theoretical Computer Science 1997 Heidelberg Springer 54-56
[5]
Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D.A., Kalus, G. (eds.) Engineering Dependable Software Systems. NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 34, pp. 141–175. IOS Press (2013)
[6]
Ferrando, A., Delzanno, G.: Incrementally predictive runtime verification. In: Monica, S., Bergenti, F. (eds.) Proceedings of the 36th Italian Conference on Computational Logic. CEUR Workshop Proceedings, Parma, Italy, 7–9 September 2021, vol. 3002, pp. 92–106. CEUR-WS.org (2021)
[7]
Havelund K Havelund K, Penix J, and Visser W Using runtime analysis to guide model checking of Java programs SPIN Model Checking and Software Verification 2000 Heidelberg Springer 245-264
[8]
Havelund K and Rosu G An overview of the runtime verification tool Java pathexplorer Formal Meth. Syst. Des. 2004 24 2 189-215
[9]
Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09–11 June 2014, pp. 337–348. ACM (2014).
[10]
Leemans SJJ, Fahland D, and van der Aalst WMP Colom J-M and Desel J Discovering block-structured process models from event logs - a constructive approach Application and Theory of Petri Nets and Concurrency 2013 Heidelberg Springer 311-329
[11]
Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science, vol. 6. North-Holland (1978)
[12]
Pinisetty S, Jéron T, Tripakis S, Falcone Y, Marchand H, and Preoteasa V Predictive runtime verification of timed properties J. Syst. Softw. 2017 132 353-365
[13]
Qadeer S and Rehof J Halbwachs N and Zuck LD Context-bounded model checking of concurrent software Tools and Algorithms for the Construction and Analysis of Systems 2005 Heidelberg Springer 93-107
[14]
Savage S, Burrows M, Nelson G, Sobalvarro P, and Anderson TE Eraser: a dynamic data race detector for multithreaded programs ACM Trans. Comput. Syst. 1997 15 4 391-411
[15]
Şerbănuţă TF, Chen F, and Roşu G Qadeer S and Tasiran S Maximal causal models for sequentially consistent systems Runtime Verification 2013 Heidelberg Springer 136-150
[16]
Zhang X, Leucker M, and Dong W Goodloe AE and Person S Runtime verification with predictive semantics NASA Formal Methods 2012 Heidelberg Springer 418-432
Recommendations
Verification of Concurrent Programs Using Petri Net Unfoldings
Verification, Model Checking, and Abstract InterpretationAbstractGiven a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be ...
Soter: an automatic safety verifier for erlang
AGERE! 2012: Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractionsThis paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic and ...
Runtime verification of concurrency-specific correctness criteria
We give an overview of correctness criteria specific to concurrent shared-memory programs and runtime verification techniques for verifying these criteria. We cover a spectrum of criteria, from ones focusing on low-level thread interference such as ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Oct 2023
230 pages
ISBN:978-3-031-45285-7
DOI:10.1007/978-3-031-45286-4
- Editors:
- Olivier Bournez,
- Enrico Formenti,
- Igor Potapov
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2023.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 11 October 2023
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 27 Dec 2024