Mercurial > hg > Papers > 2008 > atsuki-master
view paper/chapter5.tex @ 28:8dc58ffa1d79
*** empty log message ***
author | atsuki |
---|---|
date | Fri, 22 Feb 2008 08:34:55 +0900 |
parents | c1ef5abc2bb7 |
children |
line wrap: on
line source
\chapter{結論} \label{chapter5} 本稿では、Continuation based C言語による実装と その実装に対する検証手法を提案した。 第\ref{chapter3}章では、検証の対象として並列プログラムを選択し、 その例題としてDining Philosophers Problemを採用し、実装した。 検証の前準備として、並列プログラムの全状態を網羅的に探索するための タブロー展開器を実装した。 また、タブロー展開する際に検証用のコードセグメントを組み込むことで Dining Philosophers Problemのデッドロックを検知できるようにした。 第\ref{chapter4}では、タブロー展開器と それに検証用コードセグメントを組み込んだ場合のそれぞれの実装において、 プロセス数に対する状態数と検証にかかる時間の評価および考察を行った。 また、他のモデル検査ツールであるSPINとJava PathFinderとの比較を行い、考察した。 \\ 今後の課題として、状態探索にかかる時間を短縮するために メモリの Binary Tree をバランスさせることと、 状態探索空間を圧縮するために、 LZW法による状態の圧縮の実装をすることがあげられる。