--- a/paper/bibliography.tex	Wed Feb 13 20:52:35 2008 +0900
+++ b/paper/bibliography.tex	Thu Feb 14 05:30:52 2008 +0900
@@ -3,7 +3,7 @@
 	``Spin - Formal Verification''.
 	http://spinroot.com/spin/whatispin.html
 
-    \bibitem{bib:javapathfinder}
+    \bibitem{bib:jpf}
 	``Java PathFinder''.
 	http://javapathfinder.sourceforge.net/
 \end{thebibliography}

--- a/paper/chapter2.tex	Wed Feb 13 20:52:35 2008 +0900
+++ b/paper/chapter2.tex	Thu Feb 14 05:30:52 2008 +0900
@@ -285,5 +285,45 @@
 また、SPINのconcurrencyはステートメント単位となっている。
 
 \subsection{Java PathFinderの概要}
+Javaプログラムに対するモデル検査ツールであるJava PathFinder(JPF)\cite{bib:jpf}
+について説明する。
+JPFはNASAで開発され、現在はsourceforge.net上で開発が続けられている。
+
+最初の実装では、JavaをPromelaに変換していたが、
+現在は、Javaバーチャルマシン(JVM)を直接シミュレーションして実行している。
+そのため、Javaのバイトコードを直接実行可能である。
+
+
+JPFは、実行可能なJavaのバイトコードを検証するためのシステムである。
+バイトコードを状態遷移モデルとして扱い、
+実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
+キャッチされていない例外(NullPointerExceptionやAssertionErrorなど)を
+検出することができる。
+
+また、JPFはバイトコードの実行パターンを網羅的に調べるため、膨大なCPU時間を必要とする。
+
+
+JPFでできることを以下に示す。
+\begin{itemize}
+    \item スレッドの可能な実行すべてを調べる
+    \item デッドロックの検出
+    \item アサーション
+    \item Partial Order Reduction
+\end{itemize}
+
+Partial Order Reductionとは、モデル検査アルゴリズムで探索される
+状態空間のサイズを減らすための手法である。
+
+
+また、JPFはJVMベースであるため、複数のプロセスの取扱いができない。
+他にも、実用規模のプログラムは一般的に状態空間が巨大であるため、
+直接実行することはできない。
+
+JPFは、大きなプログラムには使えないため、一部を抜き出して、
+それに対してデバッグをするのに使用される。
+他にも、Javaを仕様記述言語としてプロトコルの検証などに用いられる。
+
+JPFのconcurrencyはスレッド単位である。
+
 
 %%%end%%%