Mercurial > hg > Papers > 2008 > atsuki-master

changeset 27:c1ef5abc2bb7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author atsuki
date Fri, 22 Feb 2008 08:28:02 +0900
parents 3a8e2059e713
children 8dc58ffa1d79
files paper/Makefile paper/chapter1.tex paper/chapter2.tex paper/chapter3.tex paper/chapter4.tex paper/chapter5.tex paper/master_paper.tex paper/thanx.tex
diffstat 8 files changed, 70 insertions(+), 71 deletions(-) [+]
line wrap: on
line diff
--- a/paper/Makefile	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/Makefile	Fri Feb 22 08:28:02 2008 +0900
@@ -1,5 +1,5 @@
 MAKE=make -f Makefile
-LATEX=platex
+LATEX=platex-euc
 BIBTEX=jbibtex
 MENDEX=mendex
 DVIPS=pdvips
--- a/paper/chapter1.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/chapter1.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -12,16 +12,8 @@
 困難である。
 そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
 確立が重要な課題となっている。
-%近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
-%そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
-%設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
-%デバッグ手法の確立が重要な課題となっている。
 
-%ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
-%しかし、ソフトウェアの規模の拡大や複雑化により、
-%テスト手法では時間やコストがかかってしまう。
-
-その課題の解決案として本研究では、Continuation based C(CbC)言語
+そこで、本研究では、Continuation based C(CbC)言語\cite{bib:jssst2000kono}
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
@@ -42,7 +34,7 @@
 そして、線形時相論理によるCbCプログラムの検証の手法とその実装について述べる。
 
 第\ref{chapter4}章では、実装したプログラムの評価を行い、それについて考察する。
-また、他の検証ツールとの比較を行う。
+また、他のモデル検査ツールとの比較を行う。
 
 第\ref{chapter5}章で本稿のまとめを述べる。
 
--- a/paper/chapter2.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/chapter2.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -2,7 +2,7 @@
 \label{chapter2}
 ここでは、CbCの概要を解説し、CbCプログラムの検証に必要となるタブロー法および、
 線形時相論理について述べる。
-また、検証に関連して他の検証ツールの概要を説明する。
+また、検証に関連して他のモデル検査ツールの概要を説明する。
 
 \section{Continuation based C とは}
 CbC は、C言語を制限したもので、機械依存性の無いアセンブラのような構成になっており、
@@ -93,11 +93,11 @@
     \label{fig:code-goto}
 \end{figure}
 
-図\ref{fig:code-goto}のようにCbCプログラムの構成は、オートマトンと似た構造になることがわかる。
+図\ref{fig:code-goto}のようにCbCプログラムの構成は、オートマトンと同じ構造になることがわかる。
 CbCのコードセグメントと引数付きgoto、ifはそれぞれオートマトンの状態と状態遷移および
-遷移条件に対応しており、CbCは状態遷移記述に適しているといえる。
+遷移条件に対応しており、CbCプログラムは状態遷移記述になることがわかる。
 
-また、CbCのconcurrencyはコードセグメント単位であるため、
+また、本研究では、CbCのconcurrencyはコードセグメント単位としており、
 実装の方法により任意に細分化することができる。
 concurrencyとはプログラムの並列実行性のことである。
 
@@ -219,20 +219,18 @@
     \item □¬p：安全性特性
     \item ◇p：活性特性
 \end{itemize}
-安全性特性とは、有限な期間での反例を無限の時系列に拡張しても反例であるような状態のことである。
-活性特性とは、有限な期間での反例を無限の時系列に拡張したとき、それが反例でなくなる状態である。
-つまり、安全性特性はあるシステムにおいて「何か悪いことが決して起こらない」ことを意味する。
+安全性特性とは、あるシステムにおいて「何か悪いことが決して起こらない」ことを意味する。
 また、活性特性は「何か良いことがいずれ起きる」ことを意味する。
 これらの表現を用いてシステムの要求仕様を記述することで、
 形式的検証を行うことが可能である。
 
