--- a/resume/master_proc.sty	Wed Feb 20 08:15:33 2008 +0900
+++ b/resume/master_proc.sty	Wed Feb 20 16:50:00 2008 +0900
@@ -81,12 +81,12 @@
 \hoffset -1in \addtolength{\hoffset}{0mm}
 \voffset -1in \addtolength{\voffset}{15mm}
 \oddsidemargin 10mm
-\evensidemargin 20mm
+\evensidemargin 10mm
 \topmargin 0mm
 \headheight 0mm
 \headsep 0mm
 \textheight 260mm %295-(15+20)mm
-\textwidth 180mm %odd-> 210-(10+20) : even->  210-(20+10)
+\textwidth 190mm %odd-> 210-(10+20) : even->  210-(20+10)
 \marginparsep 0mm
 \marginparwidth 0mm
 \footskip \headsep

--- a/resume/master_resume.tex	Wed Feb 20 08:15:33 2008 +0900
+++ b/resume/master_resume.tex	Wed Feb 20 16:50:00 2008 +0900
@@ -27,31 +27,28 @@
 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
 
 本研究は、CbCプログラムが状態遷移記述になることに着目し、
-状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
+状態遷移記述に対して有効であるタブロー法による状態の展開を行い、
 状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
 
 \vspace{-2mm}
 \section{Continuation based Cの概要}
 CbC は、C言語を制限したもので、
-C言語からループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
-この言語は、C言語に継続専用のプログラム単位であるコード(code)と、
+Cからループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
+この言語は、Cに継続専用のプログラム単位であるコード(code)と、
 継続(goto)を導入した構成となっている。
 継続とは、次に実行すべきコードを直接または間接的に指定する手法である。
-CbC は、サブルーチンよりも小さいプログラム単位であるコードを導入しているため、
+CbC は、サブルーチンよりも小さいプログラム単位であるcodeを導入しているため、
 C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
 
 CbCはコードセグメントを引数付きgoto文で接続することで継続を実現している。
 コードセグメントとは、codeという型で定義されるプログラム単位である。
-原則として、このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
+このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
 また、コードセグメントからの脱出も引数付きgoto文によってのみ行われる。
-つまり、CbCプログラムは、複数のコードセグメントが引数付きgoto文で接続された構造になる。
 
-CbCのコードセグメントと引数付きgoto文、ifはそれぞれオートマトンの状態と状態遷移および
-遷移条件に対応しており、CbCプログラムは状態遷移記述であると言える。
-また、CbCにおける並列動作はコードセグメント単位となる。
+また、ここでは、CbCにおける並列度はコードセグメント単位を使用する。
 
-CbCはC言語の下位言語であるが、C言語のサブルーチンへ戻るための環境付き継続を
-導入することでC言語の上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
+CbCにCのサブルーチンへ戻るための環境付き継続を
+導入することでCの上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
 CwCでは、CbCから通常のC言語の関数を呼び出すことができる。
 
 \vspace{-2mm}
@@ -80,10 +77,10 @@
 れる。
 
 \vspace{-2mm}
-\section{他の検証ツール}
-他の検証ツールとしてSPINとJava PathFinder(JPF)がある。
+\section{他のモデル検査ツール}
+他のモデル検査ツールとしてSPINとJava PathFinder(JPF)がある。
 
-SPINは、プログラム変換的な手法で検証するツールで、
+SPIN\cite{bib:spin}は、プログラム変換的な手法で検証するツールで、
 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
 それを基にC言語で記述された検証器を生成するものである。
 チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
@@ -91,16 +88,15 @@
 性質について検査することができる。
 また、SPINの並列動作はステートメント単位となる。
 
-JPFは、実行可能なJavaのバイトコードを検証するためのシステムである。
+JPF\cite{bib:jpf}は、実行可能なJavaのバイトコードを検証するためのシステムである。
 バイトコードを状態遷移モデルとして扱い、
 実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
-キャッチされていない例外(NullPointerExceptionやAssertionErrorなど)を
-検出することができる。
+キャッチされていない例外を検出することができる。
 JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
 があげられる。
 また、JPFの並列動作はスレッド単位となる。
+\vspace{-2mm}
 
-\vspace{-2mm}
 \section{実装}
 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
 これは資源共有問題の一つで、次のような内容である。
@@ -109,6 +105,8 @@
 フォークが取れない場合はフォークが空くのを待つ。
 この問題では、すべての哲学者が一斉に左手でフォークを取るとデッドロックが起きる。
 例として、左手でフォークを取るコードセグメントを示す。
+
+\vspace{-3mm}
 {\footnotesize
 \begin{verbatim}
 code pickup_lfork(PhilsPtr self)
@@ -123,6 +121,7 @@
 \end{verbatim}
 }
 \vspace{-4mm}
+
 codeがコードセグメントの定義であり、
 コードセグメントの引数部分をインターフェースと呼ぶ。
 このコードセグメントは左手でフォークが取れた場合は、
@@ -130,24 +129,25 @@
 取れなかった場合は、またこのコードセグメントへ遷移する。
 
 次に、タブロー法による状態の展開の実装について説明する。
-タブロー法による状態の展開をタブロー展開と呼ぶ。
 
-CbCプログラムのタブロー展開の特徴として、
+CbCプログラムのタブロー法による状態の展開の特徴として、
 プログラムの可能な実行の組み合わせすべてを調べる、
