More Web Proxy on the site http://driver.im/

Article

Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs

Authors:

Joshua Heneage Dawes,

Domenico BianculliAuthors Info & Claims

Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings

Pages 23 - 41

https://doi.org/10.1007/978-3-030-88494-9_2

Published: 11 October 2021 Publication History

Abstract

The problem of verifying a program at runtime with respect to some formal specification has led to the development of a rich collection of specification languages. These languages often have a high level of abstraction and provide sophisticated modal operators, giving a high level of expressiveness. In particular, this makes it possible to express properties concerning the source code level behaviour of programs. However, for many languages, the correspondence between events generated at the source code level and parts of the specification in question would have to be carefully defined.

To enable expressing—using a temporal logic—properties over source code level behaviour without the need for this correspondence, previous work introduced Control-Flow Temporal Logic (CFTL), a specification language with a low level of abstraction with respect to the source code of programs. However, this work focused solely on the intra-procedural setting. In this paper, we address this limitation by introducing Inter-procedural CFTL, a language for expressing source code level, inter-procedural properties of program runs. We evaluate the new language, iCFTL, via application to a real-world case study.

References

[1]

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

[2]

Alur R, Etessami K, and Madhusudan P Jensen K and Podelski A A temporal logic of nested calls and returns Tools and Algorithms for the Construction and Analysis of Systems 2004 Heidelberg Springer 467-481

[3]

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

[4]

Barringer H, Goldberg A, Havelund K, and Sen K Steffen B and Levi G Rule-based runtime verification Verification, Model Checking, and Abstract Interpretation 2004 Heidelberg Springer 44-57

[5]

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

[6]

Bauer A, Leucker M, and Schallhart C Comparing LTL semantics for runtime verification J. Log. Comput. 2010 20 3 651-674

[7]

Bensalem S, Bozga M, Krichen M, and Tripakis S Testing conformance of real-time applications by automatic generation of observers Electron. Notes Theor. Comput. Sci. 2005 113 23-43

[8]

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

[9]

CERN: Compact Muon Solenoid experiment. https://home.cern/science/experiments/cms

[10]

Colombo C, Pace GJ, and Schneider G Cofer D and Fantechi A Dynamic event-based runtime monitoring of real-time and contextual properties Formal Methods for Industrial Critical Systems 2009 Heidelberg Springer 135-149

[11]

D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), Burlington, Vermont, USA, 23–25 June 2005, pp. 166–174. IEEE Computer Society (2005).

[12]

Dawes, J.H.: A Python object-oriented framework for the CMS alignment and calibration data. In: Journal of Physics: Conference Series, vol. 898, p. 042059, October 2017.

[13]

Dawes, J.H.: Towards automated performance analysis of programs by runtime verification. Ph.D. thesis, University of Manchester (2021)

[14]

Dawes JH, Han M, Javed O, Reger G, Franzoni G, and Pfeiffer A Deshmukh J and Ničković D Analysing the performance of Python-based web services with the VyPR framework Runtime Verification 2020 Cham Springer 67-86

[15]

Dawes, J.H., Han, M., Reger, G., Franzoni, G., Pfeiffer, A.: Analysis tools for the VyPR framework for Python. In: International Conference on Computing in High Energy and Nuclear Physics, Adelaide, Australia 2019 (2019)

[16]

Dawes JH and Reger G Finkbeiner B and Mariani L Explaining violations of properties in control-flow temporal logic Runtime Verification 2019 Cham Springer 202-220

[17]

Dawes, J.H., Reger, G.: Specification of temporal properties of functions for runtime verification. In: Hung, C., Papadopoulos, G.A. (eds.) Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, SAC 2019, Limassol, Cyprus, 8–12 April 2019, pp. 2206–2214. ACM (2019).

[18]

Dou, W., Bianculli, D., Briand, L.C.: A model-driven approach to trace checking of pattern-based temporal properties. In: 20th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017, Austin, TX, USA, 17–22 September 2017, pp. 323–333. IEEE Computer Society (2017).

[19]

Fischer MJ and Ladner RE Propositional dynamic logic of regular programs J. Comput. Syst. Sci. 1979 18 2 194-211

[20]

Gastin P and Oddoux D Berry G, Comon H, and Finkel A Fast LTL to Büchi automata translation Computer Aided Verification 2001 Heidelberg Springer 53-65

[21]

Hallé S Falcone Y and Sánchez C When RV meets CEP Runtime Verification 2016 Cham Springer 68-91

[22]

Kim M, Viswanathan M, Kannan S, Lee I, and Sokolsky O Java-MaC: a run-time assurance approach for Java programs Formal Methods Syst. Des. 2004 24 2 129-155

[23]

Koymans R Specifying real-time properties with metric temporal logic Real Time Syst. 1990 2 4 255-299

[24]

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, pp. 46–57. IEEE Computer Society (1977).

[25]

Roşu G, Chen F, and Ball T Leucker M Synthesizing monitors for safety properties: this time with calls and returns Runtime Verification 2008 Heidelberg Springer 51-68

Cited By

Dawes JBianculli D(2022)Specifying Source Code and Signal-based Behaviour of Cyber-Physical System ComponentsFormal Aspects of Component Software10.1007/978-3-031-20872-0_2(20-38)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_2
Stoffers MWeinert A(2022)Towards Specificationless Monitoring of Provenance-Emitting SystemsRuntime Verification10.1007/978-3-031-17196-3_14(253-263)Online publication date: 28-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17196-3_14

Index Terms

Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Modal and temporal logics
  2. Semantics and reasoning
    1. Program reasoning

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

Recommendations

Specifying Source Code and Signal-based Behaviour of Cyber-Physical System Components
Formal Aspects of Component Software
Abstract
Specifying properties over the behaviour of components of Cyber-Physical Systems usually focuses on the behaviour of signals, i.e., the behaviour of the physical part of the system, leaving the behaviour of the cyber components implicit. There ...
Do bugs lead to unnaturalness of source code?
ESEC/FSE 2022: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Texts in natural languages are highly repetitive and predictable because of the naturalness of natural languages. Recent research validated that source code in programming languages is also repetitive and predictable, and naturalness is an inherent ...
Specifying Dynamic Analyses by Extending Language Semantics

Dynamic analysis is increasingly attracting attention for debugging, profiling, and program comprehension. Ten to twenty years ago, many dynamic analyses investigated only simple method execution traces. Today, in contrast, many sophisticated dynamic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings

Oct 2021

338 pages

ISBN:978-3-030-88493-2

DOI:10.1007/978-3-030-88494-9

Editors:
Lu Feng
University of Virginia, Charlottesville, VA, USA
,
Dana Fisman
Ben-Gurion University of the Negev, Be'er Sheva, Israel

© Springer Nature Switzerland AG 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 October 2021

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 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Dawes JBianculli D(2022)Specifying Source Code and Signal-based Behaviour of Cyber-Physical System ComponentsFormal Aspects of Component Software10.1007/978-3-031-20872-0_2(20-38)Online publication date: 10-Nov-2022
https://dl.acm.org/doi/10.1007/978-3-031-20872-0_2
Stoffers MWeinert A(2022)Towards Specificationless Monitoring of Provenance-Emitting SystemsRuntime Verification10.1007/978-3-031-17196-3_14(253-263)Online publication date: 28-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17196-3_14

View Options

View options

Figures

Tables

Media

View Table of Conten