ドキュメント(単なる本家の全訳です)

Java PathFinder(JPF)とは？

以前は，「JPFはJavaのバイトコードに対するな明示的状態ソフトウェアモデルチェッカ₍₁₎」と答えていた．しかし，現在，JPFは，まるでアーミーナイフのように，あらゆる種類の実行環境の検証が可能なソフトウェアであるといえる．

(1) 明示的な状態ソフトゥェアモデルチェッカ = explicit state model checker, 有限状態を前提とするモデルチェッカのことだと思うが良い訳がないので直訳

あなたが形式手法を良く知らないのなら，JPFは以下の処理をするものであると考えるとよい．JPFは，対象のプログラムを一度(通常のVMはもちろん一度だけしか実行しません)だけでなく，理論的に可能なすべての入力によって実行を繰り返すことにより，実行経路上で潜在的に生じえるデッドロックや補足されない例外のような違反がないかどうかをチェックする．もし，このような違反を発見した場合，JPFは，どのような実行によってこの違反に達したのかという，実行経路を示す．またJPFは，問題にたどり着くすべての実行ステップにおける情報を保持しており、この点で，JPFは通常のデバガと異なる．

JPFは，何をチェックできるのだろうか？

JPFはどのような種類の不具合を見つけることができるのであろうか？JPFをただインストールしただけの状態でも，JPFはデッドロックと補足されない例外(たとえば NullPointerExceptionsやAssertionErrors)を発見することができる．さらに，あなたが自分自身でプロパティクラスやリスナエクステンションを実装すれば，他の特性(たとえば，リソースの競合など)のチェックもできるようになるのである．
では，JPFが対象にできるプログラムはどのようなものであろうか？
JPFのVMは，プラットフォーム依存のネイティブコードを実行することはできない．よって，一般論で言えば，JPFはネイティブメソッドの呼び出しをしないJavaプログラムのみを対象にすることができる．この制約は，テスト対象のアプリケーションにおいて，どのような標準ライブラリを利用することができるかに関しての制約となる．ネイティブコードを呼び出すライブラリを利用できるようにするために，JPDは，Model Java Interface(MJI)を用意している．しかし，現時点ではjava.awtやjava.netは対応しておらず，java.ioの一部に対応しているのみである．
もう一つの制約として，アプリケーションの大きさがある．JPDが実行状態を保持するため，なんら状態の抽象化をしない場合，おおよそ〜10kloc程度(もちろんコードの中身によるが)のアプリケーションでないと効率的にチェックができない．
標準ライブラリの利用制限とプログラムコードの大きさの制限から，JPFは，主に完全な手続き的プログラムで記述されたモデルであるようなアプリケーションに利用されている．JPFは，特にJavaプログラムのコンカレンシーの検証に利用される．つまり，スケジュールされた連続処理の網羅的な探査のために使われる．

モデル検証とテスト

なぜJPFは普通のテストでは不可能なことができるのであろうか？それは、JPFが「非決定性」を扱うことができるからである。一方、テストドライバーは、たとえば、処理の実行順序などの非決定性を制御できない。というのも、その制御は、実行環境(VM)が制御するからである。また、ランダムな入力データのような非決定性も、提供するAPIを用いたユーザの実装によって簡単に実現可能である。非決定性をシミュレートすることは単にすべての非決定的な選択をシステマティックに実現するだけではない。バックトラッキングと状態の一致判定が可能になるということである。

1. バックトラッキングとは、JPFが実行状態の履歴を保持し、まだ実行していない処理が残っていないかを判断することである。たとえば、JPFがプログラムの終了状態に達したとする。その場合、JPFは、履歴を元に実行状態を「後戻り」することにより、まだ実行していない実行順序の処理発見することができる。このような処理は、理論的には、単にプログラムを開始状態から再実行するという機構で実現できるが、バックトラッキングは、状態を上手に保持していえば、はるかに効果的な機構である。
2. 状態の一致判定とは、無駄な処理をしないためのもう一つの工夫である。プログラムの実行状態は、主にヒープとスレッドスタックのスナップショットで構成される。JPFが動作している間、JPFは、新しい実行状態ごとに、過去に同じ状態がなかったかどうかをチェックする。そして、同じ状態が存在した場合、現在の実行経路による処理を続けることが無駄であるので、JPFは最も近い実行していない非決定的選択までバックトラックする。

理論的に、明示的状態モデル検証はきわめて厳密なやり方である。なぜならすべての選択を探索するからであり、ソフトウェアに何らかの問題があれば必ず発見できる。残念ながら、ソフトウェアのモデル検証は、この厳密性のために10kloc程度の小さなプログラムに対してのみ適応が可能である。なぜなら、複雑なプログラムになると、状態数はコンピュータが計算できる限界を上回ってしまうからである。この問題は状態爆発として知られており、原子的な処理から構成される複数のプロセスがどのような実行順序をとりうるかを考えるとわかりやすい。

---

JPFは状態爆発に起因するスケーラビリティの問題を3つの方法で解決している。一つ目は検索戦略を選択できるようにしていること、二つ目は、状態数の削減、3つ目は状態保持のための必要なメモリ量の削減である。

1. 探索戦略が選択可能であることは、すべての状態を検索することができないという問題を、問題を早く見つけるように検索を方向付けることによって解決しようという考え方である。この考え方は、モデルチェッカーを証明のためでなく、デバッグのために用いるということを前提にしている。方法としては、注目する特性に関係のある状態に達する可能性を考慮した順序や選択で探索をヒューリスティックに実行することによる。このヒューリスティック性の処理は、JPFのコアプログラムにハードコーディングされておらずプラグイン形式のクラスとして実装されている。
2. 蓄積すべき状態数の削減とは、スケーラビリティを改良する方法としてよくやるやり方であり、ＪＰＦでは、多くの方式を利用している。
   1. ヒューリスティックな選択生成
   2. 半順序の関係を利用した削減
   3. ホストVMの利用
   4. 状態の抽象化

---

リンク

JavaPathfinder 本家