Java Pathfinder (JPF) 完全安装配置过程

Java Pathfinder(JPF)完全安装配置过程(2013年6月)

Java PathFinder是一个可执行Java程序调试/检验系统。它的内核是一个Java虚拟机(JVM)，可用于系统地探测程序所有可能的执行路径，以避免死锁或无法处理的异常之类的情况发生。与传统的调试程序不同，Java PathFinder报告导致缺陷的整个执行路径。Java

PathFinder特别适合在多线程的程序中发现很难测试的并发缺陷。

一、前言

本文所介绍的JPF安装配置过程，主要参考JPF官方网站，并以Windows操作系统、Eclipse开发平台为基础进行配置。如使用Mac OS X等其它操作系统或NetBeans等其它开发平台的用户，安装配置过程有所差异，详细介绍请查阅官网。

官网：/trac/jpf/

二、系统需求及前提

Java SE Development Kit (JDK) 版本1.6 (6.0) 以上

Eclipse 版本3.5 (Galileo) 以上

最少2Gb内存

Java运行设置-Xmx1024m以上

三、辅助软件的下载与安装

1、JDK

官网：/technetwork/java/javase/downloads/

到官网或通过其它途径下载JDK，保证下载的版本为1.6（6.0）以上，并完成JDK的安装。

安装完成后需进行Java的相关配置。为保证JPF的命令行操作（cmd模式）和Eclipse能够顺利执行，至少需完成环境变量Java_Home的设置。

依次点击：“我的电脑”(右键)－“属性”－“高级”－“环境变量”，弹出Windows的“环境变量”配置卡，在“系统变量”中进行相关配置。Java_Home指向你的JDK安装目录，如：C:Program FilesJavajdk1.6.0_23，请根据你的实际目录进行设置。其它环境变量如：path、classpath，仅对JPF而言无需设置。

2、Eclipse

官网：/downloads/

到官网或通过其它途径下载Eclipse，保证下载的版本为3.5（Galileo）以上，并完成Eclipse的安装。

3、TortoiseHg

官网：

如果要下载JPF的相关组件，必须要使用一个名叫Mercurial的分布式版本控制系统。对于Windows类的操作系统，可以使用TortoiseHg，它是Mercurial

1

的可视化客户端工具，操作起来更为简便。

到官网或通过其它途径下载TortoiseHg，并完成TortoiseHg的安装。由于网上关于TortoiseHg的介绍和资源比较少，对于英文较为生疏的朋友，推荐一个汉化版TortoiseHg的下载网址：/soft/，经测试可正常使用。

四、JPF相关组件的下载

JPF的相关组件可以通过Mercurial提供的“clone”操作进行下载，各个组件资源都存储在/hg/jpf这一根目录下。你可以选择你想使用的某个组件进行clone，如：/hg/jpf/jpf-core，而不是根目录../hg/jpf，以确保所下载组件的完整性和准确性。因为如果使用根目录clone，所下载的并不是JPF的全部组件，有些仅仅是一个空文件夹而已。不过，我们倒是可以利用这一方法，来看一看整个JPF的组件资源究竟如何构成。

JPF core对于JPF来说是核心组件，也是唯一一个必须要下载的组件。我们使用Mercurial的可视化客户端TortoiseHg来进行下载。

在自己希望保存JPF组件的目录下新建一个名为jpf-core的文件夹（建议使用默认路径存放所下载的组件，默认路径的介绍请参见第五部分），右键点击文件夹，在弹出菜单里选择TortoiseHg->Clone，在弹出对话框的“源”选项中输入需要安装的JPF组件的URL，JPF core在Mercurial repository中的安装路径为：/hg/jpf/jpf-core，然后开始下载，在一段时间的等待之后，JPF core这个组件就成功下载到本地了。

可以使用类似的方法下载JPF其它组件，主要区别在于URL的不同，但其组成都是根目录+组件名的方式，即../hg/jpf/[组件名]。建议下载时保存的文件夹名称和组件名一致。初次使用JPF，只需下载JPF core即可。

五、创建ties文件