-\section{他の検証ツール}
-他の検証ツールとしてSPINとJava PathFinderがあげられる。
+\section{他のモデル検査ツール}
+他のモデル検査ツールとしてSPIN\cite{bib:spin}とJava PathFinder\cite{bib:jpf}があげられる。
 この２つのツールの概要を説明する。
 
 \subsection{SPINの概要}
 有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
-その代表的なツールとしてSPIN\cite{bib:spin}がある。
+その代表的なツールとしてSPINがある。
 
 SPINは、プログラム変換的な手法で検証するツールで、
 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
@@ -286,7 +284,7 @@
 また、SPINのconcurrencyはステートメント単位となっている。
 
 \subsection{Java PathFinderの概要}
-Javaプログラムに対するモデル検査ツールであるJava PathFinder(JPF)\cite{bib:jpf}
+Javaプログラムに対するモデル検査ツールであるJava PathFinder(JPF)
 について説明する。
 JPFはNASAで開発され、現在はsourceforge.net上で開発が続けられている。
 
--- a/paper/chapter3.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/chapter3.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -102,14 +102,14 @@
 その後、各プロセスに対してラウンドロビンやランダムといった任意の方式で実行する。
 ラウンドロビンとは、各プロセスを一定時間ずつ順番に実行することである。
 
-並列実行のシミュレーションに関しては、SPINを参考に各プロセスをランダムに
-実行することで実現する。
+並列実行のシミュレーションに関しては、
+SPIN\cite{bib:spin}を参考に各プロセスをランダムに実行することで実現する。
 
 \section{CbCプログラムのタブロー展開}
-CbCプログラムのタブロー展開の特徴を以下に示す。
+CbCプログラムのタブロー展開の概要を以下に示す。
 \begin{itemize}
     \item プログラムの可能な実行の組み合わせすべてを調べる。
-    \item 状態の探索はDepth First Searchで行う。
+    \item 状態の探索はDepth First Search(DFS)で行う。
     \item プログラムの実行によって生成される状態は木構造で記録する。
     \item 同じ状態はすべて共有される。
 \end{itemize}
@@ -163,8 +163,8 @@
 \end{figure}
 
 例では単一のプロセスの場合を述べたが、実際には5個のプロセスを並列に実行することになる。
-その場合、状態数は指数オーダーで増加する。
-状態数が多い場合、特に並列プログラムに対する状態の展開を手作業で行うのは不可能に近い。
+その場合、状態数は指数関数的に増加する。
+そのため、並列プログラムに対する状態の展開を手作業で行うのは困難である。
 
 \newpage
 \subsection{タブロー展開器の実装}
@@ -175,7 +175,7 @@
 タブロー展開器は、スケジューラと同様にCbCプログラムに組み込み、
 複数プロセスを制御することで並列実行をシミュレーションすることができる。
 また、タブロー展開器は、コードセグメントを一つずつ実行しながら状態を探索していく。
-状態の探索はDFS(Depth First Search)で行う。
+状態の探索はDFSで行う。
 例えば、Dining Philosophers Problemの単一プロセスの状態探索木は
 図\ref{fig:dpp_dfs}のようになる。
 
@@ -280,23 +280,16 @@
 \\
 
 
-次にDepth First Search(DFS)による状態の探索の実装について述べる。
+次にDepth First Searchによる状態の探索の実装について述べる。
 
 本研究では、イテレータを用いてDFSを実装した。
 イテレータとは、配列やリストなどのデータ構造の各要素に対する
 繰り返し処理を抽象化する手法のことである。
 
 タブロー展開器はスケジューラとしての機能を備えている。
