TEF/テスト技法/モデルチェッキング

TEF/テスト技法

技法名　モデルチェッキング †

技法名（英語）　model checking †

説明 †

構造ベースのホワイトボックステスト技法の1つです。静的解析へ分類すべきかもしれません。

この技法は、システムの振舞い仕様（状態遷移などの外部に見える挙動）が要件を満たすかどうかを検証します。つまり、コードからではなく設計の段階で振舞い仕様が正しいかどうか検証する方法です。

特に、SPINというモデルチェッキングツールを用いた検証が有名で、SPINは、Promelaという仕様記述言語で振舞い仕様を記述し、それをSPINを用いて動かすことによって状態空間の網羅的な探索を行い設計の不備を検証します。

富士ゼロックスの山本らは、Executable UML(Bridge Point)を用いて書いたステートチャートをPromela言語へ自動変換することで、大規模なモデルチェッキングを可能としています（C言語換算で3万行程度のプログラムに対して300万のモデルチェックを自動で実施）。

使用例 †

次のプログラムは、『SPINモデル検査』という本に掲載されているPromelaのプログラムです。

mtype = {F, S };

mtype turn = F;

active proctype Producer ()

{

　do

　　:: (turn == F) -> printf("Producer\n"); turn = S;

　od

}

active proctype Consumer ()

{

　do

　　:: (turn == S) -> printf("Consumer\n"); turn = F;

　od

}

これは、ProducerとConsumerという2つのプロセスを定義しているものです。

Producerはガード条件（大域変数turn）がFであることをチェックして、Fなら"Producer\n"と出力し、ガード条件をSに変更するという処理が書いてあります。 Consumerの方は、ガード条件がSであることをチェックしてSなら"Consumer\n"を出力してガード条件をFに変更します。

SPINは上記プログラム(alt1.pというファイルに書き込んでおく）を読み込んで逐次実行するインタプリンターですから、

spin -u100 alt1.p

とすると、100回実行し、つまりは、 Producer Consumer Producer Consumer …… という出力結果となります（SPINはWindows上で動くフリーソフトですのでcygwin環境上で誰でも実際に動かして体験できます）。

なーんだ当たり前じゃないかという感じなのですが、このプログラムにちょっとだけ手を加え、activeの2行に対して、それぞれ、

active [2] proctype Producer ()

active [2] proctype Consumer ()

として、ProducerとConsumerという各プロセスを2つずつ実行させると今度は、交互に出力せずにProducerが連続したりConsumerが連続したりすることがあります。

もし、交互に出力させたいのなら

　　:: (turn == F) -> printf("Producer\n"); turn = S;

を

　　:: atomic { (turn == F) -> turn = N};

　　printf("Producer\n"); turn = S;

とし、実行順番が来たら大域変数turnをNに設定して他のプロセスのガード条件が成り立たなくする必要があります（atmicは{……}内を他のプロセスに邪魔されない実行単位とするという意味です）。

このように、Promelaで肝となる部分を記述し、不整合が起こらないか事前チェックするというのが基本的な方法です。

補足 †

SPINとは、"Simple Promela Interpreter"の略で、"Promela"は、Gerard J. Holzmannが作った並列処理を伴う状態遷移（オートマトン）を記述できる形式仕様記述言語のことです。

参考文献 †

書籍： SPINモデル検査

total 734 today 1 yesterday 0