ties文件告诉JPF在初始化时去哪里寻找所下载的JPF组件，所以必须由用户亲自编辑，添加各个组件的地址路径。ties属于java编程中常用的properties文件，是一种配置文件，主要用于表达配置信息，文件类型为*.properties，格式为文本文件，文件的内容是格式是“键=值”的键值对格式。

以下是一个ties文件的实例：

# JPF site configuration

jpf-core = ${}/projects/jpf/jpf-core

# numeric extension

jpf-numeric = ${}/projects/jpf/jpf-numeric

# annotation-based program properties extension

jpf-aprop = ${}/projects/jpf/jpf-aprop

2

extensions=${jpf-core},${jpf-aprop}

#... and all your other installed projects

文件中的主要格式为“<组件名> = <组件路径>”，而最后的extensions一项的配置将影响到后续建立JPF工程时的参考格式，为JPF的自行拓展提供了便利。在路径中出现的，指的是当前用户的工作目录，如果不清楚你的机器的具体路径，可以使用Java中的perty("")语句读取属性的值。对于${..}的内容，JPF将自动进行拓展补充，同时避免了驱动器盘符的输入，不会因输入绝对路径而造成JPF迁移的不便。

初次创建ties文件，应至少且必须包含jpf-core的路径位置，同时extensions的值也应至少且必须包含${jpf-core}。以后如有需求，下载其它的JPF组件使用，要记得在ties文件中添加其相应的路径等信息。

有些人可能会有这样的疑问，为什么要用配置路径，而不是使用我自己之前下载时所存放的位置？一是因为之前提到的迁移不便，二是因为JPF中的默认位置就是如此。当然，我们可以在ties文件中将各组件路径指向自己所定义的任意位置，但在后续使用中的一些配置和管理上可能会出现bug。推荐使用默认位置，把刚才下载好的各个组件复制到相应路径即可。

在ties文件创建完毕后，用户还需告知JPF在启动时去哪一路径来读取ties文件。JPF官网上同样给出了默认位置，建议使用默认位置<>/.jpf/ties，这样就不需再做其它配置。否则还需自行修改配置参数（见第六部分）。

在这一步操作中，会出现一个新问题，即.jpf文件夹的创建。在Windows操作系统中，文件夹的命名（包括文件）是不允许“.”出现在名字首位的，系统认为“.”后的符号是后缀名，这时会提示“必须键入文件名”。那么怎么来创建.jpf文件夹呢？这里使用的是cmd命令行操作。到达相应目录后，使用“md .jpf”（md和.jpf中间有一个空格）命令，即可在该目录下创建.jpf文件夹。

另附官网ties源文件下载，其组件、路径等内容请自行调整：

/trac/jpf/attachment/wiki/install/site-properties/ties-windows （请注意该文件后缀名的修改）

六、安装Eclipse JPF插件

在此有两种方法：第一种方法较为便捷，推荐使用，但需要电脑连网；第二种方法的适用范围较为普遍。

1、使用网址链接安装（较便捷）

① 确保你运行的Eclipse版本>= 3.5

② 在Eclipse中选择Help->Install New Software

③ 在新窗口中选择“Add”

④ “Name”栏可以自定义，但“Location”栏需输入以下网址：

/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/u

3

pdate/

⑤ 在“Work with：”下拉菜单中，选择刚才设置的网址

⑥ 选中“Eclipse-JPF”复选框（打√），选择“Next”进行剩下的安装

2、使用dropins文件夹安装

① 下载jpf-core，核实Eclipse>= 3.5且JDK>= 1.6

② 下载eclipse-jpf_*.jar文件，最新版本1.0.6，下载地址：

/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/eclipse-jpf_

③ 将下载的jar文件放入你所安装的Eclipse目录里的dropins文件夹中

④ 启动抑或重新启动Eclipse

⑤ 在Eclipse中选择Window->Preferences，检查是否能够看到并且能够点击“JPF Preferences”选项，如果可以表示安装成功

⑥ 该方法如果不成功很可能与Eclipse和JDK版本有关，其它问题可能由操作系统导致

为进一步验证插件是否安装完成，务必执行如下操作进行测试：