-そのため、プロセスを実行する順番をリストとして持ち、制御する。
-これをタスクリストと呼ぶ(図\ref{fig:task_list})。
-
-\begin{figure}[htpb]
-    \begin{center}
-	\includegraphics[scale=.9]{figure/task_list.pdf}
-    \end{center}
-    \caption{タスクリストの例}
-    \label{fig:task_list}
-\end{figure}
+そのため、プロセスを実行する順番をリストとして持っている。
+これをタスクリストと呼ぶ。
+スケジューラはこのタスクリストを用いて、プロセスの実行順序を制御する。
 
 状態を展開する際に、このタスクリストに登録された順番にプロセスを実行していく。
 したがって、プログラムの状態を一つ進めるためにタスクリストからタスクを取りだし、
@@ -308,9 +301,12 @@
 DFSの実装の具体的な内容について述べる。
 
 タスクリストからタスクを取り出す機構としてタスクイテレータを実装した。
-タスクイテレータはその時点のタスクリストと状態データベースおよび
+タスクイテレータはその時点の状態データベースおよび
 ひとつ前の時点のタスクイテレータを保持している。
-また、タスクリストから次のタスクを取り出す機能を持っている(図\ref{fig:task_iterator})。
+それに加えて、タスクイテレータはその時点で実行可能なタスクをすべて生成し、
+タスクリストとして保持している。
+また、タスクリストから次のタスクを取り出す機能を持っている
+(図\ref{fig:task_iterator})。
 
 \begin{figure}[htpb]
     \begin{center}
@@ -372,13 +368,14 @@
 タブローコードセグメントは、関数呼び出しを使用するためCwCで記述している。
 
 \verb|get_memory_hash()|関数によってメモリパターンのハッシュ値を取得する。
-そのハッシュ値をもとに\verb|lookup_StateDB()|関数で状態データベースの検索を行っている。
+ハッシュ値は\verb|lookup_StateDB()|関数で状態データベースの検索を行う際に、
+検索を高速化するために使用している。
 \verb|next_task_iterator()|関数は次に実行するタスクを取り出すものである。
 
 \verb|restore_memory()|関数は任意の時点の状態に戻すための関数である。
 
 実際にコードセグメントを実行するのは\verb|goto list->phils->next()|である。
-引数付きgotoで検証対象のプログラムのコードセグメントに遷移する。
+引数付きgoto文で検証対象のプログラムのコードセグメントに遷移する。
 
 タスクイテレータが根に達した場合、探索を終了するために
 \verb|goto ret(0),env|を実行している。
@@ -418,13 +415,13 @@
 これは、LTLで表現できる重要な特性の一つの安全性特性である。
 
 これを検査するための検証用コードセグメントをソースコード\ref{src:check}に示す。
-
+\\
 \lstinputlisting[caption=検証用コードセグメント,label=src:check]
 {src/ltl.cbc}
 
 \verb|p()|関数は命題pに相当するもので、すべての哲学者(プロセス)が
 左手にフォークを持っているかどうかを判定するものである。
 checkコードセグメントがタブロー展開の際に実行されることで、
-すべての状態において命題pが決して起こらないかどうかを検査することができる。
+すべての状態において命題pが起こらないかどうかを検査することができる。
 
 %%% end %%%
--- a/paper/chapter4.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/chapter4.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -1,10 +1,10 @@
-\chapter{評価}
+\chapter{評価と考察}
 \label{chapter4}
 
 実装したDining Philosophers Problemのタブロー展開および、
 線形時相論理による検証を組み込んだタブロー展開の評価を行う。
 
-また、検証を組み込んだタブロー展開においては他の検証ツールとの比較を行う。
+また、検証を組み込んだタブロー展開においては他のモデル検査ツールとの比較を行う。
 
 比較の対象としては、SPIN と Java PathFinder を用いる。CbCによる記述と合わせて、
 Dining Philosophers Problemの状態空間の探索にかかる時間を測定した。
@@ -54,12 +54,13 @@
 また、実行時間も同様に増加している。
 
 しかし、プロセス数が5個と6個の場合の実行時間がそれぞれ0.66秒、3.79秒と速く、
