Checking Complex Source Code-Level Constraints using Runtime Verification

DAWES, Joshua; BIANCULLI, Domenico

doi:10.1145/3663529.3663845

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Checking Complex Source Code-Level Constraints using Runtime Verification

DAWES, Joshua; BIANCULLI, Domenico

2024 • In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE Companion ’24)

Peer reviewed Dataset

Permalink
https://hdl.handle.net/10993/61125

DOI
10.1145/3663529.3663845

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

main.pdf

Author postprint (636.74 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Runtime Verification; Temporal Logic Semantics; Instrumentation; Trace Checking; Monitoring

Abstract :

[en] Runtime Verification (RV) is the process of taking a trace, representing an execution of some computational system, and checking it for satisfaction of some specification, written in a specification language. RV approaches are often aimed at being used as part of software development processes. In this case, engineers might maintain a set of specifications that capture properties concerning their source code's behaviour at runtime. To be used in such a setting, an RV approach must provide a specification language that is practical for engineers to use regularly, along with an efficient monitoring algorithm that enables program executions to be checked quickly. This work develops an RV approach that has been adopted by two industry partners. In particular, we take a source code fragment of an existing specification language, \scslLong, which enables properties of interest to our partners to be captured easily, and develop 1) a new semantics for the fragment, 2) an instrumentation approach, and 3) a monitoring procedure for it. We show that our monitoring procedure scales to program execution traces containing up to one million events, and describe initial applications of our prototype framework (that implements our instrumentation and monitoring procedures) by the partners themselves.

Research center :

Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation

Disciplines :

Computer science

Author, co-author :

DAWES, Joshua ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust > SVV > Team Domenico BIANCULLI

BIANCULLI, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV

External co-authors :

Language :

English

Title :

Checking Complex Source Code-Level Constraints using Runtime Verification

Publication date :

July 2024

Event name :

32nd ACM International Conference on the Foundations of Software Engineering (FSE 2024)

Event place :

Brazil

Event date :

15-19 July 2024

Audience :

International

Main work title :

Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE Companion ’24)

Publisher :

ACM

Pages :

255-265

Peer reviewed :

Peer reviewed

Focus Area :

Security, Reliability and Trust

European Projects :

H2020 - 957254 - COSMOS - DevOps for Complex Cyber-physical Systems

Funders :

EC - European Commission
Union Européenne

Funding number :

957254

Data Set :

Checking Complex Source Code-level Constraints using Runtime Verification - FSE 2024 (Industry papers track) - Artefact
SCSL-Trace-Checker - Source Code

Available on ORBilu :

since 09 May 2024

Statistics

Number of views

136 (14 by Unilu)

Number of downloads

