モデル検査とは
モデル検査とはシステムの網羅的な検査（テスト）を実現する技術です。もう少し詳しく述べると、システムを有限個の状態を持つモデルで表現した上で、システムが満たすべき性質がモデル上で成り立つかどうかを、モデルが取り得る全ての状態およびパス上で、機械的かつ網羅的に検査する技術です。しらみつぶしに検査するため、性質が成り立たない極めて特別な状態やパス――つまり不具合が1つでも存在した場合、必ず発見することができます。レアケースなど気付きにくいバグでも発見できるので、品質の高いソフトウェアを開発するための有効な手段の1つに挙げられます。
このモデル検査を、計算機上で全自動に実行するソフトウェアツールがモデル検査ツールです。代表的なモデル検査ツールを表1に列挙します。
| ツール | 概要 |
|---|---|
| SMV | カーネギーメロン大学で開発されたモデル検査ツールです。歴史とたくさんの実績があります。モデル記述言語は言語体系が容易で直感的に理解しやすく、状態遷移図・表からのモデル化に適しています。処理が高速で大規模なモデルを扱える特徴があります。 |
| SPIN | SMVと同様に歴史と実績があります。モデル記述言語がC言語と似ているため、プログラムのソースコードの検査が容易です。 |
| UPPAAL | ツールの画面上で状態遷移図を描画することでモデルの入力が可能なため、視覚的に優れています。実時間モデル検査ができることでも有名です。 |
多くのモデル検査ツールでは検査結果が「False」、すなわちモデルが検査式を満たさない場合には、その証拠として反例（counter example）が出力されます。反例とは、初期状態から不具合に至るまでのパス（path）のことで、システムの動作ログと同様に順を追って解析することにより不具合の原因を究明することができます。
モデル検査がどのような作業を経て行われるのか、ワークフローを図1に示します。
モデル検査で必要な作業は主に2つあります。1つは仕様書や設計書、ソースコードなどからモデルを設計し、モデル記述言語によりコーディングする作業です。本作業は「モデル化」と呼ばれています。もう1つは要求仕様書や試験仕様書等から検査式を作成し、時相論理式と呼ばれる論理式で表現する作業です。モデルと検査式を1つのファイルに記述してモデル検査ツールに入力します。以降の検査はツールで自動的で行われて、検査結果として「True」または「False」が出力されます。検査結果が「False」の場合には合わせて反例が出力されます。
モデル検査の最大のメリットは網羅的な検査と反例出力といえます。一方で課題もあります。網羅的な検査を行うがゆえに、システムの規模すなわちモデルが巨大になると、計算機のメモリを消費し尽くす、あるいは現実的な時間で解を見つけられい「状態爆発」が発生してしまうことです。大規模なシステムの検査を行う場合は、モデル化の際に適切な抽象化や絞り込みが必要となります。
モデルと検査式の作成
ここでは、商用利用可能なモデル検査ツールの1つである「NuSMV」を用いて、実際にモデルと検査式を作成しながら、簡単な例題を解いていきます。NuSMVは公式Webサイトからダウンロードできます。GUIが付いたnuXmvもありますが、こちらは商用利用が不可なので注意が必要です。
例題として、表2に示す2つのオブジェクト「OBJ_A」と「OBJ_B」があり、それらが並行動作するシステムを取り上げます。表内の「st_」で始まる単語は、そのオブジェクトの状態を示しています。共に初期状態がst_1で、任意にどれか1つが発行されるイベント（EVENT）を入力して、遷移（上下に分割されたセルの1行目）とアクション（同セルの2行目）を行います。例えば、初期状態においてEVENT=1が発生すると、OBJ_Aはst_2という状態に遷移し、アクションは実行しません。続いてEVENT=1が発生すると、状態はst_1になり、「fg1 = TRUE」すなわち変数fg1にTRUEを代入するというアクション（処理）を行います。
NuSMVではモデルと検査式を記述したSMVファイルというファイルを作成します。リスト1には記述する内容の全体像を示します。VARでは変数宣言を行います。ASSIGN以下に全ての変数の初期状態と状態遷移の振る舞いを記述します。これがモデルです。検査式はSPECを先頭に付けて記述します。
MODULE main VAR ASSIGN SPEC
例題の変数宣言と初期状態はリスト2の通りです。
MODULE main
VAR
EVENT : 0..6; -- 取り得る値を宣言します 0は無しです
OBJ_A : {st_1, st_2, st_3}; -- 取り得る状態を宣言します
OBJ_B : {st_1, st_2, st_3};
fg1 : boolean; -- TRUEとFALSEなのでboolean型にします
fg2 : boolean;
ASSIGN
init(OBJ_A) := st_1; -- 初期状態はst_1です
init(OBJ_B) := st_1;
init(EVENT) := 0; -- 何もイベントがない状態です
init(fg1) := FALSE; -- 例題では初期状態はFALSEとしました
init(fg2) := FALSE;
次に全ての変数の状態遷移を記述します。NuSMVは状態遷移系の検査に向いているので、記述はとても簡単です。表の振る舞いをそのままコーディングすれば良いことになります。例としてリスト3に変数EVENTとOBJ_A、fg1の状態遷移を以下に示します。もちろん、OBJ_Bとfg2についても記述が必要です。
next(EVENT) := 1..6; -- 非決定的記述 next(OBJ_A) := case OBJ_A = st_1 & EVENT = 1 : st_2; -- st_1の状態でEVENT(1)を入力するとst_2に遷移 OBJ_A = st_1 & EVENT = 3 : st_3; OBJ_A = st_2 & EVENT = 1 : st_1; OBJ_A = st_2 & EVENT = 5 : st_3; OBJ_A = st_3 & EVENT = 1 : st_1; OBJ_A = st_3 & EVENT = 5 : st_2; TRUE : OBJ_A; -- その他の場合（値保持） esac; next(fg1) := case OBJ_A = st_2 & EVENT = 1 : TRUE; -- OBJ_Aがst_2でEVENT(1)を入力するとTRUEになる OBJ_A = st_3 & EVENT = 3 : FALSE; OBJ_A = st_3 & EVENT = 5 : FALSE; OBJ_B = st_2 & EVENT = 2 : FALSE; OBJ_B = st_3 & EVENT = 4 : TRUE; OBJ_B = st_3 & EVENT = 6 : TRUE; TRUE : fg1; -- その他の場合（値保持） esac;
変数EVENTでは、モデル検査ツール特有の記述方法である非決定的記述を用いています。このように記述すると、変数EVENTの値は遷移の都度、1から6の値のいずれかが代入されます。case文では、条件が成立しない場合を考慮して末尾にTRUE行（その他の場合）を記述します。この行はどの行にも該当しない場合に常に成り立つことから、状態遷移表中では状態の記述がないセルに該当します。モデルの記述はこれで完了です。
最後に検査式を作成します。例題では以下の性質を検査してみましょう。
性質：fg1とfg2が共にTRUEとなった後は、共にFALSEにはならないはずである
NuSMVでは論理式としてCTL（Computation Tree Logic）式を利用することができます。以下の基本パターンを組み合わせて検査式を作成します。
前述した性質はCTL式で以下のように表現できます。式で利用できるパターンは表3に示しました。
検査式：AG((fg1 = TRUE & fg2 = TRUE) -> !EF(fg1 = FALSE & fg2 = FALSE))
性質はシステムの全てのパスと状態で検査するため先頭にAG（Always Globaly）を付けます。
!EF(Exist Future)は、先頭に!（否定）があるので、将来存在しないという意味です。
->(Imply)は、A -> Bと記述して、AならばBであるという意味です。
検査式ができたので、モデルと合わせてSMVファイルに記述して保存します。SMVファイルの拡張子は「.smv」です。例題では「test.smv」としましょう。このファイルは、本記事のサンプルファイルとしてダウンロードできます。
ツールの実行と反例解析
ツールを実行してモデル検査を行ってみましょう。NuSMVはコマンドラインアプリケーションなのでコマンドプロンプトやターミナルで、「NuSMV test.smv」と入力して実行します。実行結果を図2に示します。
検査結果はFALSEでした。Counterexample以下に反例が出力されています。2つの状態遷移表と合わせて見ると分かりやすくなります。反例では検査した性質が成り立たないパス、すなわち「fg1とfg2が共にTRUEとなった後に、共にFALSEになってしまう」パスが示されています。初期状態から、0 1 3 1 1 4 2 2の順序でイベントが発行されると前述の性質を満たさないケースが発見されたわけです。こうして得られた事実を基にして、バグの発見につなげます。
