Marcelo d'Amorim
Klaus Havelund
Abstract
We introduce the temporal logic HAWK and its supporting tool for runtime verification of Java programs. A monitor for a HAWK formula checks if a finite trace of program events satisfies the formula. HAWK is a programming-oriented extension of the rule-based EAGLE logic that has been shown capable of defining and implementing a range of finite trace monitoring logics, including future and past time temporal logic, metric (real-time) temporal logics, interval logics, forms of quantified temporal logics, extended regular expressions, state machines, and others. Monitoring is achieved on a state-by-state basis avoiding any need to store the input trace. HAWK extends EAGLE with constructs for capturing parameterized program events such as method calls and method returns. Parameters can be executing thread, the objects that methods are called upon, arguments to methods, and return values. HAWK allows one to refer to these in formulae. The tool synthesizes monitors from formulae and automates program instrumentation.
- 1st, 2nd, 3rd, and 4th CAV Workshops on Runtime Verification (RV'01 - RV'04), volume 55(2), 70(4), 89(2), 113 of ENTCS. Elsevier Science: 2001, 2002, 2003, 2004.Google Scholar
- Eiffel language, 2005. http://www.eiffel.com/.Google Scholar
- C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Roşu, and W. Visser. Experiments with Test Case Generation and Runtime Analysis. In E. Börger, A. Gargantini, and E. Riccobene, editors, Abstract State Machines (ASM'03), volume 2589 of LNCS, pages 87--107. Springer, March 2003. Google ScholarDigital Library
- H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-Based Runtime Verification. In Proceedings of the 5th International Conference on Verification, Model Chacking, and Abstract Interpretation (VMCAI'04), volume 55(2), 70(4), 89(2) of LNCS, Venice, Italy, Jan 2004. Springer.Google Scholar
- D. Bartetzko, C. Fisher, M. Moller, and H. Wehrheim. Jass-Java with Assertions. In K. Havelund and G. Roşu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01), volume 55 of ENTCS, Paris, France, 2001. Elsevier Science.Google Scholar
- F. Chen, M. d'Amorim, and G. Roşu. A Formal Monitoring-Based Framework for Software Development and Analysis. In Proceedings of ICFEM'04, volume 3308 of LNCS, pages 357--372, 2004.Google ScholarCross Ref
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. Google ScholarDigital Library
- M. d'Amorim and G. Roşu. Efficient Monitoring of ω-languages. to appear in Computer Aided Verification (CAV'05).Google Scholar
- D. Drusinsky. The Temporal Rover and the ATG Rover. In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 323--330. Springer, 2000. Google ScholarDigital Library
- D. Gabbay. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In Proceedings of the 1st Conference on Temporal Logic in Specification, Altrincham, April 1987, volume 398 of LNCS, pages 409--448, 1989. Google ScholarDigital Library
- K. Havelund and G. Roşu. Monitoring Java Programs with Java PathExplorer. In Proceedings of the 1st International Workshop on Runtime Verification (RV'01) {1}, pages 97--114. Extended version to appear in the journal: Formal Methods in System Design, Kluwer, 2004.Google Scholar
- G. Kiczales and et al. Aspect-Oriented Programming. In ECOOP, volume 1241. Springer-Verlag, 1997.Google ScholarCross Ref
- G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An Overview of AspectJ. In Proceedings of the 15th ECOOP, Lecture Notes in Computer Science, pages 327--353. Springer-Verlag, 2001. Google ScholarDigital Library
- M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-MaC: a Run-time Assurance Tool for Java. In Proceedings of Runtime Verification (RV'01), volume 55 of ENTCS. Elsevier Science, 2001.Google Scholar
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992. Google ScholarCross Ref
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, New York, 1995. Google ScholarDigital Library
- R. Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, New York, 1992. Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. Google ScholarDigital Library
Index Terms
- Event-based runtime verification of java programs
Recommendations
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 ...
Event-based runtime verification of java programs
WODA '05: Proceedings of the third international workshop on Dynamic analysisWe introduce the temporal logic HAWK and its supporting tool for runtime verification of Java programs. A monitor for a HAWK formula checks if a finite trace of program events satisfies the formula. HAWK is a programming-oriented extension of the rule-...
An Overview of the Runtime Verification Tool Java PathExplorer
We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. ...
Comments