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

目次 モデル検査と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 -> :: 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

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、どちらかの結果が得られる コイン投入状態で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; fi; seisu++ ::else -> break od }

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)

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

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

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

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