research-article

Parametric Trace Expressions for Runtime Verification of Java-Like Programs

Authors:

Angelo Ferrando,

Luca Franceschini,

Viviana MascardiAuthors Info & Claims

FTFJP'17: Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs

Article No.: 10, Pages 1 - 6

https://doi.org/10.1145/3103111.3104037

Published: 18 June 2017 Publication History

Abstract

Parametric trace expressions are a formalism expressly designed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems.

Trace expressions are built on the general notion of event type, which allows them to be adopted in different contexts. In this paper we show how trace expressions can be used for conveniently specifying the expected behavior of a Java-like program to be monitored at runtime.

Furthermore, we investigate the basic properties of the primitive operators on which trace expressions are coinductively defined in terms of a labeled transition system; this provides a basis for formal reasoning about equivalence of trace expressions and for adopting useful optimization techniques to speed up runtime verification.

References

[1]

C. Allan, P. Avgustinov, A. S. Christensen, L. Hendren, S. Kuzins, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to Aspect J. In OOPSLA '05, pages 345--364. ACM, 2005.

Digital Library

[2]

D. Ancona, S. Drossopoulou, and V. Mascardi. Automatic generation of self-monitoring MASs from multiparty global session types in Jason. In DALT 2012, volume 7784 of LNAI, pages 76--95. Springer, 2012.

[3]

D. Ancona, D. Briola, A. El Fallah Seghrouchni, V. Mascardi, and P. Taillibert. Efficient Verification of MASs with Projections. In EMAS 2014, Revised Selected Papers, pages 246--270, 2014.

[4]

D. Ancona, V. Bono, M. Bravetti, J. Campos, G. Castagna, P. M. Deniélou, S. J. Gay, N. Gesbert, E. Giachino, R. Hu, E. B. Johnsen, F. Martins, V. Mascardi, F. Montesi, R. Neykova, N. Ng, L. Padovani, V. Vasconcelos, and N. Yoshida. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95--230, 2016a.

Digital Library

[5]

D. Ancona, A. Ferrando, and V. Mascardi. Comparing trace expressions and linear temporal logic for runtime verification. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 47--64. Springer Verlag, 2016b.

Digital Library

[6]

D. Ancona, A. Ferrando, and V. Mascardi. Parametric runtime verification of multiagent systems. In AAMAS 2017. Proceedings, 2017. Extended Abstract. To appear.

Digital Library

[7]

D. Briola, V. Mascardi, and D. Ancona. Distributed runtime verification of JADE multiagent systems. In IDC, Studies in Computational Intelligence. Springer, 2014.

[8]

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

[9]

F. Chen and G. Rosu. Mop: an efficient and generic runtime verification framework. In OOPSLA 2007, pages 569--588, 2007.

Digital Library

[10]

C. Colombo, G. J. Pace, and G. Schneider. LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper). In SEFM 2009, pages 33--37, 2009.

Digital Library

[11]

B. Courcelle. Fundamental properties of infinite trees. Theoretical Comput. Sci., 25:95--169, 1983.

[12]

F. S. de Boer and C. P. T. de Gouw. Combining Monitoring With Run-Time Assertion Checking. In SFM 14, pages 217--262. Springer, 2014.

Digital Library

[13]

Q. Luo, Y. Zhang, C. Lee, D. Jin, P. O. Meredith, T. F. Serbanuta, and G. Rosu. Rv-monitor: Efficient parametric runtime verification with simultaneous properties. In RV'14, volume 8734, pages 285--300. Springer, 2014.

[14]

M. C. Martin, V. B. Livshits, and M. S. Lam. Finding application errors and security flaws using PQL: a program query language. In OOPSLA 2005, pages 365--383, 2005.

Digital Library

[15]

C. Vasconcelos and A. Ravara. From object-oriented code with assertions to behavioural types. In SAC 2017, 2017.

Digital Library

Cited By

Ancona DFerrando AMascardi V(2022)Mind the Gap! Runtime Verification of Partially Observable MASs with Probabilistic Trace ExpressionsMulti-Agent Systems10.1007/978-3-031-20614-6_2(22-40)Online publication date: 11-Dec-2022
https://doi.org/10.1007/978-3-031-20614-6_2
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
Ancona DFranceschini LFerrando AMascardi V(2021)RML: Theory and practice of a domain specific language for runtime verificationScience of Computer Programming10.1016/j.scico.2021.102610205(102610)Online publication date: May-2021
https://doi.org/10.1016/j.scico.2021.102610
Show More Cited By

Index Terms

Parametric Trace Expressions for Runtime Verification of Java-Like Programs
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Operational semantics

Recommendations

Parametric Runtime Verification of Multiagent Systems
AAMAS '17: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems

Parametricity is an important feature of a monitoring system for making runtime verification (RV) more effective, since, typically, correctness of traces depends on the specific data values that are carried by the monitored events of the trace, and that,...
Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification
Essays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 9660

Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real protocols, and to generate monitors for mainstream ...
From parametric trace slicing to rule systems
Abstract
Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for ...

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

FTFJP'17: Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs

June 2017

49 pages

ISBN:9781450350983

DOI:10.1145/3103111

Copyright © 2017 ACM.

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 components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages
AITO: Assoc Internationale por les Technologies Objects

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

ECOOP '17

ECOOP '17: European Conference on Object-Oriented Programming

June 18 - 23, 2017

Barcelona, Spain

Acceptance Rates

FTFJP'17 Paper Acceptance Rate 10 of 12 submissions, 83%;

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
91
Total Downloads

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

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ancona DFerrando AMascardi V(2022)Mind the Gap! Runtime Verification of Partially Observable MASs with Probabilistic Trace ExpressionsMulti-Agent Systems10.1007/978-3-031-20614-6_2(22-40)Online publication date: 11-Dec-2022
https://doi.org/10.1007/978-3-031-20614-6_2
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
Ancona DFranceschini LFerrando AMascardi V(2021)RML: Theory and practice of a domain specific language for runtime verificationScience of Computer Programming10.1016/j.scico.2021.102610205(102610)Online publication date: May-2021
https://doi.org/10.1016/j.scico.2021.102610
Serrano EBajo J(2020)Discovering Hidden Mental States in Open Multi-Agent Systems by Leveraging Multi-Protocol Regularities with Machine LearningSensors10.3390/s2018519820:18(5198)Online publication date: 12-Sep-2020
https://doi.org/10.3390/s20185198
Dennis LFisher M(2020)Verifiable Self-Aware Agent-Based Autonomous SystemsProceedings of the IEEE10.1109/JPROC.2020.2991262108:7(1011-1026)Online publication date: Jul-2020
https://doi.org/10.1109/JPROC.2020.2991262
Ferrando AWinikoff MCranefield SDignum FMascardi V(2020)On Enactability of Agent Interaction Protocols: Towards a Unified ApproachEngineering Multi-Agent Systems10.1007/978-3-030-51417-4_3(43-64)Online publication date: 11-Jul-2020
https://doi.org/10.1007/978-3-030-51417-4_3
Ferrando ADennis LAncona DFisher MMascardi V(2018)Verifying and Validating Autonomous Systems: Towards an Integrated ApproachRuntime Verification10.1007/978-3-030-03769-7_15(263-281)Online publication date: 8-Nov-2018
https://doi.org/10.1007/978-3-030-03769-7_15

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten