Article

Residual Runtime Verification via Reachability Analysis

Authors:

Chukri Soueidi,

Yliès FalconeAuthors Info & Claims

Verified Software. Theories, Tools and Experiments.: 14th International Conference, VSTTE 2022, Trento, Italy, October 17–18, 2022, Revised Selected Papers

Pages 148 - 166

https://doi.org/10.1007/978-3-031-25803-9_9

Published: 01 February 2023 Publication History

Abstract

We leverage static verification to reduce monitoring overhead when runtime verifying a property. We present a sound and efficient analysis to statically find safe execution paths in the control flow at the intra-procedural level of programs. Such paths are guaranteed to preserve the monitored property and thus can be ignored at runtime. Our analysis guides an instrumentation tool to select program points that should be observed at runtime. The monitor is left to perform residual runtime verification for parts of the program that the analysis could not statically prove safe. Our approach does not depend on dataflow analysis, thus separating the task of residual analysis from static analysis; allowing for seamless integration with many RV frameworks and development pipelines. We implement our approach within BISM, which is a recent tool for bytecode-level instrumentation of Java programs. Our experiments on the DaCapo benchmark show a reduction in instrumentation points by a factor of 2.5 on average (reaching 9), and accordingly, a reduction in the number of runtime events by a factor of 1.8 on average (reaching 6).

References

[1]

Ahrendt W, Beckert B, Hähnle R, Rümmer P, and Schmitt PH de Boer FS, Bonsangue MM, Graf S, and de Roever W-P Verifying object-oriented programs with key: a tutorial Formal Methods for Components and Objects 2007 Heidelberg Springer 70-101

[2]

Ahrendt W, Pace GJ, and Schneider G Margaria T and Steffen B A unified approach for static and runtime verification: framework and applications Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change 2012 Heidelberg Springer 312-326

[3]

Avgustinov, P., et al.: ABC: an extensible AspectJ compiler. In: Proceedings of the 4th International Conference on Aspect-Oriented Software Development, AOSD 2005, pp. 87–98. Association for Computing Machinery, New York (2005).

[4]

Azzopardi, S., Colombo, C., Pace, G.: Clarva: model-based residual verification of java programs. In: Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD, pp. 352–359. INSTICC, SciTePress (2020).

[5]

Barringer H, Falcone Y, Havelund K, Reger G, and Rydeheard D Giannakopoulou D and Méry D Quantified event automata: towards expressive and efficient runtime monitors FM 2012: Formal Methods 2012 Heidelberg Springer 68-84

[6]

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

[7]

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011).

[8]

Blackburn, S.M., et al.: The DaCapo benchmarks: Java benchmarking development and analysis. SIGPLAN Not. 41(10), 169–190 (2006).

[9]

Bodden E, Lam P, Hendren L, et al. Barringer H et al. Clara: a framework for partially evaluating finite-state runtime monitors ahead of time Runtime Verification 2010 Heidelberg Springer 183-197

[10]

Bodden, E., Lam, P., Hendren, L.J.: Partially evaluating finite-state runtime monitors ahead of time. ACM Trans. Program. Lang. Syst. 34(2), 7:1–7:52 (2012).

[11]

Chen F and Roşu G Kowalewski S and Philippou A Parametric trace slicing and monitoring Tools and Algorithms for the Construction and Analysis of Systems 2009 Heidelberg Springer 246-261

[12]

Chimento JM, Ahrendt W, Pace GJ, and Schneider G Bartocci E and Majumdar R StaRVOOrS: a tool for combined static and runtime verification of Java Runtime Verification 2015 Cham Springer 297-305

[13]

Chimento, J.M., Ahrendt, W., Schneider, G.: Testing meets static and runtime verification. In: Proceedings of the 6th Conference on Formal Methods in Software Engineering, FormaliSE 2018, pp. 30–39. Association for Computing Machinery, New York (2018).

[14]

Choi JD, Gupta M, Serrano M, Sreedhar VC, and Midkiff S Escape analysis for Java SIGPLAN Not. 1999 34 10 1-19

[15]

Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis exploiting static analysis, p. 124 (2007)

[16]

Falcone Y, Fernandez J, and Mounier L What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 2012 14 3 349-382

[17]

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).

[18]

Falcone Y, Krstić S, Reger G, and Traytel D A taxonomy for classifying runtime verification tools Int. J. Softw. Tools Technol. Transfer 2021 23 2 255-284

[19]

Havelund K and Goldberg A Meyer B and Woodcock J Verify your runs Verified Software: Theories, Tools, Experiments 2008 Heidelberg Springer 374-383

