# HG changeset patch
# User atsuki
# Date 1202901916 -32400
# Node ID 732554511aedf15dc0f70f33c4326f0d17ec8d2b
# Parent  e1214989942e842a986a85028565beda3511cddb
*** empty log message ***

diff -r e1214989942e -r 732554511aed paper/chapter1.tex
--- a/paper/chapter1.tex	Tue Feb 12 19:16:22 2008 +0900
+++ b/paper/chapter1.tex	Wed Feb 13 20:25:16 2008 +0900
@@ -12,6 +12,10 @@
 設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
 デバッグ手法の確立が重要な課題となっている。
 
+ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
+しかし、ソフトウェアの規模の拡大や複雑化により、
+テスト手法では時間やコストがかかってしまう。
+
 その課題の解決案として本研究では、Continuation based C(CbC)言語
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
diff -r e1214989942e -r 732554511aed paper/chapter2.tex
--- a/paper/chapter2.tex	Tue Feb 12 19:16:22 2008 +0900
+++ b/paper/chapter2.tex	Wed Feb 13 20:25:16 2008 +0900
@@ -122,10 +122,36 @@
 この展開の際に、仕様も同時に展開することでプログラムに対する仕様の検証を行うことが可能である。
 
 \section{ソフトウェアの検証}
+現在、様々なものにソフトウェアが組み込まれているが、
+これらの中にはバグを含むものが少なくないのが現状である。
+バグとは、ソフトウェアが期待された動きと別な動きをすることである。
+また、その「期待された動き」を規定したものを仕様と呼び、
+自然言語または論理で記述される。
+
+ソフトウェアのバグを減らし信頼性を高めるために、テストや検証を行う必要がある。
+
+テストとは、限定された条件でプログラムを実行し、
+正しく動作するかどうかを確認する作業のことである。
+通常、すべての条件で動作を確認するのは難しいため、
+重要な部分のみテストを行うことが多い。
+そのため、テストでは誤りが存在することを示すことはできるが、
+誤りが存在しないことは証明できない。
+
+検証とは、ソフトウェアが仕様を満たすことを数学的、論理的に確かめることである。
+ソフトウェア検証には、大きく分類してモデル検査と定理証明がある。
+モデル検査では、有限状態モデルを網羅的に探索して、デッドロックや飢餓状態などの
+望ましくない状態を自動的に検出することができる。
+しかし、無限の状態を持つものや有限でも多くの状態を持つものは取り扱うことが困難である。
+一方、定理証明では、定理や推論規則を用いて検証を行うため、
+そのような状態を持つものでも取り扱うことが可能であるが、対話的な推論が必要になる。
 
 \section{並列プログラムにおける検証}
+並列プログラムにおいて、個々のプログラムが正しく動作することが証明されても、
+それらを並列に実行したとき、その全体の動作の正しさは証明されない。
+これは並列プログラムの非決定性によるものである。
+
 プログラムにおいて非決定性な要素として入力と並列実行があげられる。
-プログラム自体は仕様が決まっており、決定性であるといえる。
+単体のプログラム自体は仕様が決まっており、決定性であるといえる。
 しかし、複数のプログラムを並列に実行する場合、その全体の動作は非決定性となる
 (図\ref{fig:parallel_exec})。
 
@@ -138,15 +164,15 @@
 \end{figure}
 
 並列プログラムの検証手順として、並列実行するプログラムの可能な実行すべてを
-データ構造として構築し、そのデータ構造に対して、仕様を検証する。
+データ構造として構築し、そのデータ構造に対して仕様を検証する。
 
 例えば、C、VHDL、Javaなどで記述された複数のプログラムを並列実行する場合を考える。
 まず、それぞれのプログラムをCbCで書き換える。そして、それらのCbCプログラムを
 並列実行するためにスケジューラを組み込み、制御する。
-それによって作成された並列実行可能なプログラム全体は一つのCbCプログラムとみなすことができる。
+それによって作成された並列実行可能なプログラム全体は
+一つのCbCプログラムとみなすことができる。
 その並列実行を検証するために、プログラムの状態をデータ構造として構築する必要がある。
-そこで、CbCプログラムに対してタブロー展開を行う。そして、タブロー展開によって生成された
-データ構造に対して仕様を検証する(図\ref{fig:verification_procedure})。
+そこで、CbCプログラムに対してタブロー展開を行う。そして、タブロー展開によって生成されたデータ構造に対して仕様を検証する(図\ref{fig:verification_procedure})。
 
 \begin{figure}[htpb]
     \begin{center}