jpf-core代码解析 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启动。 本文来源：https://www.wddqw.com/doc/2203fb0013661ed9ad51f01dc281e53a58025132.html