Monitoring Java Programs with Java PathExplorer

By Klaus Havelund, Grigore Roşu. RV@CAV, 2001

310 citations recorded by the source corpus.

We present recent work on the development of Java PathExplorer (\JPaXX), a tool for monitoring the execution of Java programs. \JPaX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems. The tool facilitates automated instrumentation of a program''s byte code, which will then emit events to an observer during its execution. The observer checks the events against user provided high-level requirement specifications, for example temporal logic formulae, and against lower level error detection procedures, usually concurrency related such as deadlock and data race algorithms. High level requirement specifications together with their underlying logics are defined in rewriting logic using Maude, and then can either be directly checked using Maude rewriting engine, or be first translated to efficient data structures and then checked in Java.

Subfields: Computer Networks and Communications, Software

View Paper: https://www.semanticscholar.org/paper/3299d2d70ea946bfa066cf01c7eb0a14ed95c830

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computer Networks and Communications

In Software

Citations in the corpus

A brief account of runtime verification (2009, background): “Correctness properties specify the form of individual executions of a system and are usually formulated in some variant of linear temporal logic, such as LTL [51], as seen for example in [35,32,31,37,38,60].”
Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications (2018, methodology): “For instance, the presence of unbounded until operators in the specification can potentially require a large lookahead to resolve the truth of the formula appropriately [39,66,70].”
Synthesizing Monitors for Safety Properties (2002, methodology): “Since we don’t want to count on an optimizing compiler, we prefer to store the boolean formula as some kind of binary decision diagram, more precisely, as a term over the operation ? : , for example, pre[3] ? pre[2] ? now[3] : q(state) : pre[2] ? 1 : q(state) (see [9] for a formal definition).”
Mop: an efficient and generic runtime verification framework (2007, methodology): “All these runtime verification systems work in outline monitoring mode and have hardwired spec- ification languages: MaC uses a specialized language based on interval temporal logic, JPaX supports just LTL, and Eagle adopts a fixed-point logic.”
Rule-Based Runtime Verification (2004, methodology): “Our own previous work includes the development of several algorithms, such as generating dynamic programming algorithms for past time logic [14], using a rewriting system for monitoring future time logic [12, 13], or generating Büchi automata inspired algorithms adapted to finite trace LTL [11].”