モデル検査の応用徳田研究室西村太一目次 • モデル検査とSPINついて • 仕様の検証例 • Cプログラムの検証例 – 問題点 – プログラムをそのまま検査するツールの紹介モデル検査とは • ハードウェアやソフトウェアの「モデル」が形式仕様を満足するか検証 • 状態遷移系を網羅的にチェック – 状態の組み合わせが爆発しないように数理論理学の手法を用いる • 命題の記述には時相論理が使われることが多い SPINとは • Promelaという言語で状態遷移系を記述 – シェルスクリプトに似た文法 • 日本語の本も出版されているくらいメジャー • 命題は時相論理式で記述 – [] p • 今も将来もずっとpが成り立つ – <> p • 将来いずれpが成り立つ –P U q • qが成り立つまではpが成り立つ – ->, <->, !, &&, || 仕様の検証 • 仕様書に漏れがないか確認する • 例として自動販売機の検証を行う仕様書 • 静的な状態 – コイン投入口、コイン返却口、商品取出口、電源がある – 使用できる硬貨は100円硬貨のみ – ジュースはAとBの2種類でどちらも1缶100円 – ジュースの在庫量はそれぞれ5つずつ – 貯蔵可能なコインの最大枚数は3枚 – 3つの状態を持つ • 停電状態＝電源OFF • 待機状態＝電源ON • コイン投入状態＝コインが投入されている状態仕様書(2) • 動的な振舞い – 停電状態において電源がONにされた場合、待機状態に遷移 – 停電状態にコインが投入された場合は • ジュースの在庫がともに0の場合は、投入されたコインをコイン返却口に返却し、待機状態を維持 • どちらかのジュースの在庫がある場合、投入されたコインを貯蔵し、コイン投入状態に遷移 – コイン投入状態においてさらにコインが投入された場合は • 貯蔵したコインが3枚の場合、投入されたコインをコイン返却口に返しコイン投入状態を維持 • 3枚未満の場合は投入されたコインを貯蔵し、コイン投入状態を維持 – コイン投入状態において購入ボタンが押された場合は… – etc Promelaコード（抜粋） if ::total==Unpower -> if :: power==On -> total=Wait :: (power!=On) && coinIn==On -> rest=1; :: else -> skip fi ::total==Wait -> if :: (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 fi ::total==CoinIn -> if :: (power!=Off && coinIn==On && stkC==3) -> rest=1 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)) 検証の結果 • それぞれのLTL式に対して、validかinvalid、どちらかの結果が得られる • Invalidであったら、反例が得られ、仕様に漏れがあることがわかる – コイン投入状態でAの在庫が0でBの在庫が1以上の場合、ボタンAが押されると何も起こらない。したがって「必ず商品を得るかコインが戻ってくる」とはいえない – 電源Offとコイン投入が同時に発生した場合に、電源 Offを優先すると、コイン投入の情報が失われてしまう – ボタンAとボタンBが同時に押されたときの振る舞いも未定義簡単なCプログラムの検証 • 次のようなプログラムに対して検査を行う – 整数（1から1000まで）を入力する – 入力した整数が6で割り切れれば“OK”を出力 – 入力した整数が6で割り切れなければ“NG” を出力 Cプログラム #include <stdio.h> main(){ int a; printf(“a = ? >>>”); scanf(“%d”, &a); if(a % 6 == 0){ printf(“OK\n”); }else{ printf(“NG\n”); } } 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; prt = NT fi; seisu++ ::else -> break od } LTL式 [](p -> q) • 6で割り切れるときには決してNGにはならない – #define p – #define q (a % 6 == 0) (prt != NG) • 6で割り切れないときには決してOKにはならない – #define p – #define q (a % 6 != 0) (prt != OK) 問題点 • 元のCプログラムは、1から1000までという限定した値のみを受け取るようにはできていない • 入力値が網羅的なので、状態組み合わせが爆発しがち • この程度のテストであれば一般的なテストツールで十分 – 複数のスレッド間の並列動作の検証などではかなり有効問題点（2） • プログラムをPromelaコードに手作業で変換するのは面倒 • Promelaコードを美しく書くのは非常に困難 – 『4日で学ぶモデル検査』に載っている例はコピペばかり – XMLのように自動生成して使うもの？ Cプログラムをそのまま検査するツール • BLAST – 述語抽象化法でモデル検査 – ２つの定理証明器 SIMPLYFY と VAMPYREを使用 • SLAM – Microsoft製 – Static Driver Verifierに含まれている – 仕様記述言語SLICによって、APIの使用法が正しいかどうかを検証 Javaプログラムの検査 • JPF(Java Path Finder) – Javaのバイトコードを検証 – ソースコード中にアサーションや抽象化した述語変数などの注釈を埋め込む • Bandera – LTL式によって検証 – SPIN、SMV、JPFといった外部のモデル検査器を利用 • Bogor、JNuke