因为要使用Java PathFinder (JPF)，我综合了一下网上搜到的资料。首先谢谢提供这些资料的网友，文中都注明了转载出处。—— by orzorz 飞天硕鼠
一、Java PathFinder (JPF)官网资料
http://javapathfinder.sourceforge.net/
With Subclipse installed (http://subclipse.tigris.org/) one can download JPF inside of Eclipse using "Import..." "Checkout Projects from SVN". The repository URL is https://svn.sourceforge.net/svnroot/javapathfinder and the folder to check out is "trunk". It's about that easy.
The Compiler settings in either the project or the workspace Properties dialog should have the "JDK Compliance" (tab "Compliance and Classfiles", settings "compiler compliance level" "generated class files compatibility" and "source compatibility") set to "5.0".
Beyond this, the only caveat for building and running JPF is the inclusion/exclusion of the env/jpf source directory. Classes compiled from this location are MJI model classes of standard Java library components that are only meant to be seen by JPF, not the host VM, and some problems can arise from this directory appearing in the Eclipse source path. Specifically, Eclipse compiles the rest of the classes considering these model classes as global replacements for the standard Java conterparts, including classes such as java.lang.Class and java.lang.Thread. For building, the model classes do not yet contain all the functions of the standard library classes, and for execution, the functionality is quite different: tailored to execution inside JPF. On some machines and Eclipse versions (esp. under Windows), this might cause the Eclipse internal builder to abort silently!
There are two solutions to this problem:
remove env/jpf as a source directory in the build path. (this makes the model class sources unavailable when editing/compiling their native peer counterparts in env/jvm.)
add missing model class methods and fields, so that Eclipse can build the JPF classes using these features. This may or may not break execution of JPF from within Eclipse, but it can be fixed with an explicit classpath for execution. Also, keep in mind that all JPF classes other than env/jpf will be executed by the host VM, and not JPF.
To run JPF from inside Eclipse, specify gov.nasa.jpf.JPF (RunJPF not recommended inside Eclipse) as the Main class inside the Run dialog (tab "Main"), use the default working directory (tab "Arguments"), specify the target application main class as the program argument, and make sure to include the project's default classpath (or a custom one to remove build/env/jpf) under user entries (tab "Classpath"). If the application under test resides outside the jpf directory tree, its class files of course have to be added to the user entries of the Classpath dialog tab.
二、网上资料：Java PathFinder (JPF) 运行介绍
（转载自 http://hi.baidu.com/sophiaandphilem/blog/item/9c0bd11bada84cd5ad6e7516.html ）
这几日师姐布置了任务，让弄这个玩意，查网上似乎资料很少，这里就我的实践介绍一下怎样用JPF来验证一个简单的类 ,IDE ：eclipse (eryueniaobp)
1)首先下到代码，可去官方网站或是 jpf.sourceforge.net ,似乎要用SVN (类似 CVS的东西).
2)导入现有工程到 eclipse工作空间
3)更改工程属性：(右击，有个property选项)
a .构建路径---〉添加JAR ，把lib文件夹下的几个.jar都加进来.
b. 再修改编译器 ，全部设为 1.4 .允许 assert 。（注：新版的jpf设置要求是5.0）
c. 构建路径 - 〉源代码- > 添加文件夹 把env/jpf 和env/jvm加进来 。。
4)上面基本配好了 ，可以运行一个小例子了...
这个工程自带了一些例子，在example文件夹下。我胡乱把example也加入了构建路径 -〉源代码 列表中，试着运行了一次，就生成了全部的 .class 文件，我也不清楚怎么搞的。这些.class默认在build文件夹下..
然后点运行 -- 〉配置工程变量是 HelloWorld，点应用 -〉运行，就可以看到效果了。。
这个变量是传给 JPF.java中的main()的,HelloWorld指的是 HelloWorld.class，写变量时不要加上 .class。。
要运行Deadlock这个例子，应该传一个变量 deadlock.Deadlock ，表示build / deadlock/ Deadlock.class .
哈哈，试试看，有效果了吧。。。。
如果运行自己写的一个类，那么在 JPF 的 属性 -〉构建路径 - >项目 中把你自己写的项目加进来就好了。。
比如你自己写一个项目 Temp ，， 生成了 Temp.class，设置好上面的东西后，传入参数 Temp,就可以看到效果了 。。 ^_^
以前都不知道" 构建路径" 怎么回事,这次弄这个算是有了点概念。。
三、具体步骤的截图介绍，在CSDN上有下载（未经同意 就不把附件贴过来了）
下载地址 http://download.csdn.net/source/173872
"在eclipse 3.2.2 下 的JPF(java pathfinder)配置过程，附有图形表示。网上这方面东西很少，自己研究出来后拿出来与大家分享。 "
四、通过 NetBeans 构建和运行 Java PathFinder
http://gceclub.sun.com.cn/NetBeans/tutorials/partnertoolkit/java-pathfinder.html
以及
http://www.learnjava.cn/Article/xinshou/gongju/netbeans/200711/1590.html
这两个地方都有很详细的说明，包括截图的演示。
-