|
19
|
1 \documentclass[twocolumn, a4j, twoside]{jarticle}
|
|
|
2 \usepackage{master_proc}
|
|
|
3 \usepackage[dvips]{graphicx}
|
|
|
4
|
|
|
5 % dvipdfm を使って PDF ファイルに日本語の栞をつける
|
|
|
6 % \usepackage[dvipdfm]{color}
|
|
|
7 % \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
|
|
|
8 % bookmarkstype=toc]{hyperref}
|
|
|
9
|
|
|
10 \jtitle{線形時相論理によるContinuation based Cプログラムの検証} %和文タイトル
|
|
|
11 \etitle{Verification of Continuation based C Program using Linear-time Temporal Logic} %英文タイトル
|
|
|
12 \author{下地 篤樹} %著者名
|
|
|
13 \studentid{068507B} %学籍番号
|
|
|
14 \teacher{河野 真治} %指導教官
|
|
|
15
|
|
|
16 \begin{document}
|
|
|
17 \maketitle
|
|
|
18 \section{はじめに}
|
|
|
19 リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
|
|
|
20 逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
|
|
|
21 困難である。
|
|
|
22 そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
|
|
|
23 確立が重要な課題となっている。
|
|
|
24
|
|
|
25 そこで、本研究では、Continuation based C(CbC)言語による実装と
|
|
|
26 その実装に対する検証手法を提案している。
|
|
|
27 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
|
|
|
28 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
|
|
|
29
|
|
|
30 本研究は、CbCプログラムが状態遷移記述になることに着目し、
|
|
|
31 状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
|
|
|
32 状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
|
|
|
33 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
|
|
|
34 れる。
|
|
|
35
|
|
20
|
36 \section{Continuation based Cの概要}
|
|
|
37 CbC は、C言語を制限したもので、機械依存性の無いアセンブラのような構成になっており、
|
|
|
38 C言語からループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
|
|
|
39 この言語は、C言語に継続専用のプログラム単位であるコード(code)と、
|
|
|
40 継続(goto)を導入した構成となっている。
|
|
|
41 継続とは、次に実行すべきコードを直接または間接的に指定する手法である。
|
|
|
42 CbC は、サブルーチンよりも小さいプログラム単位であるコードを導入しているため、
|
|
|
43 C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
|
|
|
44
|
|
|
45 CbCはコードセグメントを引数付きgoto文で接続することで継続を実現している。
|
|
|
46 コードセグメントとは、codeという型で定義されるプログラム単位である。
|
|
|
47 原則として、このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
|
|
|
48 また、コードセグメントからの脱出も引数付きgoto文によってのみ行われる。
|
|
|
49 つまり、CbCプログラムは、複数のコードセグメントが引数付きgoto文で接続された構造になる。
|
|
|
50
|
|
|
51 CbCのコードセグメントと引数付きgoto文、ifはそれぞれオートマトンの状態と状態遷移および
|
|
|
52 遷移条件に対応しており、CbCプログラムは状態遷移記述であると言える。
|
|
|
53 また、CbCにおける並列動作はコードセグメント単位となる。
|
|
|
54
|
|
|
55 CbCはC言語の下位言語であるが、C言語のサブルーチンへ戻るための環境付き継続を
|
|
|
56 導入することでC言語の上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
|
|
|
57 CwCでは、CbCから通常のC言語の関数を呼び出すことができる。
|
|
|
58
|
|
|
59 \section{他の検証ツール}
|
|
|
60 有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。
|
|
|
61 その代表的なツールとしてSPINとJava PathFinder(JPF)があげられる。
|
|
|
62
|
|
|
63 SPINは、プログラム変換的な手法で検証するツールで、
|
|
|
64 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
|
|
|
65 それを基にC言語で記述された検証器を生成するものである。
|
|
|
66 チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
|
|
|
67 SPINでは、アサーション、デッドロック、到達性、進行制、LTL式の
|
|
|
68 性質について検査することができる。
|
|
|
69 また、SPINの並列動作はステートメント単位となる。
|
|
|
70
|
|
|
71 JPFは、実行可能なJavaのバイトコードを検証するためのシステムである。
|
|
|
72 バイトコードを状態遷移モデルとして扱い、
|
|
|
73 実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
|
|
|
74 キャッチされていない例外(NullPointerExceptionやAssertionErrorなど)を
|
|
|
75 検出することができる。
|
|
|
76 JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
|
|
|
77 があげられる。
|
|
|
78
|
|
|
79 また、JPFはJVMベースであるため、複数のプロセスの取扱いができない。
|
|
|
80 他にも、実用規模のプログラムは一般的に状態空間が巨大であるため、
|
|
|
81 直接実行することはできない。
|
|
|
82 そのため、プログラムの一部を抜き出して、
|
|
|
83 それに対してデバッグをするのに使用される。
|
|
|
84 他にも、Javaを仕様記述言語としてプロトコルの検証などに用いられる。
|
|
|
85 JPFの並列動作はスレッド単位となる。
|
|
|
86 \section{実装}
|
|
|
87 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
|
|
|
88 これは資源共有問題の一つで、次のような内容である。
|
|
|
89 5人の哲学者が円卓についており、それぞれ思索と食事を交互に繰り返す。
|
|
|
90 円卓には5本のフォークが置かれており、哲学者は左右のフォーク2本を使って食事をする。
|
|
|
91 フォークが取れない場合はフォークが空くのを待つ。
|
|
|
92 この問題では、すべての哲学者が一斉に左手でフォークを取るとデッドロックが起きる。
|
|
|
93 例として、左手でフォークを取るコードセグメントを示す。
|
|
|
94 {\footnotesize
|
|
|
95 \begin{verbatim}
|
|
|
96 code pickup_lfork(PhilsPtr self)
|
|
|
97 {
|
|
|
98 if (self->left_fork->owner == NULL) {
|
|
|
99 self->left_fork->owner = self;
|
|
|
100 goto pickup_rfork(self);
|
|
|
101 } else {
|
|
|
102 goto pickup_lfork(self);
|
|
|
103 }
|
|
|
104 }
|
|
|
105 \end{verbatim}
|
|
|
106 }
|
|
|
107 codeがコードセグメントの定義であり、
|
|
|
108 コードセグメントの引数部分をインターフェースと呼ぶ。
|
|
|
109 このコードセグメントは左手でフォークが取れた場合は、
|
|
|
110 右手でフォークを取るコードセグメントへ遷移する。
|
|
|
111 取れなかった場合は、またこのコードセグメントへ遷移する。
|
|
|
112
|
|
|
113 次に、タブロー法による状態の展開の実装について説明する。
|
|
|
114 タブロー法による状態の展開をタブロー展開と呼ぶ。
|
|
|
115
|
|
|
116 CbCプログラムのタブロー展開の特徴として、
|
|
|
117 プログラムの可能な実行の組み合わせすべてを調べる、
|
|
|
118 プログラムの状態を展開するために状態の探索をDepth First Search(DFS)で行う、
|
|
|
119 プログラムの実行によって生成される状態は木構造で記録する、
|
|
|
120 同じ状態はすべて共有することでメモリ消費を減らす、
|
|
|
121 があげられる。
|
|
|
122
|
|
|
123 まず、最初に状態として扱うすべての変数をBinary Tree構造で記録する。
|
|
|
124 そして、検証対象のプログラムのコードセグメントを実行して、
|
|
|
125 実行に伴う状態の変化をBinary Tree構造で記録していく。
|
|
|
126 このBinary Treeを状態データベースと呼ぶ。
|
|
|
127 すべての可能な実行の組み合わせを実行しながらそのときの状態を
|
|
|
128 状態データベースに登録していくことで状態を展開する。
|
|
|
129
|
|
|
130 以下にタブロー展開を行うためのタブローコードセグメントを示す。
|
|
|
131 {\footnotesize
|
|
|
132 \begin{verbatim}
|
|
|
133 code tableau(TaskPtr list)
|
|
|
134 {
|
|
|
135 StateDB out;
|
|
|
136 if (lookup_StateDB(&st, &state_db, &out)) {
|
|
|
137 while(!(list=next_task_iterator(task_iter))) {
|
|
|
138 TaskIteratorPtr prev_iter=task_iter->prev;
|
|
|
139 if (!prev_iter) {
|
|
|
140 memory_usage();
|
|
|
141 goto ret(0),env;
|
|
|
142 }
|
|
|
143 free_task_iterator(task_iter);
|
|
|
144 task_iter=prev_iter;
|
|
|
145 }
|
|
|
146 restore_memory(task_iter->state->memory);
|
|
|
147 } else {
|
|
|
148 task_iter=create_task_iterator(list,out,task_iter);
|
|
|
149 }
|
|
|
150 goto list->phils->next(list->phils,list);
|
|
|
151 }
|
|
|
152 \end{verbatim}
|
|
|
153 }
|
|
|
154 検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
|
|
|
155 \verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
|
|
|
156 得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
|
|
|
157 変数を記録したBinary Treeをコピーして登録していく。この際、同じ内容の変数が
|
|
|
158 あった場合は、同じ領域を指すことで状態を共有するようにする。
|
|
|
159
|
|
19
|
160 {\small
|
|
|
161 \begin{thebibliography}{9}
|
|
|
162 \bibitem{bib:jssst2000kono}
|
|
|
163 河野真治. ``継続を持つCの下位言語によるシステム記述''.
|
|
|
164 日本ソフトウェア科学会第17回大会, 2000.
|
|
|
165 \bibitem{bib:sigos2007}
|
|
|
166 下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
|
|
|
167 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
|
|
|
168 \end{thebibliography}
|
|
|
169 }
|
|
|
170 \end{document}
|
