Mercurial > hg > Papers > 2008 > atsuki-master

changeset 17:4c4dd3e3fc09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author atsuki
date Tue, 19 Feb 2008 03:33:12 +0900
parents 6bd5455a9335
children 5c445fc2b857
files paper/chapter1.tex paper/chapter4.tex paper/figure/mem_pat_tree.bb paper/figure/mem_pat_tree.pdf
diffstat 4 files changed, 19 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/paper/chapter1.tex	Tue Feb 19 03:33:12 2008 +0900
+++ b/paper/chapter1.tex	Tue Feb 19 03:33:12 2008 +0900
@@ -7,24 +7,29 @@
 %% 本論文の各章の概要
 
 \section{研究の背景と目的}
-近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
-そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
-設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
-デバッグ手法の確立が重要な課題となっている。
+リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
+逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
+困難である。
+そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
+確立が重要な課題となっている。
+%近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
+%そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
+%設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
+%デバッグ手法の確立が重要な課題となっている。
 
-ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
-しかし、ソフトウェアの規模の拡大や複雑化により、
-テスト手法では時間やコストがかかってしまう。
+%ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
+%しかし、ソフトウェアの規模の拡大や複雑化により、
+%テスト手法では時間やコストがかかってしまう。
 
 その課題の解決案として本研究では、Continuation based C(CbC)言語
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
-また、CbCで記述されたプログラムは決定性状態遷移記述と近い構造になるという性質がある。
+また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
 
-本研究は、CbCが決定性状態遷移記述と相性の良い言語であることに着目し、
-非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
-状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。
+本研究は、CbCプログラムが状態遷移記述になることに着目し、
+状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
+状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。
 
 \section{論文の構成}
--- a/paper/chapter4.tex	Tue Feb 19 03:33:12 2008 +0900
+++ b/paper/chapter4.tex	Tue Feb 19 03:33:12 2008 +0900
@@ -176,7 +176,7 @@
 	5 & 38,984 & 0.68 \\ \hline
 	6 & 159,299 & 3.90 \\ \hline
 	7 & 845,529 & 28.48 \\ \hline
-	8 & 3915,727 & 201.04 \\ \hline
+	8 & 3,915,727 & 201.04 \\ \hline
     \end{tabular}
     \end{center}
     \label{tab:ltl_tableau}
@@ -190,7 +190,7 @@
 	5 & 94 & 0.008 \\ \hline
 	6 & 212 & 0.01 \\ \hline
 	7 & 494 & 0.03 \\ \hline
-	8 & 212 & 0.04 \\ \hline
+	8 & 1,172 & 0.04 \\ \hline
     \end{tabular}
     \end{center}
     \label{tab:spin_dpp}
--- a/paper/figure/mem_pat_tree.bb	Tue Feb 19 03:33:12 2008 +0900
+++ b/paper/figure/mem_pat_tree.bb	Tue Feb 19 03:33:12 2008 +0900
@@ -1,5 +1,5 @@
 %%Title: ./mem_pat_tree.pdf
 %%Creator: ebb Version 0.5.2
 %%BoundingBox: 0 0 466 429
-%%CreationDate: Tue Feb 19 04:03:52 2008
+%%CreationDate: Tue Feb 19 04:08:07 2008
 
Binary file paper/figure/mem_pat_tree.pdf has changed