JPAX 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: Maude; Bandera; Java PathFinder; veriSoft; Java-MaC; NuSMV; SPIN; Jass; LLVM; Spec#; Eiffel; CESAR; ADL; SLAM; Copilot; FoCs; Java-MOP; AMT; Z; JML Cited in: 21 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year An overview of the runtime verification tool Java PathExplorer. Zbl 1073.68549Havelund, Klaus; Roşu, Grigore 2004 all top 5 Cited by 52 Authors 7 Roşu, Grigore 4 Havelund, Klaus 3 Sen, Koushik 2 Artho, Cyrille 2 Lowry, Mike 2 Păsăreanu, Corina S. 2 Visser, Willem 1 Aceto, Luca 1 Achilleos, Antonis 1 Agha, Gul A. 1 Anastasiadi, Elli 1 Arts, Thomas 1 Barringer, Howard 1 Bonakdarpour, Borzoo 1 Brauer, Jörg 1 Chauhan, Himanshu 1 Chen, Feng 1 Claessen, Koen 1 Drusinsky, Doron 1 Duan, Zhenhua 1 Fischmeister, Sebastian 1 Függer, Matthias 1 Garg, Vijay K. 1 Godefroid, Patrice 1 Ingólfsdóttir, Anna 1 Jones, Kevin D. 1 Khurshid, Sarfraz 1 Konrad, Victor 1 Leucker, Martin 1 Markey, Nicolas 1 Martí-Oliet, Narciso 1 Meseguer Guaita, José 1 Mittal, Neeraj 1 Möller, Michael 1 Natarajan, Aravind 1 Navabpour, Samaneh 1 Nickovic, Dejan 1 Olderog, Ernst-Rüdiger 1 Rasch, Holger 1 Reinbacher, Thomas 1 Sabry, Amr 1 Schallhart, Christian 1 Schnoebelen, Philippe 1 Svensson, Hans 1 Swords, Cameron 1 Tian, Cong 1 Tobin-Hochstadt, Sam 1 Viswanathan, Mahesh 1 Washington, Rich 1 Wehrheim, Heike 1 Yang, Kai 1 Zhang, Nan all top 5 Cited in 8 Serials 4 Theoretical Computer Science 4 Formal Methods in System Design 1 Information Processing Letters 1 Programming and Computer Software 1 Formal Aspects of Computing 1 Journal of Functional Programming 1 The Journal of Logic and Algebraic Programming 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 21 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year