# HG changeset patch
# User atsuki
# Date 1203462933 -32400
# Node ID d66662b295bac66833817b97b5234a6668b41bb2
# Parent  97f508fb5bf2f7a3beacf8ad8cef2b70445e4367
*** empty log message ***

diff -r 97f508fb5bf2 -r d66662b295ba resume/master_resume.tex
--- a/resume/master_resume.tex	Wed Feb 20 05:53:14 2008 +0900
+++ b/resume/master_resume.tex	Wed Feb 20 08:15:33 2008 +0900
@@ -24,17 +24,15 @@
 
 そこで、本研究では、Continuation based C(CbC)言語による実装と
 その実装に対する検証手法を提案している。
-CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
 
 本研究は、CbCプログラムが状態遷移記述になることに着目し、
 状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
 状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
-検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
-れる。
 
+\vspace{-2mm}
 \section{Continuation based Cの概要}
-CbC は、C言語を制限したもので、機械依存性の無いアセンブラのような構成になっており、
+CbC は、C言語を制限したもので、
 C言語からループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
 この言語は、C言語に継続専用のプログラム単位であるコード(code)と、
 継続(goto)を導入した構成となっている。
@@ -56,9 +54,34 @@
 導入することでC言語の上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
 CwCでは、CbCから通常のC言語の関数を呼び出すことができる。
 
+\vspace{-2mm}
+\section{線形時相論理の概要}
+線形時相論理(Linear-time Temporal Logic、LTL)は、
+時間を様相として持つ様相論理の一つで、
+状態遷移システムの単一の経路に関する性質を記述することが可能である。
+表\ref{tab:LTL}にLTLの単項演算子を示す。
+\begin{table}
+{\footnotesize
+    \begin{center}
+    \begin{tabular}{|l|c|l|} \hline
+	\multicolumn{1}{|c|}{名称} & 記号表記 & \multicolumn{1}{|c|}{意味} \\ \hline
+	Always & □p & pは今後常に真である \\ \hline
+	Sometime & ◇p & pは将来のいずれかの時点で真である\\ \hline
+	Next & ○p & pは次の時点で真である \\ \hline
+    \end{tabular}
+\vspace{-2mm}
+    \caption{線形時相論理の単項演算}
+    \label{tab:LTL}
+    \end{center}
+}
+\vspace{-8mm}
+\end{table}
+検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
+れる。
+
+\vspace{-2mm}
 \section{他の検証ツール}
-有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
-その代表的なツールとしてSPINとJava PathFinder(JPF)があげられる。
+他の検証ツールとしてSPINとJava PathFinder(JPF)がある。
 
 SPINは、プログラム変換的な手法で検証するツールで、
 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
@@ -75,14 +98,9 @@
 検出することができる。
 JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
 があげられる。
+また、JPFの並列動作はスレッド単位となる。
 
-また、JPFはJVMベースであるため、複数のプロセスの取扱いができない。
-他にも、実用規模のプログラムは一般的に状態空間が巨大であるため、
-直接実行することはできない。
-そのため、プログラムの一部を抜き出して、
-それに対してデバッグをするのに使用される。
-他にも、Javaを仕様記述言語としてプロトコルの検証などに用いられる。
-JPFの並列動作はスレッド単位となる。
+\vspace{-2mm}
 \section{実装}
 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
 これは資源共有問題の一つで、次のような内容である。
@@ -104,6 +122,7 @@
 }
 \end{verbatim}
 }
+\vspace{-4mm}
 codeがコードセグメントの定義であり、
 コードセグメントの引数部分をインターフェースと呼ぶ。
 このコードセグメントは左手でフォークが取れた場合は、
@@ -127,7 +146,8 @@
 すべての可能な実行の組み合わせを実行しながらそのときの状態を
 状態データベースに登録していくことで状態を展開する。
 
-以下にタブロー展開を行うためのタブローコードセグメントを示す。
+以下にタブロー展開を行うためのtableauコードセグメントを示す。
+このコードセグメントはCwCで記述している。
 {\footnotesize
 \begin{verbatim}
 code tableau(TaskPtr list)
@@ -151,12 +171,89 @@
 }
 \end{verbatim}
 }
+\vspace{-3mm}
 検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
 \verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
 得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
 変数を記録したBinary Treeをコピーして登録していく。この際、同じ内容の変数が
 あった場合は、同じ領域を指すことで状態を共有するようにする。
+このtableauコードセグメントによりDFSで状態を探索していく。
 
+また、タブロー展開を行う際に、線形時相論理(Linear-time Temporal Logic、LTL)式より
+生成されたコードセグメントを実行することで検証を行う。
+検証対象のプログラムからタブローコードセグメントに遷移する前に
+LTL式より生成された検証用コードセグメントを実行する。
+
+Dining Philosophers Problemに対して、デッドロックの検知を行う。
+デッドロックが起きる条件として、「哲学者が一斉に左手でフォークを取る」を
+すべての状態で検査することで検知する。
+
+\vspace{-2mm}
+\section{評価および考察}
+Dining Philosophers Problemの検証をCbC、SPIN、JPFで行った。
+それぞれの結果を表2、表3、表4に示す。
+\begin{table}[htbp]
+\vspace{-6mm}
+    {\footnotesize
+    \begin{center}
+    \caption{CbCによる検証の計測結果}
+    \begin{tabular}{|r|r|r|} \hline
+	プロセス数 & 状態数 & 実行時間(秒) \\ \hline
+	5 & 38,984 & 0.68 \\ \hline
+	6 & 159,299 & 3.90 \\ \hline
+	7 & 845,529 & 28.48 \\ \hline
+	8 & 3,915,727 & 201.04 \\ \hline
+    \end{tabular}
+    \end{center}
+    \label{tab:cbc}
+\vspace{-9mm}
+    \begin{center}
+    \caption{SPINによる検証の計測結果}
+    \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}
+    \label{tab:spin}
+\vspace{-9mm}
+    \begin{center}
+    \caption{JPFによる検証の計測結果}
+    \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}
+    \label{tab:jpf}
+    }
+\vspace{-3mm}
+\end{table}
+\vspace{-3mm}
+CbCの検証では、実際に実行可能なプログラムであり、プログラムで渡される引数全体と
+大域変数全体が状態となるため、プロセス数が増えるにつれて状態数も指数関数的に
+多くなっている。
+
+SPINによる結果は、CbCでの検証と比べて状態数が少ない。
+生成される状態数が少ないことが探索時間の短さにつながっていると考えられる。
+
+JPFの探索時間が、プロセス数6個まではCbCの探索時間よりも遅く、
+7個以上になるとCbCより速いのは、CbCの実装によるものだと推測される。
+
+CbCでの実装では、メモリのBinary Treeをバランスさせていないため、
+状態数が増えるにつれて探索時間が長くなっていると考えられる。
+\vspace{-2mm}
+\section{まとめ}
+Dining Philosophers ProblemをCbCで記述し、
+LTL式より生成された検証用コードセグメントを同時にタブロー展開することで
+検証を行い、他の検証ツールと比較した。
+CbCの方が遅いという結果になったが、実用には耐えられるレベルである。
+また、メモリのTreeをバランスさせることで探索時間の短縮を行うことが課題である。
+\vspace{-2mm}
 {\small
 \begin{thebibliography}{9}
     \bibitem{bib:jssst2000kono}