-実用レベルであると言える。
+実用レベルであるといえる。
 
 \section{線形時相論理を用いた検証}
+
+%\subsection{CbCによるDining Philosophers Problemの検証}
 Dining Philosophers Problemのデッドロックを検知するためのコードセグメントを組み込んで
 タブロー展開を行う。
-また、他の検証ツールとの比較を行う。
 \\
 
 プロセスが5〜8個の場合の計測結果は表\ref{tab:ltl_tableau}のようになった。
@@ -67,7 +68,7 @@
 検証用のコードセグメントを組み込んでのタブロー展開は、
 組み込む前のものと比べて実行時間はあまり変わっていない。
 
-また、プロセスが5個の場合の実行結果は以下のようになっている。
+また、プロセスが5個の場合のプログラムの実行結果は以下のようになっている。
 
 \begin{center}
 \begin{itembox}[l]{プロセスが5個の場合の実行結果}
@@ -155,6 +156,7 @@
 \begin{table}[htbp]
     \begin{center}
     \caption{Dining Philosophers Problemのタブロー展開結果}
+    \label{tab:dpp_tableau}
     \begin{tabular}{|r|r|r|} \hline
 	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
 	3 & 1,340 & 0.01 \\ \hline
@@ -165,12 +167,12 @@
 	8 & 3915,727 & 199.80 \\ \hline
     \end{tabular}
     \end{center}
-    \label{tab:dpp_tableau}
 %\end{table}
 
 %\begin{table}
     \begin{center}
     \caption{Dining Philosophers Problemにデッドロック検知を組み込んだ計測結果}
+    \label{tab:ltl_tableau}
     \begin{tabular}{|r|r|r|} \hline
 	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
 	5 & 38,984 & 0.68 \\ \hline
@@ -179,12 +181,12 @@
 	8 & 3,915,727 & 201.04 \\ \hline
     \end{tabular}
     \end{center}
-    \label{tab:ltl_tableau}
 %\end{table}
 
 %\begin{table}
     \begin{center}
     \caption{SPINによるDining Philosophers Problemの検証の計測結果}
+    \label{tab:spin_dpp}
     \begin{tabular}{|r|r|r|} \hline
 	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
 	5 & 94 & 0.008 \\ \hline
@@ -193,12 +195,12 @@
 	8 & 1,172 & 0.04 \\ \hline
     \end{tabular}
     \end{center}
-    \label{tab:spin_dpp}
 %\end{table}
 
 %\begin{table}
     \begin{center}
     \caption{JPFによるDining Philosophers Problemの検証の計測結果}
+    \label{tab:jpf_dpp}
     \begin{tabular}{|r|r|} \hline
 	プロセス数 & 実行時間(秒) \\ \hline
 	5 & 3.98 \\ \hline
@@ -207,7 +209,6 @@
 	8 & 123.16 \\ \hline
     \end{tabular}
     \end{center}
-    \label{tab:jpf_dpp}
 \end{table}
 
 
@@ -246,7 +247,7 @@
 探索時間が長くなっていると考えられる。
 %JPF の探索時間がCbCの探索時間よりも遅いのは、JPFがbyte code の
 %実行をSimulateしていることが大きい。また、メモリ量自体と状態数もCbCに
-%よる記述よりも多いと推定される。状態数自体は JPFに測定する昨日が
+%よる記述よりも多いと推定される。状態数自体は JPFに測定する機能が
 %ないので、これは推定である。
 
 \subsection{CbCによる検証方法の利点と欠点}
@@ -299,7 +300,7 @@
 コンパイルしたCのコードによるシミュレータにより検証を行っている。
 CbC は、他の二つと異なり、コードセグメント部分は直接実行
 される。この部分にエラーが入ることはないのがCbCによる
-検証の利点であると言える。
+検証の利点であるといえる。
 
 [検証する性質の記述]
 
@@ -324,7 +325,7 @@
 これは検証系自体が、検証される言語と同じ言語で記述されている
 ことの利点である。タブロー展開を行う{\tt goto文}
 を適切に選択することにより、同期の抽象度を選択できることも
