\section{ CbCを用いた検証手法と他の手法との比較}

コードセグメントを使わずに、Cの関数による分割を行って
も良い。この場合は、分割された関数を順々に呼び出す
マネージャを記述する必要がある。CbCのようにモデル検査を
自分で記述するようなことは出来ないが、分割に関しては
同等である。

モデル検査では SPIN\cite{holzmann97model}が有名だが、SPINでは
問題を Promela という仕様記述言語で記述する必要があり、
Promela を直接実装に使うことは出来ない。

実装言語を直接モデル検査するシステムとしては、
Java PathFinder\cite{havelund98model}、
CBMC\cite{groce04understanding}などが知られている。これらはオブジェクト指向
記述に対しても適用できるという利点がある。
これらで並列処理を記述する場合は、一般的にはThread の
機能を用いることになる。

CbCでは、スケジューラ及びモデル検査器を自分で記述出来るので、
検査する並列性や抽象度を自分で制御できると言う利点がある。
現状では、そういう可能性があるというだけで実装は行っていない。

現在用いているCbC用のモデル検査器は比較的単純に作られており、
大きなプログラムの検証をするのには向かない。2.8GHz Pentinum 4
では、Dining Philosphers の例題に対して以下のような性能が
出ている。

\begin{table}[htbp]
\begin{center}
\caption{Dining Philosophers ProblemのCbCによるモデル検査}
\label{tab:dpp_tableau}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
3 & 1,340 & 0.01 \\ \hline
4 & 6,115 & 0.08 \\ \hline
5 & 38,984 & 0.66 \\ \hline
6 & 159,299 & 3.79 \\ \hline
7 & 845,529 & 27.59 \\ \hline
8 & 3915,727 & 199.80 \\ \hline
\end{tabular}
\end{center}
\end{table}

\begin{table}[htbp]
\begin{center}
\caption{SPINによるDining Philosophers Problemのモデル検査}
\label{tab:spin_dpp}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
5 & 94 & 0.008 \\ \hline
6 & 212 & 0.01 \\ \hline
7 & 494 & 0.03 \\ \hline
8 & 1,172 & 0.04 \\ \hline
\end{tabular}
\end{center}
\end{table}

\begin{table}[htbp]
\begin{center}
\caption{JPFによるDining Philosophers Problemのモデル検査}
\label{tab:jpf_dpp}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
5 & 不明 & 3.98 \\ \hline
6 & 不明 & 7.33 \\ \hline
7 & 不明 & 26.29 \\ \hline
8 & 不明 & 123.16 \\ \hline
\end{tabular}
\end{center}
\end{table}

Java Path Finder とSPINの丁度間の性能となっているが、プロセス数が
多くなると、Java Path Finder よりも性能が落ちる。これは、モデル
検査のための状態格納のアルゴリズムに問題があると考えている。
SPINの性能が良いのは、元々の状態記述の抽象度が高く状態数そのものが
小さいからであると考えられる。

CbCの記述を変更して、スケジューラを呼び出す頻度を下げると、
状態するが下がりSPINに近い性能を得ることも可能である。
Java Path Finder では、そのような変更を行うことは原理的に
出来ない。