# HG changeset patch
# User atsuki
# Date 1202811382 -32400
# Node ID e1214989942e842a986a85028565beda3511cddb
# Parent  a67653fda270eb5b0812432d7c3f74c1408b3630
*** empty log message ***

diff -r a67653fda270 -r e1214989942e paper/chapter1.tex
--- a/paper/chapter1.tex	Tue Feb 12 17:37:48 2008 +0900
+++ b/paper/chapter1.tex	Tue Feb 12 19:16:22 2008 +0900
@@ -6,6 +6,7 @@
 %% 研究目標
 %% 本論文の各章の概要
 
+\section{研究の背景と目的}
 近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
 そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
 設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
@@ -15,9 +16,24 @@
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
-また、CbCで記述されたプログラムは状態遷移記述と近い構造になるという性質がある。
+また、CbCで記述されたプログラムは非決定性状態遷移記述と近い構造になるという性質がある。
 
-本研究は、CbCが状態遷移記述と相性の良い言語であることに着目し、
-状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
+本研究は、CbCが非決定性状態遷移記述と相性の良い言語であることに着目し、
+非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
 状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。
 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。
+
+\section{論文の構成}
+第\ref{chapter2}章ではCbCの概要を説明し、
+CbCプログラムの検証に必要となるタブロー法および、
+線形時相論理について述べる。
+また、検証に関連して他の検証ツールの概要を説明する。
+
+第\ref{chapter3}章では、CbCプログラムのタブロー展開の手法およびその実装について説明する。
+そして、線形時相論理によるCbCプログラムの検証の手法とその実装について述べる。
+
+第\ref{chapter4}章では、実装したプログラムの評価を行い、それについて考察する。
+また、他の検証ツールとの比較を行う。
+
+第\ref{chapter5}章で本稿のまとめを述べる。
+
diff -r a67653fda270 -r e1214989942e paper/chapter2.tex
--- a/paper/chapter2.tex	Tue Feb 12 17:37:48 2008 +0900
+++ b/paper/chapter2.tex	Tue Feb 12 19:16:22 2008 +0900
@@ -1,7 +1,8 @@
 \chapter{Continuation based C と検証}
+\label{chapter2}
 ここでは、CbCの概要を解説し、CbCプログラムの検証に必要となるタブロー法および、
 線形時相論理について述べる。
-また、検証に関連して他の検証ツールについて、その概要と本研究との違いを述べる。
+また、検証に関連して他の検証ツールの概要を説明する。
 
 \section{Continuation based C とは}
 CbC は、C言語を制限したもので、機械依存性の無いアセンブラのような構成になっており、
@@ -98,6 +99,7 @@
 
 また、CbCのconcurrencyはコードセグメント単位であるため、
 実装の方法により任意に細分化することができる。
+concurrencyとはプログラムの並列実行性のことである。
 
 \subsection{C with Continuation}
 CbCは、C言語の下位言語であるが、C言語のサブルーチンへ戻るための環境付き継続を
@@ -119,6 +121,8 @@
 
 この展開の際に、仕様も同時に展開することでプログラムに対する仕様の検証を行うことが可能である。
 
+\section{ソフトウェアの検証}
+
 \section{並列プログラムにおける検証}
 プログラムにおいて非決定性な要素として入力と並列実行があげられる。
 プログラム自体は仕様が決まっており、決定性であるといえる。
diff -r a67653fda270 -r e1214989942e paper/chapter3.tex
--- a/paper/chapter3.tex	Tue Feb 12 17:37:48 2008 +0900
+++ b/paper/chapter3.tex	Tue Feb 12 19:16:22 2008 +0900
@@ -1,4 +1,5 @@
 \chapter{線形時相論理によるCbCプログラムの検証手法}
+\label{chapter3}
 
 \section{CbCによる並列プログラミング}
 ここでは、例題に用いるサンプルプログラムの概要と、
diff -r a67653fda270 -r e1214989942e paper/chapter4.tex
--- a/paper/chapter4.tex	Tue Feb 12 17:37:48 2008 +0900
+++ b/paper/chapter4.tex	Tue Feb 12 19:16:22 2008 +0900
@@ -1,4 +1,5 @@
 \chapter{評価および考察}
+\label{chapter4}
 %評価に使用したマシンのスペック
 
 \section{Dining Philosophers Problemのタブロー展開}
diff -r a67653fda270 -r e1214989942e paper/chapter5.tex
--- a/paper/chapter5.tex	Tue Feb 12 17:37:48 2008 +0900
+++ b/paper/chapter5.tex	Tue Feb 12 19:16:22 2008 +0900
@@ -1,4 +1,5 @@
 \chapter{結論}
+\label{chapter5}
 本稿では、Continuation based Cプログラムに対する検証手法を提案した。
 
 まず、検証の対象として並列プログラムを選択し、