Abstract
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 language | English (US) |
---|---|
Pages (from-to) | 189-215 |
Number of pages | 27 |
Journal | Formal Methods in System Design |
Volume | 24 |
Issue number | 2 |
DOIs | |
State | Published - Mar 2004 |
Keywords
- 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