extended-abstract

RML: runtime monitoring language: a system-agnostic DSL for runtime verification

Author:

Programming '19: Companion Proceedings of the 3rd International Conference on the Art, Science, and Engineering of Programming

Article No.: 28, Pages 1 - 3

https://doi.org/10.1145/3328433.3328462

Published: 01 April 2019 Publication History

Get Access

Abstract

Runtime verification (RV) [11] is a form of verification happening at runtime rather than compile-time. While static verification proves whether a property holds for every possible run of the program under scrutiny, RV only deals with a single execution (at a time). RV offers more flexibility in terms of provable properties: some specifications that may be particularly hard (or even impossible) to enforce statically can be checked at runtime, when more information are available.

References

[1]

Ancona, D., Ferrando, A., and Mascardi, V. Comparing trace expressions and linear temporal logic for runtime verification. In Theory and Practice of Formal Methods. Springer, 2016, pp. 47--64.

Digital Library

Google Scholar

[2]

Ancona, D., Ferrando, A., and Mascardi, V. Parametric runtime verification of multiagent systems. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8--12, 2017 (2017), pp. 1457--1459.

Digital Library

Google Scholar

[3]

Bauer, A., Leucker, M., and Schallhart, C. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 14.

Digital Library

Google Scholar

[4]

Bodden, E., Hendren, L. J., Lam, P., Lhoták, O., and Naeem, N. A. Collaborative runtime verification with Tracematches. J. Log. Comput. 20, 3 (2010), 707--723.

Digital Library

Google Scholar

[5]

Brörkens, M., and Möller, M. Dynamic event generation for runtime checking using the JDI. Electr. Notes Theor. Comput. Sci. 70, 4 (2002), 21--35.

Crossref

Google Scholar

[6]

Chen, F., and Rosu, G. Java-MOP: a monitoring oriented programming environment for java. In TACAS (2005), vol. 3440, Springer, pp. 546--550.

Digital Library

Google Scholar

[7]

Colombo, C., Pace, G. J., and Schneider, G. LARVA - safer monitoring of real-time Java programs. In SEFM 2009 (2009), pp. 33--37.

Digital Library

Google Scholar

[8]

de Boer, F. S., and de Gouw, S. Combining monitoring with run-time assertion checking. In Formal Methods for Executable Software Models. Springer, 2014, pp. 217--262.

Digital Library

Google Scholar

[9]

Gamma, E. Design patterns: elements of reusable object-oriented software. Pearson Education India, 1995.

Digital Library

Google Scholar

[10]

Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., and Griswold, W. G. An overview of AspectJ. In ECOOP 2001 --- Object-Oriented Programming (Berlin, Heidelberg, 2001), J. L. Knudsen, Ed., Springer Berlin Heidelberg, pp. 327--354.

Digital Library

Google Scholar

[11]

Leucker, M., and Schallhart, C. A brief account of runtime verification. The Journal of Logic and Algebraic Programming 78, 5 (2009), 293 -- 303. The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'07).

Crossref

Google Scholar

[12]

Martin, M., Livshits, B., and Lam, M. S. Finding application errors and security flaws using PQL: a program query language. In ACM SIGPLAN Notices (2005), vol. 40, ACM, pp. 365--383.

Digital Library

Google Scholar

[13]

Parr, T. J., and Quong, R. W. ANTLR: A predicated- LL(k) parser generator. Softw., Pract. Exper. 25, 7 (1995), 789--810.

Digital Library

Google Scholar

[14]

Pnueli, A. The temporal logic of programs. In Foundations of Computer Science, 1977., 18th Annual Symposium on (1977), IEEE, pp. 46--57.

Digital Library

Google Scholar

[15]

Simon, L., Mallya, A., Bansal, A., and Gupta, G. Coinductive logic programming. In Logic Programming (Berlin, Heidelberg, 2006), S. Etalle and M. Truszczyński, Eds., Springer Berlin Heidelberg, pp. 330--345.

Digital Library

Google Scholar

Cited By

View all

Ancona DFerrando AMascardi V(2023)Exploiting Logic Programming for Runtime Verification: Current and Future PerspectivesProlog: The Next 50 Years10.1007/978-3-031-35254-6_25(300-317)Online publication date: 17-Jun-2023
https://doi.org/10.1007/978-3-031-35254-6_25
Ferrando ADennis LCardoso RFisher MAncona DMascardi V(2021)Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive SystemsACM Transactions on Software Engineering and Methodology10.1145/344724630:4(1-43)Online publication date: 10-May-2021
https://dl.acm.org/doi/10.1145/3447246
Douha DMokhtari AGuessoum ZMandiau R(2021)Towards a non monotonic agent testing2021 IEEE/ACS 18th International Conference on Computer Systems and Applications (AICCSA)10.1109/AICCSA53542.2021.9686931(1-8)Online publication date: Nov-2021
https://doi.org/10.1109/AICCSA53542.2021.9686931
Show More Cited By

