--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/chapter4.tex	Tue Feb 12 17:37:48 2008 +0900
@@ -0,0 +1,29 @@
+\chapter{評価および考察}
+%評価に使用したマシンのスペック
+
+\section{Dining Philosophers Problemのタブロー展開}
+CbCで実装したDining Philosophers Problemに対してタブロー展開を適用した。
+プロセス(哲学者)が5〜7人の場合の結果は表\ref{tab:dpp_tableau}のようになった。
+
+\begin{table}
+    \centering
+    \begin{tabular}{|r|r|r|} \hline
+	プロセス数 & 状態数 & 時間(秒) \\ \hline
+	5 & 38,984 & 0.76 \\ \hline
+	6 & 159,299 & 4.21 \\ \hline
+	7 & 845,529 & 31.01 \\ \hline
+	8 & 3915,727 & 202.48 \\ \hline
+    \end{tabular}
+    \caption{Dining Philosophers Problemのタブロー展開結果}
+    \label{tab:dpp_tableau}
+\end{table}
+
+
+\section{線形時相論理を用いた検証}
+Dining Philosophers Problemのデッドロックを検知するためのコードセグメントを組み込んで
+タブロー展開を行った。
+
+\section{他の検証ツールとの比較}
+SPINはモデル検査ツールであるため、検証対象をモデル化しそれをPROMELAで記述する必要がある。
+
+CbCでの検証は、実際に動作するプログラムに対して行うことができる。