Article

A lightweight LTL runtime verification tool for java

Author:

OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

Pages 306 - 307

https://doi.org/10.1145/1028664.1028776

Published: 23 October 2004 Publication History

Get Access

Abstract

Runtime verification is a special form of runtime testing, employing formal methods and languages. In this work, we utilize next-time free linear-time temporal logic (LTL\textbackslash X) as formal framework. The discipline serves the purpose of asserting certain design-time assumptions about object-oriented (OO) entities such as objects, methods, and so forth. In this paper we propose a linear-time logic over joinpoints \citeLaddad03AspectJ, and introduce a lightweight runtime veri\-fication tool based on this logic, J2SE 5 metadata \citeJSR175 and an AspectJ-based \citeAspectJ runtime backend. Implementations have been proposed so far for imperative and functional languages \citeHuchStolz04a. To our knowledge our approach is the first to allow addressing of entire sets of states, also over subclass boundaries, thus exploiting the OO nature.

References

[1]

Adrian Colyer (IBM), AspectJ project lead. Personal communication, June 2004.

Google Scholar

[2]

AspectJ website. http://www.eclipse.org/aspectj/.

Google Scholar

[3]

Java specification request for metadata annotations (JSR175). http://jcp.org/en/jsr/detail?id=175.

Google Scholar

[4]

R. Laddad. AspectJ in Action: Practical Aspect-Oriented Programming. Manning Publications Co., 2003.

Digital Library

Google Scholar

[5]

V. Stolz and F. Huch. Runtime verification of Concurrent Haskell programs. In Proceedings of the Fourth Workshop on Runtime Verification, to appear in ENTCS. Elsevier Science Publishers, 2004.

Google Scholar

Cited By

View all

Zheng XJulien CPodorozhny RCassez FRakotoarivelo T(2018)Efficient and Scalable Runtime Monitoring for Cyber–Physical SystemIEEE Systems Journal10.1109/JSYST.2016.261459912:2(1667-1678)Online publication date: Jun-2018
https://doi.org/10.1109/JSYST.2016.2614599
Cook BKhlaaf HPiterman N(2017)Verifying Increasingly Expressive Temporal Logics for Infinite-State SystemsJournal of the ACM10.1145/306025764:2(1-39)Online publication date: 30-Apr-2017
https://dl.acm.org/doi/10.1145/3060257
Cook BKhlaaf HPiterman N(2015)On Automation of CTL* Verification for Infinite-State SystemsComputer Aided Verification10.1007/978-3-319-21690-4_2(13-29)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_2
Show More Cited By

Index Terms

A lightweight LTL runtime verification tool for java
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Runtime verification of LTL on lossy traces
SAC '17: Proceedings of the Symposium on Applied Computing

Runtime verification techniques mostly assume the existence of complete execution traces. However, real-world systems often produce lossy traces due to network issues, partial instrumentation, sampling, and logging failures. A few verification ...
Runtime Verification for LTL and TLTL

This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and ...
Model-based Runtime Verification Framework

Model-based runtime verification is an extension to the state-of-the-art runtime verification, aimed at checking at runtime the system implementation against the system model (consistency checking) and the system model against the system specification (...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

October 2004

348 pages

ISBN:1581138334

DOI:10.1145/1028664

Conference Chair:
John Vlissides
IBM Research
,
Program Chairs:
Doug Schmidt
Vanderbilt University
,
Geoff Cohen
Coherence Engine

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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 October 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

OOPSLA04

Sponsor:

OOPSLA04: ACM SIGPLAN Object Oriented Programming Systems and Applications Conference

October 24 - 28, 2004

BC, Vancouver, CANADA

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
466
Total Downloads

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

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zheng XJulien CPodorozhny RCassez FRakotoarivelo T(2018)Efficient and Scalable Runtime Monitoring for Cyber–Physical SystemIEEE Systems Journal10.1109/JSYST.2016.261459912:2(1667-1678)Online publication date: Jun-2018
https://doi.org/10.1109/JSYST.2016.2614599
Cook BKhlaaf HPiterman N(2017)Verifying Increasingly Expressive Temporal Logics for Infinite-State SystemsJournal of the ACM10.1145/306025764:2(1-39)Online publication date: 30-Apr-2017
https://dl.acm.org/doi/10.1145/3060257
Cook BKhlaaf HPiterman N(2015)On Automation of CTL* Verification for Infinite-State SystemsComputer Aided Verification10.1007/978-3-319-21690-4_2(13-29)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_2
Zhao YLi ZShen HMa D(2013)Development of global specification for dynamically adaptive softwareComputing10.1007/s00607-013-0295-395:9(785-816)Online publication date: 1-Sep-2013
https://dl.acm.org/doi/10.1007/s00607-013-0295-3
Sokolsky OHavelund KLee I(2012)Introduction to the special section on runtime verificationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3115971.311616114:3(243-247)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.5555/3115971.3116161
Bauer ALeucker MSchallhart C(2011)Runtime Verification for LTL and TLTLACM Transactions on Software Engineering and Methodology10.1145/2000799.200080020:4(1-64)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1145/2000799.2000800
Alberti MDell'Acqua PPereira L(2011)Observation strategies for event detection with incidence on runtime verificationAnnals of Mathematics and Artificial Intelligence10.1007/s10472-011-9259-562:3-4(161-186)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1007/s10472-011-9259-5
Sokolsky OHavelund KLee I(2011)Introduction to the special section on runtime verificationInternational Journal on Software Tools for Technology Transfer10.1007/s10009-011-0218-614:3(243-247)Online publication date: 29-Nov-2011
https://doi.org/10.1007/s10009-011-0218-6
Noguera CKellens ADeridder DD'Hondt T(2010)Tackling pointcut fragility with dynamic annotationsProceedings of the 7th Workshop on Reflection, AOP and Meta-Data for Software Evolution10.1145/1890683.1890684(1-6)Online publication date: 22-Jun-2010
https://dl.acm.org/doi/10.1145/1890683.1890684
Leye SMazemondet OUhrmacher A(2010)Parallel Analysis with FAMVal to Speed Up Simulation-based Model CheckingProceedings of the 2010 Fourth UKSim European Symposium on Computer Modeling and Simulation10.1109/EMS.2010.63(344-350)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.1109/EMS.2010.63
Show More Cited By

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

Runtime verification of LTL on lossy traces

Runtime Verification for LTL and TLTL

Model-based Runtime Verification Framework