The JPF Core System is a framework to analyze and verify Java bytecode programs. The major component of JPF core is an extensible and runtime-configurable virtual machine (VM) that can be customized with runtime components such as specific instruction sets and plug-ins to observe program execution. The JPF core can store and restore program states, and comes with a configuration that constitutes a standalone software model checker that can be used to detect and analyze concurrency defects in Java applications like deadlocks or data race conditions.
The underlying key capability of the JPF VM is to execute the system under test in many alternative ways, thus achieving significantly better coverage than traditional testing, while providing better insight into execution details. The main design goal of the JPF core framework is its extensibility. It therefore is a suitable basis for creating specialized, runtime-configured verification tools that use the JPF core libraries to perform tasks such as test case generation or user interface model checking.
This work was done by Peter Mehlitz of SGT, Inc. for Ames Research Center. This software is available for use. To request a copy, please visit https://software.nasa.gov/software/ARC-17487-1 .