Index Terms

RML: runtime monitoring language: a system-agnostic DSL for runtime verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. Context specific languages
      1. Domain specific languages

Recommendations

Introduction to the special issue on runtime verification

This article introduces the extended versions of selected papers from the refereed proceedings of the 16th International Conference on Runtime Verification (RV 2016) held in Madrid, Spain, in September 2016. Runtime verification encompasses all aspects ...
Introduction to the Special Issue on Runtime Verification
Abstract
Runtime verification (RV) refers to methods for formal reasoning about all aspects of the dynamic execution of systems, including hardware, software, and cyber-physical systems. RV includes techniques to assess and enforce correctness of a system ...
Timed runtime monitoring for multiparty conversations
Abstract
We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, which we have developed ...

Reviews

Reviewer: Bernard Kuc

This paper on the runtime monitoring language (RML) is a very brief look at a system-agnostic domain-specific language (DSL) for runtime verification. This language is system agnostic due to its use of JavaScript Object Notation (JSON) as a communication format between the verification language and the instrumentation layer that wraps the system to be monitored. The author provides an example of how the specification for the verification of an iterator would be written. There is also a brief summary of the implementation, which compiles the language down to trace expressions that are then implemented in Prolog. The translation into Prolog is implemented in Kotlin. When comparing against related work, the author focuses on the system independence of RML. The design pattern of providing a wrapper or adapter to construct a uniform interface over heterogeneous systems is not new in any respect. Given that there is only a single client of the instrumentation layer in this situation, the success of the approach depends entirely on the relative complexity of the client, in this case RML, and the adaptation layer, which will need to be written for every system to be verified. A more detailed paper is required to formulate a qualitative assessment of the approach.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Programming '19: Companion Proceedings of the 3rd International Conference on the Art, Science, and Engineering of Programming

April 2019

201 pages

ISBN:9781450362573

DOI:10.1145/3328433

Editors:
Stefan Marr
University of Kent, United Kingdom
,
Walter Cazzola
Università degli Studi di Milano, Italy

Permission to make digital or hard copies of part or all 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.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 2019

Check for updates

Author Tags

Qualifiers

Extended-abstract

Conference

Programming '19

Programming '19: Companion of the 3rd International Conference on Art, Science, and Engineering of Programming

April 1 - 4, 2019

Genova, Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
69
Total Downloads

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

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ancona DFerrando AMascardi V(2023)Exploiting Logic Programming for Runtime Verification: Current and Future PerspectivesProlog: The Next 50 Years10.1007/978-3-031-35254-6_25(300-317)Online publication date: 17-Jun-2023
https://doi.org/10.1007/978-3-031-35254-6_25
Ferrando ADennis LCardoso RFisher MAncona DMascardi V(2021)Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive SystemsACM Transactions on Software Engineering and Methodology10.1145/344724630:4(1-43)Online publication date: 10-May-2021
https://dl.acm.org/doi/10.1145/3447246
Douha DMokhtari AGuessoum ZMandiau R(2021)Towards a non monotonic agent testing2021 IEEE/ACS 18th International Conference on Computer Systems and Applications (AICCSA)10.1109/AICCSA53542.2021.9686931(1-8)Online publication date: Nov-2021
https://doi.org/10.1109/AICCSA53542.2021.9686931
Cardoso RKourtis GDennis LDixon CFarrell MFisher MWebster M(2021)A Review of Verification and Validation for Space Autonomous SystemsCurrent Robotics Reports10.1007/s43154-021-00058-12:3(273-283)Online publication date: 18-Jun-2021
https://doi.org/10.1007/s43154-021-00058-1
Calegari RCiatto GMascardi VOmicini A(2021)Logic-based technologies for multi-agent systems: a systematic literature reviewAutonomous Agents and Multi-Agent Systems10.1007/s10458-020-09478-335:1Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10458-020-09478-3
Biagetti AFerrando AMascardi V(2020)The DigForSim Agent Based Simulator of People Movements in Crime ScenesAdvances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection10.1007/978-3-030-49778-1_4(42-54)Online publication date: 15-Jun-2020
https://doi.org/10.1007/978-3-030-49778-1_4

View Options

Login options

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

Cited By

Index Terms

Recommendations

Introduction to the special issue on runtime verification

Introduction to the Special Issue on Runtime Verification

Timed runtime monitoring for multiparty conversations

Reviews

Access critical reviews of Computing literature here