[20]

Havelund K, Reger G, Thoma D, and Zălinescu E Bartocci E and Falcone Y Monitoring events that carry data Lectures on Runtime Verification 2018 Cham Springer 61-102

[21]

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley Longman Publishing Co., Inc. (2006)

[22]

Jakse, R., Falcone, Y., Méhaut, J., Pouget, K.: Interactive runtime verification - when interactive debugging meets runtime verification. In: 28th IEEE International Symposium on Software Reliability Engineering, ISSRE 2017, Toulouse, France, 23–26 October 2017, pp. 182–193. IEEE Computer Society (2017).

[23]

Karandikar P, Niewerth M, and Schnoebelen P On the state complexity of closures and interiors of regular languages with subwords and superwords Theoret. Comput. Sci. 2016 610 91-107

[24]

Kupferman O and Vardi MY Model checking of safety properties Formal Methods Syst. Des. 2001 19 3 291-314

[25]

Leucker M Qadeer S and Tasiran S Sliding between model checking and runtime verification Runtime Verification 2013 Heidelberg Springer 82-87

[26]

Leucker M and Schallhart C A brief account of runtime verification J. Logic Algebraic Program. 2009 78 5 293-303

[27]

Sánchez C et al. A survey of challenges for runtime verification from advanced application domains (beyond software) Formal Methods Syst. Des. 2019 54 3 279-335

[28]

Soueidi, C., Falcone, Y.: Capturing program models with BISM. In: Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022, pp. 1857–1861. Association for Computing Machinery, New York (2022).

[29]

Soueidi, C., Kassem, A., Falcone, Y.: BISM: Bytecode-Level Instrumentation for Software Monitoring. https://gitlab.inria.fr/monitoring/bism-tool

[30]

Strom RE and Yemini S Typestate: a programming language concept for enhancing software reliability IEEE Trans. Softw. Eng. 1986 12 1 157-171

[31]

Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, CASCON 1999, p. 13. IBM Press (1999)

[32]

Wang C, Chen Z, and Mao X Legay A and Bensalem S Optimizing Nop-shadows typestate analysis by filtering interferential configurations Runtime Verification 2013 Heidelberg Springer 269-284

[33]

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

Cited By

Soueidi CFalcone Y(2023)Instrumentation for RV: From Basic Monitoring to Advanced Use CasesRuntime Verification10.1007/978-3-031-44267-4_23(403-427)Online publication date: 3-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44267-4_23
Soueidi CFalcone Y(2023)Bridging the Gap: A Focused DSL for RV-Oriented Instrumentation with BISMRuntime Verification10.1007/978-3-031-44267-4_17(327-338)Online publication date: 3-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44267-4_17

Index Terms

Residual Runtime Verification via Reachability Analysis

Index terms have been assigned to the content through auto-classification.

Recommendations

Efficient and expressive bytecode-level instrumentation for Java programs
Abstract
We present an efficient and expressive tool for the instrumentation of Java programs at the bytecode level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool that features an ...
BISM: Bytecode-Level Instrumentation for Software Monitoring
Runtime Verification
Abstract
BISM (Bytecode-level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool which features an expressive high-level control-flow-aware instrumentation language. The language follows the aspect-oriented ...
Method for Reducing Overhead of Shared Memory Access Instrumentation
CSAE '19: Proceedings of the 3rd International Conference on Computer Science and Application Engineering

Memory monitoring is crucial for understanding the memory access behavior of applications. Especially in multithreaded programs, dealing with concurrency bugs relies on tracking and analyzing accesses to shared memory. Instrumentation is widely used to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Verified Software. Theories, Tools and Experiments.: 14th International Conference, VSTTE 2022, Trento, Italy, October 17–18, 2022, Revised Selected Papers

Oct 2022

175 pages

ISBN:978-3-031-25802-2

DOI:10.1007/978-3-031-25803-9

Editors:
Akash Lal
Microsoft Research, Karnataka, India
,
Stefano Tonetta
Fondazione Bruno Kessler, Trento, Italy

© The Author(s), under exclusive license to Springer Nature Switzerland AG 2023.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 February 2023

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Soueidi CFalcone Y(2023)Instrumentation for RV: From Basic Monitoring to Advanced Use CasesRuntime Verification10.1007/978-3-031-44267-4_23(403-427)Online publication date: 3-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44267-4_23
Soueidi CFalcone Y(2023)Bridging the Gap: A Focused DSL for RV-Oriented Instrumentation with BISMRuntime Verification10.1007/978-3-031-44267-4_17(327-338)Online publication date: 3-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44267-4_17

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents