Abstract
We present recent work on the development of Java PathExplorer (JPaX), 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.
Original language | English (US) |
---|---|
Pages (from-to) | 200-217 |
Number of pages | 18 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 55 |
Issue number | 2 |
DOIs | |
State | Published - Oct 2001 |
Externally published | Yes |
Event | RV'2001, Runtime Verification (in Connection with CAV '01) - Paris, France Duration: Jul 23 2001 → Jul 23 2001 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science