\chapter{評価および考察}
\label{chapter4}
%評価に使用したマシンのスペック

\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での検証は、実際に動作するプログラムに対して行うことができる。