Mercurial > hg > Papers > 2008 > atsuki-master
view paper/chapter4.tex @ 0:a67653fda270
Initial revision
author | atsuki |
---|---|
date | Tue, 12 Feb 2008 17:37:48 +0900 |
parents | |
children | e1214989942e |
line wrap: on
line source
\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での検証は、実際に動作するプログラムに対して行うことができる。