what is JPF?
JPF 的功能取决于你如何去配置它，首先，没有一个单一的JPF，它是运行时配置的不同组件的组合。JPF的设计使其易于扩展。因此，我们在此仅限于说明jpf core是什么，但是请记住这只是jpf组建中最主要的一部分而已。
The Core : a VM that supports Model Checking （核心：支持模型检查的VM）
JPF内核是用于解释Java™字节码的虚拟机(VM)，这意味着它是一个可以执行java程序的程序。它用于查找这些程序中的缺陷，因此您还需要提供属性来作为输入检查。
JDF基于java实现，所以不要期望他可以有java虚拟机一样运行速度。他是一个运行在java虚拟机上的虚拟机。java的语法已经定义在Sun's Java Virtual Machine Specification中，我们在JPF中几乎没有固定的语义-VM指令集由一组可替换的类表示。
JPF使用下面的特征来设定默认的指令集：execution choices（执行选项） JPF可以从不同的执行过程中识别出程序中的点，然后系统地探索所有这些点。这意味着JPF(理论上)通过程序执行所有路径，不像普通的java虚拟机。特定的选择是不同的调度序列或随机值。但是，JPF允许您介绍您自己的选择，如用户输入或状态事件。
路径的数量可能会失控，而且它通常会。这就是软件模型检查所称的 状态爆炸问题(state explosion problem)。所以JPF采用的第一套办法就是 状态匹配(state matching)每当JPF到达一个选择点，都会检查是否已经有了相似的程序状态，在这种情况下，它可以安全地放弃这条执行序列，回溯到以前的尚未被探索的选择点，然后从那里出发。没错，JPF可以恢复程序状态，这就像告诉调试器“回溯100个指令”一样。
那么这些特性是用来做什么的呢？通常是要在程序中找到要验证的缺陷，是什么样的缺陷呢？现在你应该知道答案了：这取决于你如何配置JPF。JPF-core 检测可以有VM检测出的缺陷，并且不需要你指定任何缺陷属性：死锁和未处理的异常（包括java assert 表达式） ，我们称这些为非函数特性，任何应用程序都不应违反它们。但是JPF并不仅仅限于此--您可以定义您自己的属性，通常用 listener 来完成，一个可以让您密切监视JPF所采取的所有操作的“小插件”，比如执行单个指令，创建对象，达到一个新的程序状态等等。这样一个典型的listener实现的本质是一个竞争检测器，它标识并发程序中对共享变量的不同步访问(JPF核心包括其中的两个)。
另外一个有用的特性是，如果JPF发现了缺陷JPF可以获得导致错误的完整执行历史的记录，如果您需要的话，可以执行每个执行的字节码指令。我们称之为 程序跟踪（trace） ，发现缺陷的真正原因是无价的。拿死锁来说——通常没有多少可以直接从调用堆栈快照中推断出来。
所有的这些解释了为什么JPF被称为 开挂的调试工具箱（a debugger toolbox on steroids）首先，它会以所有可能的方式自动执行程序，以找到甚至您还不知道的缺陷，然后它解释了你造成这些缺陷的原因。
Caveat : not a lightweight tool （警告：不是一个轻量级的工具）
当然，那是理想的状态。实际上，这可能需要相当多的配置，甚至需要一些编程。jpf不是像编译器那样的“黑盒（black box）”工具，学习曲线可能很陡峭。更糟的是JPF不能执行利用本地代码的java库。不是因为它不知道怎么做，而是因为这样做通常没有意义：本机代码类似于系统调用来写入文件不易恢复-JPF将失去其匹配或回溯程序状态的能力。当然还有有补救办法，而且是可配置的：native peers 和 model classes 。native peers 是具有用来代替真实本地方法的方法的类。这个代码是由真正的java虚拟机执行，不是JPF，因此，它可以提升运行速度。model classes 是标准类的简单替换，像java.lang.Thread这为完全可观察和可回溯的本机方法提供了可选方案。
如果您熟悉java实现，你知道的包含库的巨大的比例，很明显，我们不能处理所有这些问题，至少现在不能。没有理论上的限制，实现缺失的库方法通常是非常容易的。但是你应该准备好面对UnsatisfiedLinkErrors比如你让JPF运行大的生产系统。臭名昭著的白点是 java.io 和 java.net ，但也有人在做这方面的工作。谁知道呢，也许你也有兴趣加入这项工作-JPF是开源的，没有什么是你不可以看到的。我们现在有二十多个行业的主要合作者，世界各国政府和学术界。
那么，是什么使投资jpf值得呢？毕竟，它是一个重量级的工具。不是一个快速简单的bug查找器。首先，如果你正在寻找一个研究平台来尝试你的新软件验证思想，chances are you can get along with JPF in a fraction of time compared to native production VMs，它们通常是针对速度而优化的，很少考虑可扩展性或可观察性。第二个答案是，如这篇文章所写的，有些bug只有JPF才能找到(before the fact,that is)，而且还有越来越多的Java应用程序无法在事实之后了解这些错误。JPF是一个针对关键应用的程序，在这些程序中，失败是不能容忍的。这也就不奇怪，JPF是由美国宇航局发起的。
