JPF components
Java™不仅仅是一种编程语言。它是一组层，从特定于平台的VM实现开始 ("host VM"),它位于为您的操作系统编写和使用的本机库之上。在这个结构上，我们添加了JPF --- 一个运行在 Host VM上的java应用程序，但是它本身是一个虚拟机用来执行你的被测系统（SUT）。
所有这些递归,对于java代码到底是在那个水平进行处理这是容易混淆的。更糟的是，大多书的标准库类文件（java.*classes）和一些注解同时被两个虚拟机运行，当然，在不同的实例。本页的目的是了解代码与系统的不同层和部件相关的一些指示灯。
为了进一步的说明，我们退一步，看看在将JPF应用在SUT上时使用到了哪些组件。我们从两个方面对组件进行分类：
processing VM (host VM, JPF)
associated distribution entity 关联分布实体(host Java installation, JPF core, JPF extensions, SUT)
还记得what is jpf中的介绍图吗？下面这个图更详细一点：
让我们从左往右看这幅图，我们从要验证的编译后的java应用程序开始，这当然不是JPF一部分，但是要通过JPF来执行。因此，相应的类文件不必在主机VM中可见（因为运行在JPF上）。但是，应用程序代码可能使用驻留在JPF发行版中的类和接口（例如框架的UML状态图建模，或验证相关的注释类型从JPF APROP扩展）。同时，应用程序和这些建模库和/或注释形成被测试系统(SUT)。
接下来是JPF核心本身，现在我们知道这是一个用java写的虚拟机，所以你可以运行在任何装有java的系统上。这意味着构成JPF的所有类都必须对“主机jvm”可见。例如，通过设置CLASSPATH环境变量(这不是建议的方法)。
下面是重要的一部分：JPF不是一个单一的系统。它使用各种配置的组件来执行以下任务：
- property implementation
- library modeling
- report generation
除此之外还有更多，即使你在运行时不指定任何东西，Jpf将使用默认配置，该配置将引入许多组件，如监听器listener。它们不必是JPF核心的一部分，但可以驻留在它们自己的JPF扩展模块中。
如果您确实指定了自己的配置，您可以告诉JPF使用位于JPF核心发行版之外的组件，无论是在已安装的JPF扩展模块中还是在您自己的项目中。无论哪种方式，所有这些 listeners, native peers, publishers和其他组件都处于整个JPF系统的运行时部分，因此它们需要在主机VM中可见。
最后一部分是最棘手的部分，您的应用程序很可能使用标准java库（e.g. System.out.println()。当jpf执行sut时，一些标准库类必须替换为jpf特定的版本（例如，类如java.lang.classthat有本地方法），不过JPF有一个特殊的MJI机制来实现这一点。然而，大多数标准库类都有纯java实现，我们可以从主机JVM的安装中直接获取这些。
JPF保持关联的类路径分离。在JPF配置中有三种不同的路径设置：
- native_classpath --- 这包括必须对主机vm可见的所有内容，主要包括JPF本身的类，listeners, native peers和bytecode instruction sets。
The native_classpath is dynamically constructed from your site.properties and jpf.properties configuration files during JPF startup, and processed by the JPF classloader
- classpath --- 这包括由JPF执行的类。
- sourcepath --- 取决于必须由JPF生成的报告,它可能必须为执行的类文件(字节码)查找SUT和库源。这就是如何告诉JPF这些源位于何处。
可以从应用程序属性文件或命令行显式地设置这些路径列表，但是最好让JPF在处理JPF组件的JPF.properties文件时收集它们，这些文件都包括类似的行：
<jpf-module>.native_classpath = .. </br>
<jpf-module>.classpath = .. </br>
<jpf-module>.sourcepath = .. </br>
警告：如果--在启动JPF期间--您会遇到如下消息:
...
[SEVERE} error during VM runtime initialization: wrong model classes (check 'classpath')
这意味着CLASSPATH设置是错误的，jpf加载了一些必须用自己的版本替换的标准库类。they need to be modeled (like java.lang.Thread, java.lang.Class and others - all part of jpf-classes.jar within the jpf-core module).
This can also happen later-on with less essential library classes that are not part of jpf-core, but should be loaded from one of the installed extensions. In this case, this usually shows up as an UnsatisfiedLinkError
