JPF是什么
首先并不存在单一的完整的JPF，它由多个可配置的不同组件组成，是一个可扩展的框架。Jpf-core是所有其他组件所共同依赖的。
JPF的特征
l Explict State model checking是JPF的基本运行模式。也就是说JPF会跟踪局部变量、堆栈对象和线程状态的具体值。
l Symbolic Execution意味着JPF可以使用符号值来执行程序，当然它也能混合具体及符号执行。
l State Matching是避免不必要工作的关键机制。它会检查每一个新产生的状态之前是否碰到过，如果是就没必要继续沿着当前的路径执行了。同时它能回溯到最近的未被搜索的不确定性选择。
l Backtracking指的是JPF能恢复到先前的执行状态，来检查是否还有未被搜索的选择，这与重复执行程序而言，回溯机制的效率是非常有优势的。
l Partial order Reduction意味着JPF能最小化不同线程间的上下文切换。这是在运行时完成的，也就是不需要预先的分析或者在程序中添加标记，而是通过检查那些可能会对进程间操作有影响的指令来完成的。
JPF的灵活性体现在以下几个方面：
- 搜索策略：控制状态空间的搜索次序
- 监听器：监控并与JPF的执行交互
- Native peers：在主机VM层建构库并执行代码
- Bytecode factories：支持不同的执行模型，如符号执行
- Publisher：生成特定的报告
JPF-CORE
它是支持Model Checking的一个VM，被用来检测程序中的缺陷。输入java字节码程序和待检测的特征（配置文件指定）,输出一个验证报告（如特征是否满足或者可以用来进行进一步分析的非直接的验证结果）。它与JVM的区别在于，其构建于JVM基础之上，并能够识别出会导致程序做出不同执行的点，也就是说它能执行程序中所有可能的路径，而JVM只能执行一条。
JPF不需指定任何的特征就可以检测能被VM识别的缺陷，如死锁(Deadlock)和未被处理的异常(Unhandled Exception,包括assert等)，我们称这些特征为非功能性特征(Non-functional properties)，这些特征是任何应用程序都不该违反的。
当然，JPF并不止于此，我们也可以定义自己的特征，这通常是通过listener来实现的，这些listener可以监控JPF执行的所有动作，如每一条指令的执行、对象的创建、新的程序状态的到达等等。一个典型的例子就是race detector，它是基于监听器来实现的特征，用于检测并行程序中对共享变量的不同步的访问。
另外，JPF找到缺陷时，它还能给出会导致这个缺陷的完整的执行历史，精确到每一个字节码语句，也就是程序trace，它对于分析缺陷的根源是十分重要的。
当然，JPF也有它的缺点。它不是一个轻量的工具，它的学习曲线非常陡峭。并且它不能用于分析使用了本地代码的java库，因为像写文件这类系统调用是不容易恢复的，这使得JPF失去了匹配以及回溯程序状态的能力。当然也存在解决方法，就是利用”native peers”和”model classes”。Natvie peers就是包含可以代替本地方法的方法的类，它们在JVM中被执行，而不是在JPF中被执行。Model classes则是标准类的简单替代，使其可以支持监控及回溯。还有就是JPF目前不支持java.io和java.net。
当然JPF还是值得研究的，它可以作为一个测试新的软件验证方法的研究平台，因为它比JVM具有更好的可扩展性和可观测性。还有就是有些只有JPF才能发现的缺陷，它是针对任务关键系统的分析工具，这也是难怪它的研究最初由NASA启动。