159 (11 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenAlex citations

Bibliography

Stanley Bak. 2023. The AeroBenchVVPython GitHub Repository. https://github.com/stanleybak/AeroBenchVVPython. Accessed: 2023-08-11.
David Basin, Bhargav Nagaraja Bhatt, Srđan Krstić, and Dmitriy Traytel. 2019. Almost event-rate independent monitoring. Formal Methods in System Design 54, 3 (2019), 449–478. https://doi.org/10.1007/s10703-018-00328-3
David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke, and Heiko Mantel. 2016. Scalable Offline Monitoring of Temporal Specifications. Form. Methods Syst. Des. 49, 1–2 (oct 2016), 75–108. https://doi.org/10.1007/s10703-016-0242-y
Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20, 4, Article 14 (sep 2011), 64 pages. https://doi.org/10.1145/2000799.2000800
Eric Bodden, Patrick Lam, and Laurie Hendren. 2010. Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In Runtime Verification, Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon Pace, Grigore Roşu, Oleg Sokolsky, and Nikolai Tillmann (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183–197.
Borzoo Bonakdarpour, Samaneh Navabpour, and Sebastian Fischmeister. 2011. Sampling-Based Runtime Verification. In FM 2011: Formal Methods, Michael Butler and Wolfram Schulte (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 88–102.
Chaima Boufaied, Claudio Menghi, Domenico Bianculli, and Lionel C. Briand. 2023. Trace Diagnostics for Signal-Based Temporal Properties. IEEE Transactions on Software Engineering 49, 5 (2023), 3131–3154. https://doi.org/10.1109/TSE.2023.3242588
Agnishom Chattopadhyay and Konstantinos Mamouras. 2020. A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics. In Runtime Verification. Springer International Publishing, Cham, 383–403.
Christoph Czepa, Amirali Amiri, Evangelos Ntentos, and Uwe Zdun. 2019. Modeling compliance specifications in linear temporal logic, event processing language and property specification patterns: a controlled experiment on understandability. Software and Systems Modeling 18, 6 (2019), 3331–3371. https://doi.org/10.1007/s10270-019-00721-4
C. Czepa and U. Zdun. 2018. On the Understandability of Temporal Properties Formalized in Linear Temporal Logic, Property Specification Patterns and Event Processing Language. IEEE Trans. Softw. Eng. 46 (2018), 1–13. doi: 10.1109/TSE. 2018.2859926.
Joshua Dawes and Domenico Bianculli. 2024. Checking Complex Source Code-level Constraints using Runtime Verification - FSE 2024 (Industry papers track) - Artefact. https://doi.org/10.6084/m9.figshare.25783266.v1
Joshua Dawes and Alexander Vatov. 2024. SCSL-Trace-Checker - Source Code. https://doi.org/10.6084/m9.figshare.25784355.v1
Joshua Heneage Dawes and Domenico Bianculli. 2021. Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs. In Runtime Verification, Lu Feng and Dana Fisman (Eds.). Springer International Publishing, Cham, 23–41.
Joshua Heneage Dawes and Domenico Bianculli. 2021. Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs. In Runtime Verification. Springer International Publishing, Cham, 23–41.
Joshua Heneage Dawes and Domenico Bianculli. 2022. Specifying Source Code and Signal-based Behaviour of Cyber-Physical System Components. In Formal Aspects of Component Software. Springer International Publishing, Cham, 20–38.
Joshua Heneage Dawes, Marta Han, Omar Javed, Giles Reger, Giovanni Franzoni, and Andreas Pfeiffer. 2020. Analysing the Performance of Python-Based Web Services with the VyPR Framework. In Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings (Los Angeles, CA, USA). Springer-Verlag, Berlin, Heidelberg, 67–86. https://doi.org/10.1007/978-3-030-60508-7_4
Joshua Heneage Dawes and Giles Reger. 2019. Specification of Temporal Properties of Functions for Runtime Verification. In Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing (Limassol, Cyprus) (SAC’19). Association for Computing Machinery, New York, NY, USA, 2206–2214. https://doi.org/10.1145/3297280.3297497
Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos. 2014. On-Line Monitoring for Temporal Logic Robustness. CoRR abs/1408.0045 (2014). arXiv:1408.0045 http://arxiv.org/abs/1408.0045
Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, and David Van Campenhout. 2003. Reasoning with Temporal Logic on Truncated Paths. In Computer Aided Verification, Warren A. Hunt and Fabio Somenzi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 27–39.
Thomas Ferrère, Oded Maler, and Dejan Ničković. 2015. Trace diagnostics using temporal implicants. In International Symposium on Automated Technology for Verification and Analysis. Springer, Cham, 241–258.
M.C.W. Geilen. 2001. On the Construction of Monitors for Temporal Logic Properties. Electronic Notes in Theoretical Computer Science 55, 2 (2001), 181–199. https://doi.org/10.1016/S1571-0661(04)00252-X RV’2001, Runtime Verification (in connection with CAV’01).
Klaus Havelund and Grigore Roşu. 2002. Synthesizing Monitors for Safety Properties. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 342–356.
Hsi-Ming Ho, Joël Ouaknine, and James Worrell. 2014. Online Monitoring of Metric Temporal Logic. In Runtime Verification. Springer International Publishing, Cham, 178–192.
Moonzoo Kim, Mahesh Viswanathan, Sampath Kannan, Insup Lee, and Oleg Sokolsky. 2004. Java-MaC: A Run-Time Assurance Approach for Java Programs. Form. Methods Syst. Des. 24, 2 (mar 2004), 129–155. https://doi.org/10.1023/B:FORM.0000017719.43755.7c
Konstantinos Mamouras, Agnishom Chattopadhyay, and Zhifu Wang. 2021. A Compositional Framework for Quantitative Online Monitoring over Continuous-Time Signals. In Runtime Verification. Springer International Publishing, Cham, 142–163.
Amjad Nusayr and Jonathan Cook. 2009. Using AOP for Detailed Runtime Monitoring Instrumentation. In Proceedings of the Seventh International Workshop on Dynamic Analysis (Chicago, Illinois) (WODA’09). Association for Computing Machinery, New York, NY, USA, 8–14. https://doi.org/10.1145/2134243.2134246
Giles Reger, Helena Cuenca Cruz, and David Rydeheard. 2015. MarQ: Monitoring at Runtime with QEA. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 596–610.
Joshua Schneider, David Basin, Frederik Brix, Srdjan Krstic, and Dmitriy Traytel. 2019. Adaptive Online First-Order Monitoring. In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11781). Springer, 133–150. https://doi.org/10.1007/978-3-030-31784-3_8
Joshua Schneider, David Basin, Frederik Brix, Srundefinedan Krstić, and Dmitriy Traytel. 2021. Scalable Online First-Order Monitoring. Int. J. Softw. Tools Technol. Transf. 23, 2 (apr 2021), 185–208. https://doi.org/10.1007/s10009-021-00607-1
Cristina Stratan, Joshua Dawes, and Domenico Bianculli. 2024. Diagnosing Violations of Time-based Properties Captured in iCFTL. In Proceedings of the 2024 International Conference on Formal Methods in Software Engineering (FormaliSE 2024), co-located with ICSE 2024, Lisbon, Portugal. ACM.
Moshe Y. Vardi. 1996. An Automata-Theoretic Approach to Linear Temporal Logic. In Proceedings of the VIII Banff Higher Order Workshop Conference on Logics for Concurrency: Structure versus Automata: Structure versus Automata (Banff, Canada). Springer-Verlag, Berlin, Heidelberg, 238–266.