グラフィック入力のツールも
モデル検査を行う際はツール内部だけでなく，使い手側の工夫も必要である。探索アルゴリズムの工夫だけで状態爆発を抑えられるわけではないため，使い手がプログラムの論理構造を抽出し，探索範囲を狭めた上で状態遷移モデルを作成する必要がある。例えば，プログラム中のループの回数を減らしたり，特定の代表値に置き換えたりする。モデル検査の適用経験が豊富なメルコ・パワー・システムズの早水氏によると，モデル作成の際「まず，わざと状態爆発するようなモデルを作成し，状態爆発の程度を見ながら徐々に絞り込んでいくのがいい」という（図6）。
図6 始めはわざと状態爆発させる
モデル検査でモデルを作成する際は，現在のコンピュータやアルゴリズムの制約内で探索可能な状態空間に収める必要がある。ただし，その境界はつかみにくいため，始めはわざと状態爆発させ，その後，徐々に状態を絞り込んでいく。
モデル検査ツールでは，状態遷移系を時系列に展開した際の状態遷移パスのノード数を表示する機能があり，この数の増え方があまりに急な場合は現実的な時間内に探索が終了しない。このため，ノード数の増え方がある一定のスピード以下になるまで状態空間の削減を続ける。
なお，現在，モデル検査用の状態遷移モデルを作成する場合は「SMV」や「Promela」など各ツール専用の言語で記述する必要がある。このため，事前に状態遷移図表などを用意してあったとしても，各専用言語への変換の手間が必要となる。そこで最近では，状態遷移図表をGUIで直接入力できるモデル検査ツールも登場している（図7）。
図7 グラフィカルにモデルを入力できるツールも登場
モデル検査を行うためには，従来は「Promela」や「SMV」などのモデル検査用の言語でモデルやプロパティを人手で作成する必要があった。現在では「Uppaal」や「SCADE」など，グラフィカルなモデルを直接入力できるモデル検査ツールが登場している。
[画像のクリックで拡大表示]
