Mercurial > hg > Papers > 2016 > atton-ipsjpro

comparison presentation/slide.md @ 53:fa1d602b1676

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add rbtree image
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 04 Aug 2016 18:11:02 +0900
parents 02e5ae71c319
children a0bffeced069
comparison
equal deleted inserted replaced
52:02e5ae71c319 53:fa1d602b1676
15 * 網羅的にテストできない 15 * 網羅的にテストできない
16 * ユニットテストと組み合わせて使う 16 * ユニットテストと組み合わせて使う
17 * 検証の計算システムで実行する(メタ計算) 17 * 検証の計算システムで実行する(メタ計算)
18 * Java Path Finder, Valgrind 18 * Java Path Finder, Valgrind
19 * 大規模システムは実行できない 19 * 大規模システムは実行できない
20
21 # ソフトウェアの信頼性向上手法
20 * アルゴリズムの正しさを証明する 22 * アルゴリズムの正しさを証明する
21 * Agda, Coq, Idris といった証明支援系でプログラムを記述する 23 * Agda, Coq, Idris といった証明支援系でプログラムを記述する
22 * 極めて難しい 24 * 極めて難しい
23 * 実装に対して適用できない 25 * 実装に対して適用できない
24 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする 26 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする
75 * メタレベルではポインタを扱っても良い 77 * メタレベルではポインタを扱っても良い
76 * TODO メタ計算の図 78 * TODO メタ計算の図
77 79
78 # CbC のメタ計算の実際 80 # CbC のメタ計算の実際
79 * プログラムで使用する Data Segment は Meta Data Segment で全て定義されている 81 * プログラムで使用する Data Segment は Meta Data Segment で全て定義されている
82
80 ``` 83 ```
81 union Data { 84 union Data {
82 struct Count { 85 struct Count {
83 int x; 86 int x;
84 } count; 87 } count;
92 unsigned int gotoCount; // メタ計算に必要なデータ 95 unsigned int gotoCount; // メタ計算に必要なデータ
93 unsigned int stepOfAddTen; 96 unsigned int stepOfAddTen;
94 }; 97 };
95 ``` 98 ```
96 99
100 # CbC のメタ計算の実際
97 * Meta Code Segment では Data Segment は struct Data という形で一様に処理される 101 * Meta Code Segment では Data Segment は struct Data という形で一様に処理される
98 * メタ計算と通常の計算は stub と meta によって接続される 102 * メタ計算と通常の計算は stub と meta によって接続される
103
99 ``` 104 ```
100 __code addTen_stub(struct Context* context) { 105 __code addTen_stub(struct Context* context) {
101 goto addTen(context, context->data[Count]); 106 goto addTen(context, context->data[Count]);
102 } 107 }
103 108
115 p.x = p.x*2; 120 p.x = p.x*2;
116 goto meta(context, ShowValue); 121 goto meta(context, ShowValue);
117 } 122 }
118 ``` 123 ```
119 124
125 # CbC のメタ計算の実際
120 * デフォルトの meta 126 * デフォルトの meta
121 * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう 127 * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう
122 128
123 ``` 129 ```
124 __code meta(struct Context* context, enum Code next) { 130 __code meta(struct Context* context, enum Code next) {
183 * 各ノードは赤または黒の色を持つ 189 * 各ノードは赤または黒の色を持つ
184 * ルートの色は黒である 190 * ルートの色は黒である
185 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない) 191 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
186 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である 192 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
187 * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる 193 * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
188 * todo 図を入れておこう 194
189 195 ![rbtree](./images/rbtree.svg){:width="35%"}
190 # Verification of Red-Black Tree
191 * どのような順番で要素が挿入されても常に仕様が満たされることを確認する
192 * 仕様を満たさないような挿入順番があればそれを表示する
193 * 木への挿入は有限の個数だけ行なわれる
194 196
195 # Verification Library Akasha 197 # Verification Library Akasha
196 * 本研究で作成した検証用メタ計算ライブラリ 198 * 本研究で作成した検証用メタ計算ライブラリ
197 * 実装コードの ``meta`` を上書きするだけで検証を行なうことができる 199 * 実装コードの `meta` を上書きするだけで検証を行なうことができる
198 * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙 200 * どのような順番で要素が挿入されても常に仕様が満たされることを確認する
199 * 挿入後の木はきちんとバランスしているかチェックする 201 * 仕様を満たさない挿入順番があればそれを表示
200 * Meta Data Segment に挿入順番や実行履歴を記憶させる 202 * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
203 * 挿入後の木はきちんとバランスしているかチェックする
204 * CbC のメタ計算 Akasha では要素数13個までチェックできた
205 * 実装にわざとバグを入れた場合にはバランスしていない入力例を返した
201 206
202 # C Bounded Model Checker 207 # C Bounded Model Checker
203 * Carnegie Mellon University で開発されている ANSI-C の記号実行モデルチェッカ 208 * Carnegie Mellon University で開発されている記号実行モデルチェッカ
209 * C, C++, Java に対応
204 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる 210 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
205 * Red-Black Tree を C に変換して検証 211 * コードを C に変換して検証
206 * 挿入順番は非決定的な入力 `nondet_int` を使う 212 * 挿入順番は非決定的な入力 `nondet_int` を使う
207 213 * 関数呼び出しやループは展開される
208 # Result of Verification 214 * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず
209 * CbC のメタ計算 Akasha では要素数13個までチェックできた 215
210 * CBMC ではチェックできなかった 216 # Conclusion
211 217 * 動作するプログラムの記述を変更せず検証を行なえた
212 | | akasha | CBMC | 218 * テストケースの自動生成+仕様の反例表示ができた
213 |----------------------------------|:------:|:----:| 219 * CBMC では検証できない範囲の検証を行なうことができた
214 | 要素数1個までは仕様を保証 | 可 | 不可 | 220 * 総当たりでチェックしているため
215 | 要素数13個までは仕様を保証 | 可 | 不可 |
216 | 実装にバグを入れた際に反例を表示 | 可 | 不可 |
217
218 221
219 # Comparison of tools 222 # Comparison of tools
220 223
221 | | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | 224 | | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind |
222 |------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:| 225 |------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:|
223 | 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 必要 | 必要なし | 必要なし | 必要なし | 226 | 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 別に記述 | 別に記述 | 必要なし | 必要なし |
224 | 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし | 227 | 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし |
225 | 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 | 228 | 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 |
226 | メモリリークなどの検出 | 今は不可能 | 不可能? | 不可能 | | | | 可能 | 229 | メモリリークなどの検出 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | 不可能 | 可能 |
227 | 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | ものによる | 可能 | | 230 | 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | 不可能 | 可能 | 不可能 |
228 | 反例の表示 | 可能 | 可能 | 不可能 | | | 不可能 | | 231 | 反例の表示 | 可能 | 可能 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 |
229 232
230 233
231 # Conclusion and Future Works 234 # Future Works
232 * CBMC では検証できない範囲の検証を行なうことができた 235 * 挿入だけでなく削除を含む赤黒木の仕様検証
233 * 動作するプログラムの記述を変更することなく検証を行なえた 236 * 状態の抽象化による探索の効率化
234 * テストケースの自動生成+仕様の反例表示ができた 237 * ポインタへの不正アクセス検出などの機能
235 * 今後の課題 238 * 言語処理系に検証を行ないやすくする機構の導入
236 * 挿入だけでなく削除を含む赤黒木の仕様検証 239
237 * 状態の抽象化による探索の効率化 240 # CBMC Informations
238 * ポインタへの不正アクセス検出などの機能 241 * CBMC 5.4
239 * 言語処理系に検証を行ないやすくする機構の導入 242 * 実行オプション
240 243 * cbmc --unwind 1
241 # TODO: おまけ 244 * cbmc --depth 400 --property verifySpecification.assertion.1
242 * cbmc のバージョン、オプション 245 * 赤黒木のCbC実装
243 * rbtree の行数 246 * 赤黒木部分のみ: 330行
244 * 実行時間 247 * スタックやメモリのアロケータなどを含める: 640行
245 248
246 249
247 250
248 <!-- vim: set filetype=markdown.slide: --> 251 <!-- vim: set filetype=markdown.slide: -->