Java Pathfinder

Java Pathfinder (JPF) は、実行可能なJava バイトコードプログラムを検証するためのシステムです。JPF はNASAエイムズ研究センターで開発され、2005 年にオープンソース化されました。JPF という略語は、無関係なJava Plugin Frameworkプロジェクトと混同しないように注意してください。

JPFの中核はJava仮想マシンです。JPFは通常のJavaバイトコードプログラムを実行し、プログラムの状態を保存、照合、復元できます。主な用途は、データ競合やデッドロックなどの欠陥を見つけるための並行プログラムのモデル検査です。JPFは、それぞれの拡張機能により、以下のようなさまざまな他の目的にも使用できます。

• 分散アプリケーションのモデル検査
• ユーザーインターフェースのモデル検査
• 記号実行によるテストケース生成
• 低レベルプログラム検査
• プログラム計測とランタイム監視

JPFには状態空間の分岐に関する固定的な概念はなく、データとスケジューリングの両方の選択肢を扱うことができる。

JPFは、さまざまな方法で拡張できるオープンシステムです。主な拡張構成要素は次のとおりです。

• リスナー- 複雑なプロパティ（例：時間的プロパティ）を実装する
• ピアクラス- ホストJVMレベルでコードを実行する（JPFではなく）。これは主にネイティブメソッドの実装に使用される。
• バイトコードファクトリ- バイトコード命令の代替実行セマンティクスを提供する（例：記号実行を実装する）
• 選択生成器- スケジューリングの選択やデータ値セットなどの状態空間分岐を実装する
• シリアライザ- プログラムの状態抽象化を実装する
• 出版社- さまざまな出力形式を作成する
• 検索ポリシー- 異なるプログラム状態空間探索アルゴリズムを使用する

JPFには、このような構成要素を個別のJPF拡張プロジェクトとしてパッケージ化するためのランタイムモジュールシステムが含まれています。メインのJPFサーバーからは、シンボリック実行モード、数値解析、緩和されたメモリモデルの競合状態検出、ユーザーインターフェースモデルの検査など、多数のプロジェクトが利用可能です。

• JPFはJavaネイティブメソッドを解析できません。テスト対象システムがそのようなメソッドを呼び出す場合、それらはピアクラス内で提供されるか、リスナーによってインターセプトされる必要があります。
• モデルチェッカーとして、JPFは組み合わせ爆発の影響を受けやすいが、オンザフライで部分順序削減を実行する。
• JPFモジュールとランタイムオプションの設定システムは複雑になる可能性がある

• MoonWalker - Java PathFinderに似ていますが、Javaプログラムではなく.NETプログラム用です。

• NASAの新ソフトウェアがJavaコンピュータコードの「バグ」を検出
• NASAがJavaコンピュータコードの「バグ」を検出する新しいソフトウェアを開発

• Willem Visser、Corina S. Păsăreanu、Sarfraz Khurshid。「Java PathFinder によるテスト入力生成」。George S. Avrunin、Gregg Rothermel 編：ACM/SIGSOFT 国際ソフトウェアテストおよび分析シンポジウム 2004 論文集。ACM Press、2004 年。ISBN 1-58113-820-2。
• Willem Visser、Klaus Havelund、Guillaume Brat、Seungjoon Park、Flavio Lerda、「モデル検査プログラム」、Automated Software Engineering 10(2)、2003年。
• Klaus Havelund、Willem Visser、「プログラムモデル検査は新たなトレンド」、STTT 4(1)、2002年。
• Klaus Havelund、Thomas Pressburger、「Java PathFinder を使用した Java プログラムのモデル検査」、STTT 2(4)、2000 年。