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.

References in zbMATH (referenced in 30 articles , 1 standard article )

Showing results 1 to 20 of 30.
Sorted by year (citations)

1 2 next

  1. Aceto, Luca; Achilleos, Antonis; Anastasiadi, Elli; Ingolfsdottir, Anna: Axiomatizing recursion-free, regular monitors (2022)
  2. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  3. Swords, Cameron; Sabry, Amr; Tobin-Hochstadt, Sam: An extended account of contract monitoring strategies as patterns of communication (2018)
  4. Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan: A compiler for MSVL and its applications (2018)
  5. Natarajan, Aravind; Chauhan, Himanshu; Mittal, Neeraj; Garg, Vijay K.: Efficient abstraction algorithms for predicate detection (2017)
  6. Reinbacher, Thomas; Függer, Matthias; Brauer, Jörg: Runtime verification of embedded real-time systems (2014)
  7. Bonakdarpour, Borzoo; Navabpour, Samaneh; Fischmeister, Sebastian: Time-triggered runtime verification (2013)
  8. Sapozhnikov, A.: Automation of the construction of models of normal program behavior (2012)
  9. Jones, Kevin D.; Konrad, Victor; Ničković, Dejan: Analog property checkers: a DDR2 case study (2010)
  10. Leucker, Martin; Schallhart, Christian: A brief account of runtime verification (2009)
  11. Liang, Hui; Dong, Jin Song; Sun, Jing; Wong, W. Eric: Software monitoring through formal specification animation (2009) ioport
  12. Fraser, Gordon; Wotawa, Franz: Using model-checkers to generate and analyze property relevant test-cases. (2008) ioport
  13. Möller, Michael; Olderog, Ernst-Rüdiger; Rasch, Holger; Wehrheim, Heike: Integrating a formal method into a software engineering process with UML and Java (2008)
  14. Elbaum, Sebastian; Kanduri, Satya; Andrews, Anneliese: Trace anomalies as precursors of field failures: An empirical study (2007) ioport
  15. Markey, Nicolas; Schnoebelen, Philippe: Mu-calculus path checking (2006)
  16. Sen, Koushik; Roşu, Grigore; Agha, Gul: Online efficient predictive safety analysis of multithreaded programs (2006) ioport
  17. Artho, Cyrille; Barringer, Howard; Goldberg, Allen; Havelund, Klaus; Khurshid, Sarfraz; Lowry, Mike; Pasareanu, Corina; Roşu, Grigore; Sen, Koushik; Visser, Willem; Washington, Rich: Combining test case generation and runtime verification (2005)
  18. Arts, Thomas; Claessen, Koen; Svensson, Hans: Semi-formal development of a fault-tolerant leader election protocol in Erlang (2005)
  19. Chen, Feng; Roşu, Grigore: Java-MOP: A monitoring oriented programming environment for Java (2005)
  20. Giannakopoulou, Dimitra; Păsăreanu, Corina S.; Barringer, Howard: Component verification with automatically generated assumptions (2005) ioport

1 2 next