Installation

In order to use JPF, you need to install a current version of the Java 7 Development Kit (JDK). You can find an installer on Oracle’s website

With the JDK in place, installing the JPF VM is as simple as downloading the binary package and extracting the contents into a folder of your choice.

Using JPF: A random example

We start with a simple example that uses java.util.Random. Consider the following program that obtains two random values in (2) and (3), and then performs some computation (4) with them. Copy the following code into a file called Rand.java, in the same folder as where the contents of the binary package were extracted:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import java.util.Random;

public class Rand {
    public static void main (String[] args) {
        Random random = new Random(42);      // (1)
         
        int a = random.nextInt(2);           // (2)
        System.out.println("a=" + a);
         
        //... lots of code here
          
        int b = random.nextInt(3);           // (3)
        System.out.println("  b=" + b);
         
        int c = a/(b+a -2);                  // (4)
        System.out.println("    c=" + c);         
    }
}

You can can then compile the code to produce a class file:

> javac Rand.java

Next, copy the following code to a file called Rand.jpf in the same directory:

target=Rand

classpath=./
sourcepath=./

Testing

Executing this program with a normal Java VM yields something like the following output. If we don’t provide an explicit seed when creating the Random object in (1), the result is going to differ between runs, but every run will choose just a single ‘a’ and ‘b’ value (i.e. print just a single “a=..” and “b=..” line.

> java Rand
a=1
  b=0
    c=1
>

Let’s look at a graphical representation of all the ways our program could be executed, and how it actually was executed in our test run. The nodes of the graph represent “program states”, and the edges “transitions” the execution could take from a certain state.

Model Checking

Enter JPF - not much different results if we start JPF as a plain ‘java’ replacement. The only difference is that it (a) takes longer to complete, and (b) tells us something about a “search”, which hints on that something more than in our test run is going on:

> java -jar ./RunJPF.jar Rand.jpf
JavaPathfinder v7.0 (rev ${version}) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
Rand.main()

====================================================== search started: 8/27/14 12:24 PM
a=1
  b=0
    c=-1

====================================================== results
no errors detected

>

What is this “search” supposed to mean? Looking at source line (4) we realize that there is a potential problem: for certain ‘a’ and ‘b’ values, this expression can cause a “division by zero” ArithmeticException. Depending on the random seed used in (1), it’s quite possible we would never encounter this case if we run (i.e. test) the program with a normal JVM.

Re-enter JPF - but this time we tell it to not only consider single values for ‘a’ and ‘b’, but look at all possible choices:

> java -jar ./RunJPF.jar +cg.enumerate_random=true Rand
JavaPathfinder v7.0 (rev ${version}) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
Rand.main()

====================================================== search started: 8/27/14 12:29 PM
computing c = a/(b+a - 2)..
a=0
  b=0       ,a=0
=>  c=0     , b=0, a=0
  b=1       ,a=0
=>  c=0     , b=1, a=0
  b=2       ,a=0

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
    at Rand.main(Rand.java:16)
....
>

What has happened? By specifying “+vm.enumerate_random=true” we told JPF to consider all possible values for expressions (2) and (3). JPF starts with “a=0”, then picks “b=0”, which yields a valid “c=0” value. But instead of terminating like a normal VM, JPF recognized that there are more choices left, so it “backtracks” to (3) and picks “b=1”. Again, no problem here with computing “c=0”. Back to (3), JPF now tries “b=2”, which of course spells disaster for our little program when executing (4), as can be seen by the following error report.

Here is a graphical representation of this search process. It should be noted that JPF per default only runs up to the point where it finds an error or there are no more choices left to explore. But if we would somehow “fix” the “a=0,b=2” case, JPF would still find the “a=1,b=1” case in the next run, since it systematically tries all choices. No matter what error it finds, JPF also keeps the complete “trace” (execution path) how it got to this error (denoted by the red arrows), which means we don’t have to debug the program to find out.

Note: This tutorial is a slightly modified version of the random example from the original JPF wiki.