[en] Runtime Verification (RV) dynamically analyses the sequence of events recorded during system execution, typically stored in traces, and provides a verdict on system behavior.
RV has tended to use Boolean, or sometimes quantitative, verdicts to express whether an execution satisfied some specification. However, engineers often want to know the reason for the verdict, which can be found by carrying out diagnostics.
In this paper, we develop a diagnostics approach for a time-based
fragment of iCFTL, a specification language designed for capturing
properties concerning inter-procedural, source code-level behaviour of
programs. We begin by developing an instrumentation scheme that builds
on iCFTL's original scheme, enabling the construction of more
informative traces. These traces are then used to determine a
point of no return, which is an event past which a
specification can never be satisfied. Our diagnostics approach then
highlights a section of the trace in question that leads to the point
of no return. We conclude the paper by presenting an evaluation of a
prototype tool. Across 21 diverse programs, we observe that our
approach is effective, efficient, and induces low time and space
overhead.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation
Disciplines :
Computer science
Author, co-author :
STRATAN, Cristina ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
DAWES, Joshua ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
BIANCULLI, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
External co-authors :
no
Language :
English
Title :
Diagnosing Violations of Time-based Properties Captured in iCFTL
Publication date :
April 2024
Event name :
FormaliSE '24: International Conference on Formal Methods in Software Engineering
Event date :
April 14-15, 2024
Audience :
International
Main work title :
FormaliSE '24: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE))
Publisher :
ACM, New York, United States - New York
Pages :
33--43
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
FnR Project :
FNR17065054 - Diagnostics Of Violations Of Signal And Source Code Behaviour In The Cps Settings, 2022 (01/03/2022-31/01/2026) - Cristina Stratan
Name of the research project :
Diagnostics of Violations of Signal and Source Code Behaviour in the CPS Settings
Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J Pace, and Gerardo Schneider. 2015. A specification language for static and runtime verification of data and control properties. In FM 2015: Formal Methods. Springer International Publishing, Cham, 108-125.
Howard Barringer, Ylies Falcone, Klaus Havelund, Giles Reger, and David Rydeheard. 2012. Quantified event automata: Towards expressive and efficient runtime monitors. In FM 2012: Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, 68-84.
Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. 2018. Introduction to Runtime Verification. Springer International Publishing, Cham, 1-33.
Ezio Bartocci, Niveditha Manjunath, Leonardo Mariani, Cristinel Mateis, and Dejan Ničkovic. 2019. Automatic failure explanation in CPS models. In International Conference on Software Engineering and Formal Methods. Springer, Cham, 69-86.
Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 1-64.
Michael A Bender, Martin Farach-Colton, Giridhar Pemmasani, Steven Skiena, and Pavel Sumazin. 2005. Lowest common ancestors in trees and directed acyclic graphs. Journal of Algorithms 57, 2 (2005), 75-94.
Chaima Boufaied, Claudio Menghi, Domenico Bianculli, Lionel Briand, and Yago Isasi Parache. 2020. Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach. In International Conference on Automated Software Engineering (ASE). IEEE/ACM, New York, NY, USA, 1004-1015.
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
Joshua Heneage Dawes and Domenico Bianculli. 2021. Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs. In International Conference on 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 and Giles Reger. 2019. Explaining violations of properties in control-flow temporal logic. In Runtime Verification. Springer International Publishing, Cham, 202-220.
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.
Jyotirmoy V Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A Seshia. 2017. Robust online monitoring of signal temporal logic. Formal Methods in System Design 51, 1 (2017), 5-30.
Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos. 2015. Metric interval temporal logic specification elicitation and debugging. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE, Austin, TX, USA, 70-79.
Wei Dou, Domenico Bianculli, and Lionel Briand. 2018. Model-driven trace diagnostics for pattern-based temporal specifications. In Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems. Association for Computing Machinery, New York, NY, USA, 278-288.
Thomas Ferrčre, Oded Maler, and Dejan Ničkovic. 2015. Trace diagnostics using temporal implicants. In International Symposium on Automated Technology for Verification and Analysis. Springer International Publishing, Cham, 241-258.
Robert J. Hall. 1995. Call path refinement profiles. IEEE Transactions on Software Engineering 21, 6 (1995), 481-496.
Hsi-Ming Ho, Joël Ouaknine, and JamesWorrell. 2014. Online monitoring of metric temporal logic. In Runtime Verification: 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings 5. Springer International Publishing, Cham, 178-192.
David Weisskopf Holmqvist and Suejb Memeti. 2023. Enhancing Performance Monitoring in C/C++ Programs with EDPM: A Domain-Specific Language for Performance Monitoring.
Ron Koymans. 1990. Specifying real-Time properties with metric temporal logic. Real-Time systems 2, 4 (1990), 255-299.
Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 152-166.
Dejan Ničkovic, Olivier Lebeltel, Oded Maler, Thomas Ferrère, and Dogan Ulus. 2020. AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer 22, 6 (2020), 741-758.
Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). IEEE, Providence, RI, USA, 46-57.
Barbara G Ryder. 1979. Constructing the call graph of a program. IEEE Transactions on Software Engineering SE-5, 3 (1979), 216-226.
Catia Trubiani, Riccardo Pinciroli, Andrea Biaggi, and Francesca Arcelli Fontana. 2023. Automated Detection of Software Performance Antipatterns in Java-Based Applications. IEEE Transactions on Software Engineering 49, 4 (2023), 2873-2891.
Ehsan Zibaei, Sebastian Banescu, and Alexander Pretschner. 2018. Diagnosis of Safety Incidents for Cyber-Physical Systems: A UAV Example. In 2018 3rd International Conference on System Reliability and Safety (ICSRS). IEEE, Barcelona, Spain, 120-129. https://doi.org/10.1109/ICSRS.2018.8688886
