モデル検査の応用 徳田研究室 西村太一.

Presentation on theme: "モデル検査の応用 徳田研究室 西村太一."— Presentation transcript:

1 モデル検査の応用 徳田研究室 西村太一

2 目次 モデル検査とSPINついて 仕様の検証例 Cプログラムの検証例 問題点 プログラムをそのまま検査するツールの紹介

3 モデル検査とは ハードウェアやソフトウェアの「モデル」が形式仕様を満足するか検証 状態遷移系を網羅的にチェック
状態の組み合わせが爆発しないように数理論理学の手法を用いる 命題の記述には時相論理が使われることが多い

4 SPINとは Promelaという言語で状態遷移系を記述 日本語の本も出版されているくらいメジャー 命題は時相論理式で記述
シェルスクリプトに似た文法 日本語の本も出版されているくらいメジャー 命題は時相論理式で記述 [] p 今も将来もずっとpが成り立つ <> p 将来いずれpが成り立つ P U q qが成り立つまではpが成り立つ ->, <->, !, &&, ||

5 仕様の検証 仕様書に漏れがないか確認する 例として自動販売機の検証を行う

6 仕様書 静的な状態 コイン投入口、コイン返却口、商品取出口、電源がある 使用できる硬貨は100円硬貨のみ
ジュースはAとBの2種類でどちらも1缶100円 ジュースの在庫量はそれぞれ5つずつ 貯蔵可能なコインの最大枚数は3枚 3つの状態を持つ 停電状態＝電源OFF 待機状態＝電源ON コイン投入状態＝コインが投入されている状態

7 仕様書(2) 動的な振舞い 停電状態において電源がONにされた場合、待機状態に遷移 停電状態にコインが投入された場合は
ジュースの在庫がともに0の場合は、投入されたコインをコイン返却口に返却し、待機状態を維持 どちらかのジュースの在庫がある場合、投入されたコインを貯蔵し、コイン投入状態に遷移 コイン投入状態においてさらにコインが投入された場合は 貯蔵したコインが3枚の場合、投入されたコインをコイン返却口に返しコイン投入状態を維持 3枚未満の場合は投入されたコインを貯蔵し、コイン投入状態を維持 コイン投入状態において購入ボタンが押された場合は… etc

8 Promelaコード（抜粋） if ::total==Unpower -> :: power==On -> total=Wait
:: (power!=On) && coinIn==On -> rest=1; :: else -> skip fi ::total==Wait -> :: (power!=Off && coinIn==On && stkA==0 && stkB==0) -> rest=1; :: (power!=Off && coinIn==On && !(stkA==0 && stkB==0)) -> stkC++; total==CoinIn :: (power==Off) -> total=Unpower ::total==CoinIn -> :: (power!=Off && coinIn==On && stkC==3) -> rest=1

9 LTL式の例 停電状態において電源がONにされた場合、待機状態に遷移する
[]((total==Unpower && power==On) -> <>total==Wait) 待機状態においてコインが投入された場合、いずれかのジュースの在庫がある場合、コインを貯蔵しコイン投入状態に遷移する []((total==Wait && coinIn==On && !(stkA==0 && stkB==0)) -> <>(total==CoinIn && stkC==1)) コインを投入したら、必ず商品を得るかコインが戻ってくる [](coinIn==On -> <>(outlet!=No || rest!=0))

10 検証の結果 それぞれのLTL式に対して、validかinvalid、どちらかの結果が得られる
コイン投入状態でAの在庫が0でBの在庫が1以上の場合、ボタンAが押されると何も起こらない。したがって「必ず商品を得るかコインが戻ってくる」とはいえない 電源Offとコイン投入が同時に発生した場合に、電源Offを優先すると、コイン投入の情報が失われてしまう ボタンAとボタンBが同時に押されたときの振る舞いも未定義

11 簡単なCプログラムの検証 次のようなプログラムに対して検査を行う 整数（1から1000まで）を入力する
入力した整数が6で割り切れれば“OK”を出力 入力した整数が6で割り切れなければ“NG”を出力

12 Cプログラム #include <stdio.h> main(){ int a;
printf(“a = ? >>>”); scanf(“%d”, &a); if(a % 6 == 0){ printf(“OK\n”); }else{ printf(“NG\n”); }

13 Promelaコード mtype = {OK, NG, NT}; int seisu = 1; int a; mtype prt;
active proctype p(){ prt = NT; do :: (seisu <= 1000) -> a=seisu; if ::(a % 6 == 0) -> prt = OK; prt = NT ::else -> prt = NG; fi; seisu++ ::else -> break od }

14 LTL式 [](p -> q) 6で割り切れるときには決してNGにはならない 6で割り切れないときには決してOKにはならない
#define p (a % 6 == 0) #define q (prt != NG) 6で割り切れないときには決してOKにはならない #define p (a % 6 != 0) #define q (prt != OK)

15 問題点 元のCプログラムは、1から1000までという限定した値のみを受け取るようにはできていない
入力値が網羅的なので、状態組み合わせが爆発しがち この程度のテストであれば一般的なテストツールで十分 複数のスレッド間の並列動作の検証などではかなり有効

16 問題点（2） プログラムをPromelaコードに手作業で変換するのは面倒 Promelaコードを美しく書くのは非常に困難
『4日で学ぶモデル検査』に載っている例はコピペばかり XMLのように自動生成して使うもの？

17 Cプログラムをそのまま検査するツール BLAST SLAM 述語抽象化法でモデル検査
２つの定理証明器 SIMPLYFY と VAMPYREを使用 SLAM Microsoft製 Static Driver Verifierに含まれている 仕様記述言語SLICによって、APIの使用法が正しいかどうかを検証

18 Javaプログラムの検査 JPF(Java Path Finder) Bandera Bogor、JNuke Javaのバイトコードを検証
ソースコード中にアサーションや抽象化した述語変数などの注釈を埋め込む Bandera LTL式によって検証 SPIN、SMV、JPFといった外部のモデル検査器を利用 Bogor、JNuke