Java PathFinder (JPF) 是 NASA 開發的 Java 字節碼級模型檢查器，能系統性探索多線程程序所有執行路徑，檢測死鎖、未捕獲異常等並發缺陷。本文記錄在 Windows 平台使用 NetBeans 4.1 從 SourceForge CVS 獲取源碼、配置項目、構建運行測試套件的全流程。
1. 環境準備
- JDK 1.4.2+ 或 1.5.0+ (建議 1.5.0)
- NetBeans 4.1 IDE
- JPF Convenience Libraries (
jpf-lib.zip，含 bcel.jar, fast-MD5.jar, xercesImpl.jar)
下載目錄統一設為 C:\tmp。
2. 安裝組件
- 運行
jdk-1_5_0_02-windows-i586-install.exe 安裝 JDK。
- 運行
netbeans-4_1-rc1-windows.exe 安裝 NetBeans。
- 解壓
jpf-lib.zip 到 JPF 源碼目錄下的 lib 文件夾 (CVS 會創建 javapathfinder/lib)。
3. NetBeans 從 CVS 獲取源碼
- 菜單 Versioning → CVS → Check Out。
- 服務器：
cvs.sourceforge.net，端口 2401，類型 pserver。
- 用戶名：
anonymous，密碼：留空。
- 倉庫路徑：
/cvsroot/javapathfinder。
- 模塊/標籤：留空 (獲取全部)。
- 工作目錄：如
C:\jpf。
- 登錄 (匿名) → OK，等待下載完成。
4. 創建 NetBeans 項目 (Existing Ant Script)
- File → New Project → General → Java Project with Existing Ant Script。
- 位置：選擇 CVS 工作目錄下的
javapathfinder 文件夾 (含 build.xml)。
- 項目名/文件夾接受默認。
- Build and Run Actions：保持 Ant 目標映射默認。
- Source Package Folders：
- Add Folder →
javapathfinder/src
- Test Package Folders → Add Folder →
javapathfinder/test
- Source Level：選擇 JDK 1.4。
- Java Sources Classpath：添加
lib 下三個 jar：bcel.jar, fast-MD5.jar, xercesImpl.jar。
- Finish。
5. 構建與運行測試套件
- 項目窗口右鍵
JavaPathFinder → Run Project (會先構建再運行測試)。
- 輸出窗口顯示 Ant 構建過程與 JUnit 測試結果。
- 測試通過即表示環境配置正確，JPF 核心模型檢查引擎可用。
JPF 核心價值回顧
- 顯式狀態空間探索：JVM 級別攔截線程調度、鎖操作、字節碼指令，系統枚舉所有可能執行路徑。
- 並發缺陷檢測：死鎖、數據競爭、活鎖、未捕獲異常——傳統測試極難覆蓋的場景。
- 完整錯誤路徑報告：不僅給出錯誤點，還給出導致錯誤的完整執行序列 (線程切換、鎖獲取/釋放歷史)。
- 擴展性：監聽器 API、自定義搜索策略、抽象域、模擬環境 (文件系統、網絡、數據庫)。
現代替代與傳承
JPF 現已遷移至 GitHub (javapathfinder/jpf-core)，支持 Maven/Gradle，集成 IntelliJ/Eclipse/VS Code。核心理念被現代工具吸收：
- ThreadSanitizer (TSan)：LLVM 編譯器插桩檢測數據競爭 (C/C++/Go/Rust)。
- Java Concurrency Stress Tests (jcstress)：OpenJDK 官方並發壓測框架。
- Model Checking in TLA+/PlusCal：系統設計層面形式化驗證。
理解 JPF 原理，有助於掌握並發程序驗證的本質思維：狀態空間窮盡 vs 抽象近似。
