An Overview of the Runtime Verification Tool Java PathExplorer

Klaus Havelund, Grigore Roşu

Research output: Contribution to journalArticlepeer-review


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. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into automata or algorithms that can efficiently check the event stream. 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.

Original languageEnglish (US)
Pages (from-to)189-215
Number of pages27
JournalFormal Methods in System Design
Issue number2
StatePublished - Mar 2004


  • Automata
  • Data races
  • Deadlocks
  • Dynamic programming
  • Java
  • Maude
  • Program instrumentation
  • Rewriting logic
  • Runtime verification
  • Temporal logic
  • Trace analysis

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'An Overview of the Runtime Verification Tool Java PathExplorer'. Together they form a unique fingerprint.

Cite this