首先，设置Eclipse完成JPF自动build（构建）的操作。选择Project，在下拉菜单中查看Build Automatically前的对勾√是否选中，如果没有，点击一下即为选中。

其次，完成JPF相关参数的配置。选择Window->Preferences，点击“JPF

Preferences”选项，在Path to ties栏设置你所创建的配置文件的路径。如果你的ties文件使用的是默认路径，此处无需设置。另外JPF还有其它参数可配置，如有需要再做修改。

再次，将下载好的jpf-core工程导入到eclipse中。选择File->Import，在弹出窗口中选择General下的Existing Projects into Workspace，点击Next，在Select root directory这一栏后点击Browse（即浏览„），找到jpf-core文件夹点击“确定”，点击Finish即完成导入。导入的同时Eclipse自动build，如无异常Console面板会显示BUILD SUCCESSFUL字样。

最后，测试.jpf文件能否进行Verify。在成功build的jpf-core工程中，src/examples下提供了一些.jpf文件测试例。右键点击一个.jpf文件，如果插件已经被正确安装，那么将会出现一个Verify选项，否则表示没有成功。选择Verify选项，就表示开始对系统的验证过程。

七、构建（build）和运行

1、构建（build）

正如上文中所述，Eclipse可以自动完成build操作，但我仍要强调build操作的重要性。每一个新clone的JPF组件都要进行build过程后方可使用，通过build操作，可间接验证组件的完整性以及运行环境的可适性。如果build出现问题，根据错误提示可以判断：是我的JDK出了问题？还是下载的组件不完全？抑或是环境变量Java_Home没配置好？等等。

4

对于喜欢命令行操作的用户，可以使用如下命令进行build：

> cd jpf-core（以jpf-core为例）

> bin/ant

如果构建成功，最后将显示：BUILD SUCCESSFUL

特别的，对于Eclipse来说，如果自动build出现问题的话，可进行如下设置，尝试问题的解决：

在Eclipse中选择Project->Properties，点击“Builders”选项，选择Ant_Builder点击Edit，点击JRE书签，选择Separate JRE->Installed JREs，选中JDK1.6(1.7)xxx。如果列表中没有显示所安装的JRE，那么点击Add，浏览找到所安装的JDK1.6(1.7)xxx的位置并选中它。

2、运行

JPF验证的运行，离不开.java文件和.jpf文件的支持。.java文件是验证之本，具体验证细节则是由.jpf文件配置，通常情况下两类文件要放在同一目录中才能进行验证。.jpf文件里的必备元素是target=MAIN_CLASS，MAIN_CLASS是需要测试的系统中包含main方法的类，这就使得两类文件建立了关联。如有其它需要指定的配置也在这里添加，例如listener、classpath等参数。

JPF验证在Eclipse中的运行十分简单，有两种方法：一种是上一部分提到过的Verify，右键点击一个.jpf文件，将会出现一个Verify选项，选择Verify选项，就表示开始对系统的验证过程；另一种是在Eclipse中打开某个.jpf文件，然后选择Run-> Run Configurations-> Java Application-> run-JPF。无论何种方法，最后的结果都显示在Console面板中。

运行结果的显示效果如下：

JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center

.....

========================================= statistics

elapsed time: 0:00:00

states: new=9, visited=1, backtracked=4, end=2

search: maxDepth=5, constraints=0

choice generators: thread=8, data=0

heap: gc=8, new=291, free=32

instructions: 3112

max memory: 79MB

loaded code: classes=73, methods=1010

========================================= search finished: 1/12/10 2:30 PM

八、小结

关于Java Pathfinder（JPF）的安装配置过程，有几点是需要特别注意的，如有纰漏可能会造成最终运行的失败：

1、务必保证JDK的版本在1.6（6.0）以上，Eclipse的版本在3.5（Galileo）

5

以上；

2、使用Mercurial的clone方法到官网下载JPF组件，以确保准确完整；

3、按照规范的格式创建ties文件，保证路径等参数的准确性；

4、各路径的选用以默认路径为佳，减少配置时的出错率；

5、逐步完成Eclipse中的各项配置，逐步排错，逐步验证，确保无误再进行下一步配置。

6