無償で使えるソフトウェアモデル検査の体験ツール

モデル検査 メモ

ひょんなことから知ったのですが、「モデル検査によるソフトウェアテストの実践研究会」という団体が 「実践！ソフトウェアモデル検査」 というサイトを作っていたんですね。

モデル検査というとついつい理論的な研究が先行しがちですが、ここでは名前通り実践的な活動をしているようで、ソフトウェアへのモデル検査の適用事例 なんかも載っており、非常に興味深いです。ただ、事例を見ても、やはりモデル化できるのは1000行前後のコードくらいまでなんでしょうね。残念ながらまだまだターゲットは狭そうです。サイズはコンパクトだが状態遷移の固まり、といったアプリケーションの検証には絶大な効果を発揮できるんですけどね。

また、ここでは「モデル検査支援ソフトウェア」というものも公開しています。実体は、作図ツールの Visio とモデル検証器の NuSMV を繋ぐマクロ群＋そこから呼び出される Java ソフトのようなのですが、優れた既存のものを最大限活用して、最小限のコストで現場で使えるツールを作る、という姿勢は実践派の最たるものでしょう。

簡単にできることを紹介すると、「モデル検査支援ソフトウェア」に含まれる Visio のステンシルを使って、フロー図や状態遷移図を書くと（Flash デモ）、それを NuSMV のコードに変換して検証することができます。また、検査したい仕様を記述するための CTL 式の作成を支援する GUI （Flash デモ）と、NuSMV から出力された反例を図面上に戻して確認できる反例ビュワー（Flash デモ）が含まれています。

Visio を持っていない＆ Visio 2007 体験版 を落とすために個人情報をいろいろ記入するのが嫌だったために、実際の動作は確認できていませんが、充実の操作マニュアルを見るだけでも一通り使えるものができているように思います。

個人的な興味では、CTL 式の作成をサポートする GUI がホットトピックだったりするわけですが、やはり自然言語で書かれた検証したいこと（例：「Q以降でRより前の間で/Pに先だってSが成立する」）を一覧から選ばせて、その穴埋めの式を別に入力させる、という方法が無難そうですね。

まだ、ダミーノードを手動で置ねばならない制約が各所にあったり、30個までしか図形を配置できなかったりと、制限は多いですが、今後の発展が楽しみなツールです。モデル検査器の独自言語を学ばなくても使えますので、モデル検査の本質を短い時間で体験するような演習用にも最適ですね。

思い出したようにモデル検査を語ってみる

ちなみに、モデル検査を使ったテストの工程をぶっちゃけて言えば:

  1. 何らかの形で状態遷移機械としてターゲットを表現する
  2. 成り立って欲しい仕様を時相論理式で書く
  3. モデル検査器に上記２つを入れてしばらく（数秒〜数日）待つ
  4. 成り立っていたら True が返るので喜ぶ
  5. 成り立っていなかったら False が返り、反例として不成立になる状態遷移のステップが表示されるのでじっくり観察して満足する*1

ソフトウェアモデル検査といっても、今回公開されているようなツールを使用する場合は、検証対象のソフトウェアを分析して、検証したい要素を人力で抜き出していったん状態遷移モデルに変換してから、ツールに入れてあげないといけないため、なかなか大規模なソフトを検証することは難しいわけです。

ちなみに、ソフトウェアモデル検査ツールの中には、検証したい生のコードを直接流し込めるというアプローチのものもあるわけですが、その場合は何の性質を見たいのかをしっかり限定できないことには、現実的な時間で検査できるモデルはできません。特定の API の呼び出し方が条件を満たすか確認する、といった形での限定をかければ、Microsoft の Windows 向けの優れたドライバーとハードウェアの設計、開発、および認定 のように直接 C のコードを入力して検証する、といった応用の仕方も可能です。

Eclipse + NuSMV なツール

しかしながら、今回のツールもせっかく Java で書いているのですし、Eclipse + GEF を使ってモデルエディタも自作してみると、Visio が買えない人でも使えて嬉しいような気もします。というより、すでに有ってもおかしくない気もしますが、ないんでしょうか。

ということで、さくっとググってみましたが、OCaml + NuSMV で構成された C/C++ の検証ツールを Eclipse から呼び出すという論文(PDF) くらいしか見つかりませんでした。

こちらは AST から変数宣言・代入・参照の順番が正しいかをモデル検査で調べる、というお話で、確かに分岐条件を確認しなければモデルも小さくなりますので OpenSSL のソースに適用できたというのも頷けます。が、そんなことはコンパイラでも出力してくれる警告なので、ぶっちゃけ NuSMV までは必要ありません。もっとも、NuSMV を使っておけば、あとは時相論理式を工夫するだけでいろいろな性質を調べられるようになりますし、そういった拡張性・応用性のメリットは十分にあります。id でしか引かないデータを RDB に放り込むようなものですが、プログラムが組みやすくて応用も利けばそれもアリですよね。

「モデル検査！」と堅く考えずに、「状態遷移モデルと見なせそうな何かの様々な性質を調べるために便利に使えるエンジン」として NuSMV を使ってみるというのも一つのやり方かなぁ、と思う今日この頃でした。

追記: 大事なことを言い忘れていました

自分にとっては当然のことなのですっかり書き忘れていましたが、ここの存在意義のひとつなのでしっかりアピールしないと。ソフトウェアモデル検査は一般のプログラムに適用するにはまだかなり制限が強いのは上述のとおりですが、すぐにでも適用できそうなソフトウェアもあります。それがゲームのスクリプトです。

一般のソフトウェアモデル検査の難しいところは配列やポインタの存在だったり、アプリを取り巻く環境が内包している状態がやたら複雑だったり、といった点です。しかし、ADV のシナリオスクリプトにせよ、ゲーム AI の記述スクリプトにせよ、ゲームのスクリプトというのは、一般的に限られた変数で状態が遷移していくもので、ポインタなどが出てくることはほとんどありません。まさにモデル検査にうってつけの題材なのです！

というのがこの日記の主張のひとつです。実際に現場に導入するには何らかのツールのサポートが必要だとは思うのですけどね……。

*1:ときどき、反例を得るのが目的で、最初から不成立と分かっている式を入れてみたりもします。