What is JPF?
JPF is a highly extensible Java Virtual Machine purpose-built for software verification. You can think of it as a “a debugger toolbox on steroids”: first it automatically executes your program in all possible ways to find defects you don’t even know about yet, then it explains to you what caused these defects.
The Core: A VM that supports Model Checking
The JPF core is a Virtual Machine (VM) for Java™ bytecode, which means it is a program which you give Java programs to execute. It is used to find defects in these programs, so you also need to give it the properties to check for as input. JPF gets back to you with a report that says if the properties hold and/or which verification artifacts have been created by JPF for further analysis (like test cases).
JPF is a VM with several twists. It is implemented in Java itself, so don’t expect it to run as fast as your normal Java. It is a VM running on top of a VM.While execution semantics of Java bytecodes are clearly defined, we have little hardwired semantics in JPF - the VM instruction set is represented by a set of classes that can be replaced.
The default instruction set makes use of the next JPF feature: execution choices. JPF can identify points in your program from where execution could proceed differently, then systematically explore all of them. This means JPF (theoretically) executes all paths through your program, not just one like a normal VM. Typical choices are different scheduling sequences or random values, but again JPF allows you to introduce your own type of choices like user input or statemachine events.
The number of paths can grow out of hand, and it usually will. This is what software model checking calls the state explosion problem. The first line of defense employed by JPF is state matching: each time JPF reaches a choice point, it checks if it has already seen a similar program state, in which case it can safely abandon this path, backtrack to a previous choice point that has still unexplored choices, and proceed from there. That’s right, JPF can restore program states, which is like telling a debugger “go back 100 instructions”.
One additional feature that comes in handy in case JPF finds a defect is the availability of the complete execution history that leads to the bug, down to every executed bytecode instruction if you need it. We call this a program trace, and it is invaluable to find out what really caused the defect. Think of a deadlock - usually there is not much you can directly deduce from a snapshot of call stacks.
Caveat: not a lightweight tool
Of course that is the ideal world. In reality, this can require quite a lot of configuration and even some programming. JPF is not a “black box” tool like a compiler, and the learning curve can be steep. What makes this worse is that JPF cannot execute Java libraries that make use of native code. Not because it doesn’t know how to do that, but because it often doesn’t make sense: native code like system calls to write to a file cannot easily be reverted - JPF would loose its capability to match or backtrack program states.
So what makes it worthwhile to invest in JPF? First, if you are looking for a research platform to try out your new software verification ideas, chances are you can get along with JPF in a fraction of time compared to native production VMs, which are typically optimized towards speed and care little about extensibility or observability. The second answer is that - as of this writing - there are bugs only JPF can find (before the fact, that is), and there are more and more Java applications that cannot afford to learn about these bugs after the fact. JPF is a tool for mission critical applications, where failure is not an option. No surprise it was started by NASA.