-利点であると言える。
+利点であるといえる。
 
 JPFでは一見同じ言語で検証系を記述しているように見えるが、
 実際の検証対象はJava バイトコードであり、実装はインタプリタ
--- a/paper/chapter5.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/chapter5.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -9,17 +9,20 @@
 検証の前準備として、並列プログラムの全状態を網羅的に探索するための
 タブロー展開器を実装した。
 
-タブロー展開する際に検証用のコードセグメントを組み込むことで
+また、タブロー展開する際に検証用のコードセグメントを組み込むことで
 Dining Philosophers Problemのデッドロックを検知できるようにした。
 
 第\ref{chapter4}では、タブロー展開器と
 それに検証用コードセグメントを組み込んだ場合のそれぞれの実装において、
 プロセス数に対する状態数と検証にかかる時間の評価および考察を行った。
 
-プロセス数が5個の場合の実行時間が0.68秒と高速であり、実用レベルであることが言えた。
+プロセス数が5個の場合の実行時間が0.68秒と高速であり、
+実用レベルに達しているといえる。
 
-また、他の検証ツールであるSPINとJava PathFinderとの比較を行い、考察した。
+また、他のモデル検査ツールであるSPINとJava PathFinderとの比較を行い、考察した。
 \\
 
-今後の課題として、状態探索空間を圧縮するために、
-LZW法による状態の圧縮の実装があげられる。
+今後の課題として、状態探索にかかる時間を短縮するために
+メモリの Binary Tree をバランスさせることと、
+状態探索空間を圧縮するために、
+LZW法による状態の圧縮の実装をすることがあげられる。
--- a/paper/master_paper.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/master_paper.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -10,7 +10,7 @@
 % \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
 % bookmarkstype=toc]{hyperref}
 
-\jtitle{線形時相論理による Continuation based C プログラムの検証}
+\jtitle{線形時相論理を用いた Continuation based C プログラムの検証}
 \etitle{Verification of Continuation based C Program using Linear-time Temporal Logic} 
 \year{平成19年度}
 \affiliation{\center%
@@ -29,7 +29,7 @@
   \end{minipage}}
 \markleftfoot{% 左下に挿入
   \begin{minipage}{.8\textwidth}
-   線形時相論理による Continuation based C プログラムの検証
+   線形時相論理を用いた Continuation based C プログラムの検証
   \end{minipage}}
 
 
@@ -52,19 +52,19 @@
 %表目次
 \listoftables
 
-%概要
+%背景と研究目的
 \input{chapter1.tex}
-%CbCについて
+%CbC、線形時相論理、他のモデル検査ツールについて
 \input{chapter2.tex}
-%検証手法の提案
+%検証手法の実装
 \input{chapter3.tex}
-%実装
+%評価と考察
 \input{chapter4.tex}
-%考察
+%まとめと今後の課題
 \input{chapter5.tex}
 
 %謝辞
-%\input{thanx.tex}
+\input{thanx.tex}
 
 %参考文献
 \input{bibliography.tex}
--- a/paper/thanx.tex	Thu Feb 21 07:18:44 2008 +0900
+++ b/paper/thanx.tex	Fri Feb 22 08:28:02 2008 +0900
@@ -3,3 +3,11 @@
 
 本研究を行うにあたって、ご多忙にも関わらず日頃より多くのご助言、ご指導を
 頂きました河野真治准教授に心より感謝いたします。
+
+また、本研究に大変貴重なご意見を下さった、和田知久教授、遠藤聡志教授、
+並びに情報工学科の先生方に感謝いたします。
+
+研究を行うにあたり、心の支えとなってくれた本研究室の同期である
+神里晃さん、渕田良彦さん、並びに研究室の後輩のみなさまに深く感謝いたします。
+
+最後に、長年に渡り理解を示し、支援して下さった家族に感謝いたします。