JavaPathfinder(JPF)完全安装配置过程.doc

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/index.html到官网或通过其它途径下载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的可视化客户端工具，操作起来更为简便。到官网或通过其它途径下载TortoiseHg，并完成TortoiseHg的安装。由于网上关于TortoiseHg的介绍和资源比较少，对于英文较为生疏的朋友，推荐一个汉化版TortoiseHg的下载网址：/soft/48257.html，经测试可正常使用。四、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即可。五、创建perties文件perties文件告诉JPF在初始化时去哪里寻找所下载的JPF组件，所以必须由用户亲自编辑，添加各个组件的地址路径。perties属于java编程中常用的properties文件，是一种配置文件，主要用于表达配置信息，文件类型为*.properties，格式为文本文件，文件的内容是格式是“键=值”的键值对格式。以下是一个perties文件的实例：# JPF site configurationjpf-core = $user.home/projects/jpf/jpf-core# numeric extensionjpf-numeric = $user.home/projects/jpf/jpf-numeric# annotation-based program properties extensionjpf-aprop = $user.home/projects/jpf/jpf-apropextensions=$jpf-core,$jpf-aprop#. and all your other installed projects文件中的主要格式为“ = ”，而最后的extensions一项的配置将影响到后续建立JPF工程时的参考格式，为JPF的自行拓展提供了便利。在路径中出现的user.home，指的是当前用户的工作目录，如果不清楚你的机器的具体路径，可以使用Java中的System.getProperty(user.home)语句读取user.home属性的值。对于$.的内容，JPF将自动进行拓展补充，同时避免了驱动器盘符的输入，不会因输入绝对路径而造成JPF迁移的不便。初次创建perties文件，应至少且必须包含jpf-core的路径位置，同时extensions的值也应至少且必须包含$jpf-core。以后如有需求，下载其它的JPF组件使用，要记得在perties文件中添加其相应的路径等信息。有些人可能会有这样的疑问，为什么要用user.home配置路径，而不是使用我自己之前下载时所存放的位置？一是因为之前提到的迁移不便，二是因为JPF中的默认位置就是如此。当然，我们可以在perties文件中将各组件路径指向自己所定义的任意位置，但在后续使用中的一些配置和管理上可能会出现bug。推荐使用默认位置，把刚才下载好的各个组件复制到相应路径即可。在perties文件创建完毕后，用户还需告知JPF在启动时去哪一路径来读取perties文件。JPF官网上同样给出了默认位置，建议使用默认位置/.jpf/perties，这样就不需再做其它配置。否则还需自行修改配置参数（见第六部分）。在这一步操作中，会出现一个新问题，即.jpf文件夹的创建。在Windows操作系统中，文件夹的命名（包括文件）是不允许“.”出现在名字首位的，系统认为“.”后的符号是后缀名，这时会提示“必须键入文件名”。那么怎么来创建.jpf文件夹呢？这里使用的是cmd命令行操作。到达相应目录后，使用“md .jpf”（md和.jpf中间有一个空格）命令，即可在该目录下创建.jpf文件夹。另附官网perties源文件下载，其组件、路径等内容请自行调整：/trac/jpf/attachment/wiki/install/site-properties/perties-windows （请注意该文件后缀名的修改）六、安装Eclipse JPF插件在此有两种方法：第一种方法较为便捷，推荐使用，但需要电脑连网；第二种方法的适用范围较为普遍。1、使用网址链接安装（较便捷） 确保你运行的Eclipse版本= 3.5 在Eclipse中选择Help-Install New Software 在新窗口中选择“Add” “Name”栏可以自定义，但“Location”栏需输入以下网址：/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/update/ 在“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_1.0.6.jar 将下载的jar文件放入你所安装的Eclipse目录里的dropins文件夹中 启动抑或重新启动Eclipse 在Eclipse中选择Window-Preferences，检查是否能够看到并且能够点击“JPF Preferences”选项，如果可以表示安装成功 该方法如果不成功很可能与Eclipse和JDK版本有关，其它问题可能由操作系统导致为进一步验证插件是否安装完成，务必执行如下操作进行测试：首先，设置Eclipse完成JPF自动build（构建）的操作。选择Project，在下拉菜单中查看Build Automatically前的对勾是否选中，如果没有，点击一下即为选中。其次，完成JPF相关参数的配置。选择Window-Preferences，点击“JPF Preferences”选项，在Path to perties栏设置你所创建的配置文件的路径。如果你的perties文件使用的是默认路径，此处无需设置。另外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没配置好？等等。对于喜欢命令行操作的用户，可以使用如下命令进行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。无论何种方法，最后