-プログラムの状態を展開するために状態の探索をDepth First Search(DFS)で行う、
+プログラムの状態を展開するために状態の探索をDepth First Searchで行う、
 プログラムの実行によって生成される状態は木構造で記録する、
-同じ状態はすべて共有することでメモリ消費を減らす、
+同じ状態はすべて共有することでメモリ消費を減らすということ
 があげられる。
 
-まず、最初に状態として扱うすべての変数をBinary Tree構造で記録する。
+まず、最初に状態として扱うすべてのメモリをBinary Tree構造で記録する。
 そして、検証対象のプログラムのコードセグメントを実行して、
 実行に伴う状態の変化をBinary Tree構造で記録していく。
 このBinary Treeを状態データベースと呼ぶ。
 すべての可能な実行の組み合わせを実行しながらそのときの状態を
-状態データベースに登録していくことで状態を展開する。
+状態データベースに登録していく。
 
 以下にタブロー展開を行うためのtableauコードセグメントを示す。
 このコードセグメントはCwCで記述している。
+
+\vspace{-3mm}
 {\footnotesize
 \begin{verbatim}
 code tableau(TaskPtr list)
@@ -172,68 +172,62 @@
 \end{verbatim}
 }
 \vspace{-3mm}
+
 検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
 \verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
 得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
-変数を記録したBinary Treeをコピーして登録していく。この際、同じ内容の変数が
+メモリを記録したBinary Treeをコピーして登録していく。この際、同じメモリ内容が
 あった場合は、同じ領域を指すことで状態を共有するようにする。
 このtableauコードセグメントによりDFSで状態を探索していく。
 
-また、タブロー展開を行う際に、線形時相論理(Linear-time Temporal Logic、LTL)式より
-生成されたコードセグメントを実行することで検証を行う。
-検証対象のプログラムからタブローコードセグメントに遷移する前に
-LTL式より生成された検証用コードセグメントを実行する。
+また、タブロー展開を行う際に、
+LTL式より生成されたコードセグメントを実行することで検証を行う。
+検証対象プログラムからtableauコードセグメントに遷移する前に
+生成された検証用コードセグメントを実行することで検証する。
 
-Dining Philosophers Problemに対して、デッドロックの検知を行う。
-デッドロックが起きる条件として、「哲学者が一斉に左手でフォークを取る」を
-すべての状態で検査することで検知する。
+ここでは、実装したDining Philosophers Problemに対して、デッドロックの検知を行う。
+デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
+結果としてプログラムが停止してしまうことである。
+Dining Philosophers Problemにおいて、資源とはフォークのことである。
+つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
+右手のフォークが空くのを待っている状態である。
+
+デッドロックが起きる条件である、「哲学者が一斉に左手でフォークを取る」を
+すべての状態で検査することでプログラムのデッドロックを検知する。
 
 \vspace{-2mm}
 \section{評価および考察}
 Dining Philosophers Problemの検証をCbC、SPIN、JPFで行った。
-それぞれの結果を表2、表3、表4に示す。
+それぞれの結果を表\ref{tab:time}に示す。
 \begin{table}[htbp]
-\vspace{-6mm}
+\vspace{-2mm}
     {\footnotesize
     \begin{center}
-    \caption{CbCによる検証の計測結果}
     \begin{tabular}{|r|r|r|} \hline
+	\multicolumn{3}{|c|}{\textbf{CbCによる検証}} \\ \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
+	\multicolumn{3}{|c|}{\textbf{SPINによる検証}} \\ \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
+	\multicolumn{3}{|c|}{\textbf{JPFによる検証}} \\ \hline
 	5 & 不明 & 3.98 \\ \hline
 	6 & 不明 & 7.33 \\ \hline
 	7 & 不明 & 26.29 \\ \hline
 	8 & 不明 & 123.16 \\ \hline
     \end{tabular}
+\vspace{-3mm}
+    \caption{検証の計測結果}
+    \label{tab:time}
     \end{center}
-    \label{tab:jpf}
     }
-\vspace{-3mm}
+\vspace{-7mm}
 \end{table}
-\vspace{-3mm}
 CbCの検証では、実際に実行可能なプログラムであり、プログラムで渡される引数全体と
 大域変数全体が状態となるため、プロセス数が増えるにつれて状態数も指数関数的に
 多くなっている。
@@ -246,13 +240,15 @@
 
 CbCでの実装では、メモリのBinary Treeをバランスさせていないため、
 状態数が増えるにつれて探索時間が長くなっていると考えられる。
+
 \vspace{-2mm}
 \section{まとめ}
 Dining Philosophers ProblemをCbCで記述し、
 LTL式より生成された検証用コードセグメントを同時にタブロー展開することで
-検証を行い、他の検証ツールと比較した。
+検証を行い、他のモデル検査ツールと比較した。
 CbCの方が遅いという結果になったが、実用には耐えられるレベルである。
 また、メモリのTreeをバランスさせることで探索時間の短縮を行うことが課題である。
+
 \vspace{-2mm}
 {\small
 \begin{thebibliography}{9}
@@ -262,6 +258,12 @@
     \bibitem{bib:sigos2007}
 	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
 	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
+    \bibitem{bib:spin}
+	``Spin - Formal Verification''.
+	http://spinroot.com/spin/whatispin.html
+    \bibitem{bib:jpf}
+	``Java PathFinder''.
+	http://javapathfinder.sourceforge.net/
 \end{thebibliography}
 }
 \end{document}