Operational and Declarative Runtime Verification (Keynote)
Pages 3 - 12
Abstract
Runtime verification (RV) is used to monitor executions of a system, checking them against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid a failure. One can identify two main approaches of specifying properties to be monitored: operational specification and declarative specification. Operational specification describes, using a programming language like formalism, how each new monitored event updates a summary of the observed sequence of events, consisting of user defined variables. This kind of specification is attractive, e.g., for describing aggregated arithmetic calculations and can be very simple to implement. Declarative specification gives a more global view of the requirements that the monitored execution sequences must satisfy, based on a temporal formalism, e.g., propositional or first-order temporal logic. We describe an RV system designed and implemented to work with the two kinds of specifications. It allows the two parts to collaborate by sending ongoing results between them. This results in benefiting from both capabilities and reducing the deficiencies of each of the separate specification methods. We compare alternative approaches to combining operational and declarative specification as internal and external DSLs.
References
[1]
Howard Barringer and Klaus Havelund. 2011. TraceContract: A Scala DSL for Trace Analysis. In Proc. 17th Int. Symposium on Formal Methods (FM 2011) (LNCS, Vol. 6664). Springer, Limerick, Ireland. 57–72.
[2]
Howard Barringer, David Rydeheard, and Klaus Havelund. 2007. Rule Systems for Run-Time Monitoring: From Eagle to RuleR. In Runtime Verification, Oleg Sokolsky and Serdar Taşıran (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 111–125.
[3]
David A. Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu. 2015. Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des., 46, 3 (2015), 262–285.
[4]
Christian Colombo, Andrew Gauci, and Gordon J. Pace. 2010. LarvaStat: Monitoring of Statistical Properties. In Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings, Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, and Nikolai Tillmann (Eds.) (Lecture Notes in Computer Science, Vol. 6418). Springer, 480–484.
[5]
Dennis Dams, Klaus Havelund, and Sean Kauffman. 2022. A Python Library for Trace Analysis. In 22nd International Conference on Runtime Verification (RV), Thao Dang and Volker Stolz (Eds.) (LNCS, Vol. 13498). Springer International Publishing, 264–273.
[6]
B. D’Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H.B. Sipma, S. Mehrotra, and Z. Manna. 2005. LOLA: runtime monitoring of synchronous systems. In 12th International Symposium on Temporal Representation and Reasoning (TIME’05). 166–174.
[7]
Normann Decker, Martin Leucker, and Daniel Thoma. 2016. Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf., 18, 2 (2016), 205–225.
[8]
Felipe Gorostiaga and César Sánchez. 2021. HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.) (Lecture Notes in Computer Science, Vol. 13047). Springer, 563–580.
[9]
Sylvain Halle and Roger Villemaire. 2012. Runtime Enforcement of Web Service Message Contracts with Data. IEEE Transactions on Services Computing, 5, 2, 192–206.
[10]
Klaus Havelund. 2014. Data Automata in Scala. In 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014. IEEE Computer Society, 1–9.
[11]
Klaus Havelund. 2015. Rule-based runtime verification revisited. Software Tools for Technology Transfer (STTT), 17, 2 (2015), 143–170.
[12]
Klaus Havelund and Gerard Holzmann. 2023. Programming event monitors. International Journal on Software Tools for Technology Transfer, https://doi.org/10.1007/s10009-023-00706-1
[13]
Klaus Havelund and Rajeev Joshi. 2017. Modeling Rover Communication Using Hierarchical State Machines with Scala. In 2nd International Workshop on the Timing Performance in Safety Engineering (TIPS 2017) (LNCS, Vol. 10489). Springer, 447–461.
[14]
Klaus Havelund, Panagiotis Katsaros, Moran Omer, Doron Peled, and Anastasios Temperekidis. 2024. TP-DejaVu: Combining Operational and Declarative Runtime Verification. In Verification, Model Checking, and Abstract Interpretation, Rayna Dimitrova, Ori Lahav, and Sebastian Wolff (Eds.). Springer Nature Switzerland, Cham. 249–263.
[15]
Klaus Havelund and Doron Peled. 2020. First-Order Timed Runtime Verification Using BDDs. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, Dang Van Hung and Oleg Sokolsky (Eds.) (Lecture Notes in Computer Science, Vol. 12302). Springer, 3–24. https://doi.org/10.1007/978-3-030-59152-6_1
[16]
Klaus Havelund and Doron Peled. 2021. An extension of first-order LTL with rules with application to runtime verification. Int. J. Softw. Tools Technol. Transf., 23, 4 (2021), 547–563.
[17]
Klaus Havelund, Doron Peled, and Dogan Ulus. 2020. First-order temporal logic monitoring with BDDs. Formal Methods in System Design, 56, 1-3 (2020), 1–21.
[18]
Klaus Haveund. 2024. Daut - Monitoring Data Streams with Data Automata. https://github.com/havelund/daut
[19]
Hannes Kallwies, Martin Leucker, Malte Schmitz, Albert Schulz, Daniel Thoma, and Alexander Weiss. 2022. TeSSLa – An Ecosystem for Runtime Verification. In Runtime Verification, Thao Dang and Volker Stolz (Eds.). Springer International Publishing, Cham. 314–324.
[20]
Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, and Mahesh Viswanathan. 2001. Java-MaC: a Run-time Assurance Tool for Java Programs. In Workshop on Runtime Verification, RV 2001, in connection with CAV 2001, Paris, France, July 23, 2001, Klaus Havelund and Grigore Rosu (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 55). Elsevier, 218–235. https://doi.org/10.1016/S1571-0661(04)00254-3
[21]
Elif Kurklu and Klaus Havelund. 2020. A Flight Rule Checker for the LADEE Lunar Spacecraft. In 17th International Colloquium on Theoretical Aspects of Computing (ICTAC’20). TBD.
[22]
John McCarthy. 2007. Elephant 2000: A programming language based on speech acts. In 22nd ACM SIGPLAN conference on object-oriented programming systems and applications companion. 723–724.
[23]
Giles Reger, Helena Cuenca Cruz, and David E. Rydeheard. 2015. MarQ: Monitoring at Runtime with QEA. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Christel Baier and Cesare Tinelli (Eds.) (Lecture Notes in Computer Science, Vol. 9035). Springer, 596–610.
[24]
W3 Schools. 2024. Python MySQL. https://www.w3schools.com/python/python_mysql_getstarted.asp
[25]
Open Source. 2024. ScalikeJDBC. https://scalikejdbc.org
Index Terms
- Operational and Declarative Runtime Verification (Keynote)
Recommendations
Runtime verification: the application perspective
In the past decade, runtime verification (RV) has gained much focus, from both the research community and practitioners. RV combines a set of theories, techniques and tools aiming towards efficient analysis of systems' executions and guaranteeing their ...
Runtime Verification of Generalized Test Tables
NASA Formal MethodsAbstractRuntime verification allows validation of systems during their operation by monitoring crucial system properties. It is common to generate monitors from temporal specifications formulated in languages like MTL or LTL. However, writing formal ...
Extending Ina Jo with Temporal Logic
The authors give both informal and formal descriptions of both the current Ina Jo specification language and Ina Jo enhanced with temporal logic. They include details of a simple example to demonstrate the use of the proof system and details of an ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2024
51 pages
Copyright © 2024 Copyright held by the owner/author(s).
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 September 2024
Check for updates
Author Tags
Qualifiers
- Keynote
Funding Sources
- NASA
Conference
VORTEX '24
Sponsor:
VORTEX '24: 7th ACM International Workshop on Verification and Monitoring at Runtime Execution
September 19, 2024
Vienna, Austria
Upcoming Conference
ISSTA '25
- Sponsor:
- sigsoft
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 73Total Downloads
- Downloads (Last 12 months)73
- Downloads (Last 6 weeks)3
Reflects downloads up to 27 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in