第6回：バグをしらみつぶしに探索，仕様精査やテストの手段に（1）

形式的手法の一種であるモデル検査（model checking）が流行の兆しを見せている。
アルゴリズムの改良やコンピュータの高速化が後押しし
LSI設計分野だけでなくソフトウエア分野においても実用段階に入りつつあるのだ。
上流工程で仕様のバグを機械的に検出するモデル検査技術を
人手に頼ることの多いテストやシミュレーションと組み合わせることで
より多様な観点からバグをつぶせるようになる。
現場のソフトウエア技術者が使いこなせる技術に成長してきた。

　モデル検査はこれまで研究対象として語られることが多かったため，一見，難しそうな印象があるが，その目的は非常にシンプルである。ひと言でいえば，ソフトウエアやハードウエアなど何らかのシステムの状態遷移モデルをコンピュータに入力することで，その振る舞いにおかしな点がないかどうかを，しらみつぶしにチェックする技術である。具体的には，入力した状態遷移系にデッドロックが潜んでいないかどうか^注1），到達しない状態はないか，など確かめたい検証項目を「プロパティ」としてコンピュータに与える（図1）^注2）。

図1　モデル検査の本質は「しらみつぶし探索」

モデル検査では，状態遷移系としてのモデル，およびそのモデルが満たすべき性質を検証したい項目「プロパティ」として用意し，ツールに入力する。プロパティには，次の状態遷移先が必ずあるか（デッドロック）や，ある状態Sがいつか必ず訪れるかどうか（活性：liveness property）などを与えることが多い。なお，プロパティとはモデルが適切かどうか（proper）という意味である。理論としては，モデル検査はモデル内のある状態sが，プロパティfを満たすかどうかという「Kripke構造」として定式化されている。

[画像のクリックで拡大表示]

注1） デッドロックとは，次の状態遷移先が存在しない状態のことをいう。

注2） モデル検査で与えるプロパティは，具体的には論理式で与える。「Aという論理式（命題）がずっと真であるかどうか」といった具合である。通常の論理式では「ずっと」や「いつかは」という時間的な概念を表記できないため，時間概念を論理式で書けるよう拡張した「時相論理（temporal logic）」と呼ぶ表記方法を使う。CTLやLTL，CTL^＊，μ計算といった形式がある。

　モデル検査の利点は，モデルとプロパティを与えてしまえば，あとはコンピュータが機械的にバグを探索する点だ。探索の途中で，デッドロックのように仕様を満たさない状態である「反例」が見つかれば，その時点で探索を終了し，バグが見つかったことを使い手に報告する。プロパティはシステムが満たすべき仕様であるため，反例が出れば元のソフトウエアにバグがあるというわけだ。「モデル検査の面白さは，不具合に至る状態が反例という形で明確に返ってくる点である」（国立情報学研究所 ソフトウェア研究系 教授の中島震氏）。