Java Pathfinder

Java Pathfinder

Developer(s)	NASA
Stable release	6.0 / November 30, 2010 (2010-11-30)
Written in	Java
Operating system	Cross-platform
Size	1.6 MB (archived)
Type	Model checking
License	NASA Open Source Agreement version 1.3
Website	http://babelfish.arc.nasa.gov/trac/jpf

Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project.

The core of JPF is a Java Virtual Machine that is also implemented in Java. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for test case generation (using symbolic execution), program inspection, runtime monitoring and program instrumentation. JPF has no fixed notion of state space branches and can handle both data and scheduling choices.

The input of JPF consists of Java Class files of the System under test, and configuration files to specify the main class to execute, the program properties to verify and the report to generate.

Example

The following system under test contains a simple race condition that leads to a division by zero if statement (1) is executed before (2)

public class Racer implements Runnable {
     int d = 42;

     public void run () {
          doSomething(1001);
          d = 0;                              // (1)
     }

     public static void main (String[] args){
          Racer racer = new Racer();
          Thread t = new Thread(racer);
          t.start();

          doSomething(1000);
          int c = 420 / racer.d;              // (2)
          System.out.println(c);
     }
     
     static void doSomething (int n) {
          try { Thread.sleep(n); } catch (InterruptedException ix) {}
     }
}

Executing this program with JPF will produce the following output, explaining the error and showing a counter example leading to the error

JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: Racer.java
...
====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field Racer@13d.d
  main at Racer.main(Racer.java:16)
		"int c = 420 / racer.d;               "  : getfield
  Thread-0 at Racer.run(Racer.java:7)
		"d = 0;                               "  : putfield

====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
...
------------------------------------------------------ transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sleep",isCascaded:false,{main,>Thread-0}]
      [3 insn w/o sources]
  Racer.java:22                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  Racer.java:23                  : }
  Racer.java:7                   : d = 0;                      
...
------------------------------------------------------ transition #5 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sharedField",isCascaded:false,{>main,Thread-0}]
  Racer.java:16                  : int c = 420 / racer.d;

Extensibility

JPF is an open system that can be extended in a variety of ways. The main extension constructs are

• listeners - to implement complex properties (e.g. temporal properties)
• peer classes - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods
• bytecode factories - to provide alternative execution semantics of bytecode instructions (e.g. to implement symbolic execution)
• publishers - to produce different output formats
• search policies - to use different program state space traverse algorithms

JPF includes a runtime module system to package such extensions into separate projects. A number of such projects are available from the main JPF server, including a symbolic execution mode, numeric analysis, race condition detection for relaxed memory models, user interface model checking and many more.

Limitations

• JPF cannot analyze Java native methods. If the system under test calls such methods, these have to be provided within peer classes, or intercepted by listeners
• as a model checker, JPF is susceptible to Combinatorial explosion, although it performs on-the-fly Partial order reduction
• the configuration system for JPF modules and runtime options can be complex

See also

• Bogor - software model checking framework of Kansas State University
• MoonWalker - similar to Java PathFinder, but for .NET programs instead of Java programs
• McErlang - model checker for Erlang programs

External links

• Official site
• New NASA Software Detects 'Bugs' in Java Computer Code
• NASA Develops New Software to Detect "Bugs" in Java Computer Code
• Willem Visser, Corina S. Păsăreanu, Sarfraz Khurshid. Test Input Generation with Java PathFinder. In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. ISBN 1-58113-820-2.