モデル検査

モデル検査器のNuSMVを呼び出すアプリケーションを作成しました。 モデル検査によるソフトウェアテストの実践研究会が提供するモデル検査サービスの講習会に参加（2012年記事作成当時）してサーバ上で使用したので、これのWindows版のバイナリをPC上で動かそうと思い作成したものです。

モデル検査について知りたい方は、上記の研究会のページの 「モデル検査とは」こちらをご覧ください。（2014年8月18日修正：リンク切れのため別記事へのリンク作成）

準備としてNuSMVのページからバイナリを入手して、 NuSMV.exeとlibexpat.dllを配置する必要があります。

• 概要
• コマンド実行のGUI化

NuSMVのEXEファイルを外部プログラム通信コンポーネントから起動して、結果をテキストエリアに出力します。 検査対象のモデルはファイルで指定します。 ファイルの記述の仕方は上記の研究会のページ「検査ファイルについて」 NuSMVのマニュアルをご覧ください。（2014年8月18日修正：リンク切れのため修正）

コマンドラインアプリケーション実行のGUI化

NuSMVのEXEファイル(NuSMV.exe)とDLL(libexpat.dll)および対象とするモデルのファイルを同一のフォルダに配置して、 Windowsのコマンドプロンプトでそのフォルダに移動して下記のコマンドを実行すると、下図のように出力されます。

NuSMV.exe (モデルのファイル名)

このアプリケーションでは、このようなコマンドラインアプリケーションをGUIから実行するようにします。

下図は処理の一部を切り出したもので、外部プログラム通信コンポーネントに対して「実行プログラム名取得」 ファンクションで取得した文字列を引数として「通信先プログラムの設定」メソッドを起動し、 続いて「モード指定での通信先プログラムの起動」メソッドを実行させます。 このときのモード指定はfalse(非対話モード)としていて、 今回のように一回のコマンド実行で文字列の出力を取得したい場合に用います。 このように起動したときは、処理が完了したときに外部プログラム通信コンポーネントから処理完了イベントが発生するので、 そのイベント処理でテキストエリアに出力された文字列を設定しています。

上記と同一のコマンドの実行結果は概要の図になります。