Java PathFinder 是 NASA 项目的结果。它主要是在 NASA 软件模型研究中心开发的,现在仍然在使 用。Java PathFinder 项目是一个软件模型检查的可行性研究,开始于 1999 年。从那时起它便开始了通 往学术研究和工业之路,它甚至在实际太空船缺陷检测中也发挥过作用。
Java PathFinder 是一个用来验证可执行 Java bytecode 程序的系统。它的基本形式是用作显式声明 软件模型检查程序的 Java 虚拟机 (JVM),从系统上探测程序所有可能的执行路径,以避免死锁或未处理 异常之类的情况发生。与传统的调试程序不同,Java PathFinder 报告导致缺陷的整个执行路径。Java PathFinder 特别适合在多线程的程序中发现很难测试的并发缺陷。
入门要入门,首先需要设置您的环境。验证环境设置正确之后,您将准备获得 Java PathFinder 源文 件,然后从 NetBeans 中构建并运行它。
本文档中的说明是从 Windows 用户的角度提出的。Solaris 和 Linux 用户应该针对其平台在适用的 地方替换路径名、安装程序名等。
设置环境构建和运行 Java PathFinder 之前,您需要安装几个附加组件。完成此操作的最简单方法是 下载所有组件,然后按照下文列出的顺序安装它们。
下载组件
注意: 安装说明假设您将所有组件下载到 C:\tmp 中。
Java 2 SDK 标准版本 1.4.2 或 1.5.0 或更高版本(如果尚未安装)。
http://java.sun.com/j2se/1.5.0/download.jsp
注意: 下面的说明假设您下载了 Windows 版本的 JDK。
NetBeans 4.1 IDE(如果您未安装 NetBeans)
http://www.netbeans.info/downloads/download.php?type=4.1rc1
注意: 如果您没有打算进行 J2EE 开发,则可以下载 NetBeans 4.1 RC 安装程序 (netbeans-4_1- rc1-windows.exe) 版本。
Java PathFinder Convenience Libraries
http://sourceforge.net/project/showfiles.php? group_id=136825&package_id=151191&release_id=323978
这个文件是 jpf-lib.zip,它包含 Java PathFinder 所需的 .jar 文件。
安装组件
下载所有组件之后,按照下面的说明安装它们。
如果您尚未安装 1.4.2 或 1.5.0 或更高版本的 JDK,则安装 Java 2 SDK:
转到下载 JDK 的 C:\tmp 目录,然后双击 jdk-1_5_0_02-windows-i586-install.exe 文件即可启动 JDK 的安装。按照 JDK 安装程序给出的说明来安装 JDK。
如果您尚未安装 NetBeans,则安装 NetBeans IDE:
转到下载 NetBeans 的 C:\tmp 目录,然后双击 netbeans-4_1-rc1-windows.exe 文件即可启动 NetBeans 的安装。按照 NetBeans 安装程序给出的说明来安装 NetBeans。
您已经具有构建 Java PathFinder 所需的环境了,现在开始准备启动 NetBeans、获得 Java PathFinder 源代码、从源中构建 Java PathFinder 并从 NetBeans 中运行所有 Java PathFinder。