|
0
|
1 %% 要旨
|
|
|
2 \begin{abstract}
|
|
|
3 近年、ソフトウェアは大規模かつ複雑化していく傾向がある。
|
|
|
4 そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
|
|
|
5 設計・実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
|
|
|
6 デバッグ手法の確立が重要な課題となっている。
|
|
|
7 検証とは、ソフトウェアが仕様を満たすことを数学的に厳密に確かめることである。
|
|
|
8
|
|
|
9 本研究では、検証を実装に組み込むことが可能な言語である
|
|
|
10 Continuation based C(CbC)を提案する。
|
|
|
11 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
|
|
|
12 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという
|
|
|
13 利点がある。
|
|
|
14
|
|
|
15 CbCによって記述されたプログラムは状態遷移記述と近い構造になるという性質がある。
|
|
|
16 その性質に着目し、非決定性状態遷移記述に対して有効である、
|
|
|
17 タブロー法による状態の展開を行い、その際に線形時相論理式も同時に展開することで
|
|
|
18 検証を行った。
|
|
|
19 タブロー法とは、様相論理式の恒真性を検証する定理証明アルゴリズムで、
|
|
|
20 木構造に基づく反駁手法である。
|
|
|
21 検証にかかる実行時間を計測したところ、実用において十分であることが示された。
|
|
|
22 また、他の検証ツールと比較することで、その優位性と改善すべき点について考察した。
|
|
|
23 \end{abstract}
|
