swMATH ID: 9906
Software Authors: Havelund, Klaus; Roşu, Grigore
Description: 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. 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.
Homepage: http://ti.arc.nasa.gov/m/pub-archive/archive/0262.pdf
Keywords: runtime verification; trace analysis; temporal logic; rewriting logic; Maude; automata; dynamic programming; program instrumentation; deadlocks; data races; Java
Related Software: Java PathFinder; Maude; Bandera; veriSoft; Java-MaC; Copilot; NuSMV; SPIN; Jass; LOLA; LTL2BA; LearnLib; Coq; LLVM; Spec#; Eiffel; SLAM; CESAR; ADL; FoCs
Cited in: 25 Documents

Citations by Year