Mercurial > hg > Papers > 2008 > atsuki-master

comparison paper/chapter1.tex @ 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 0ba2de3295b8
children c1ef5abc2bb7
comparison
equal deleted inserted replaced
16:6bd5455a9335 17:4c4dd3e3fc09
5 %% 解決案の提示 5 %% 解決案の提示
6 %% 研究目標 6 %% 研究目標
7 %% 本論文の各章の概要 7 %% 本論文の各章の概要
8 8
9 \section{研究の背景と目的} 9 \section{研究の背景と目的}
10 近年、ソフトウェアは大規模かつ複雑なものが増えてきている。 10 リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
11 そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、 11 逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
12 設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および 12 困難である。
13 デバッグ手法の確立が重要な課題となっている。 13 そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
14 確立が重要な課題となっている。
15 %近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
16 %そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
17 %設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
18 %デバッグ手法の確立が重要な課題となっている。
14 19
15 ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。 20 %ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
16 しかし、ソフトウェアの規模の拡大や複雑化により、 21 %しかし、ソフトウェアの規模の拡大や複雑化により、
17 テスト手法では時間やコストがかかってしまう。 22 %テスト手法では時間やコストがかかってしまう。
18 23
19 その課題の解決案として本研究では、Continuation based C(CbC)言語 24 その課題の解決案として本研究では、Continuation based C(CbC)言語
20 による実装とその実装に対する検証手法を提案している。 25 による実装とその実装に対する検証手法を提案している。
21 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。 26 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
22 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。 27 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
23 また、CbCで記述されたプログラムは決定性状態遷移記述と近い構造になるという性質がある。 28 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
24 29
25 本研究は、CbCが決定性状態遷移記述と相性の良い言語であることに着目し、 30 本研究は、CbCプログラムが状態遷移記述になることに着目し、
26 非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、 31 状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
27 状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。 32 状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
28 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。 33 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。
29 34
30 \section{論文の構成} 35 \section{論文の構成}
31 第\ref{chapter2}章ではCbCの概要を説明し、 36 第\ref{chapter2}章ではCbCの概要を説明し、
32 CbCプログラムの検証に必要となるタブロー法および、 37 CbCプログラムの検証に必要となるタブロー法および、