モデル検査

モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。

解説

モデル検査はハードウェア設計に適用されることが最も多い。ソフトウェアに対するモデル検査は決定不能であるため、アルゴリズム的な手法だけでは完全ではなく、証明も反証もできない場合がある。

モデルはハードウェア記述言語や専用の言語で記述されたソースコードの形態となるのが一般的である。そのようなプログラムは有限状態機械に対応付けられ、ノード（接点）とエッジから成る有向グラフで表される。原子命題の集合は各ノードと対応し、一般にメモリ要素の内容に対応する。ノードはシステムの状態を表し、エッジはある状態から他の状態への遷移可能性を意味する。その場合、原子命題は実行のある時点で保持される基本的属性を表す。

問題を形式的に表現すると次のようになる。時相論理の論理式 p で表される属性について、初期状態 s のモデル M があるとき、[math]M,s \models p[/math] が成り立つかどうかを決定する。ハードウェアの場合のように M が有限であれば、モデル検査はグラフ探索に帰着できる。

実世界の問題を扱おうとしたとき、モデル検査は状態組み合わせ爆発問題（状態の数が膨大となって検査不能となること）に直面する。これに対応する方法はいくつか存在する。

記号的アルゴリズムは有限状態機械のグラフを作らず、命題論理の論理式によって暗黙のうちにグラフを表現する。Ken McMillan (1992年）の研究により、二分決定木の利用が一般的となった。最近では、SAT solver （充足可能性問題参照）をグラフ探索に使用するようになってきた。
半順序法は明確にグラフの形式をとっている場合に、考慮すべき並行プロセス群の独立した同時動作の数を削減することができる。考え方の基本は、A と B のどちらが先に実行されるかが証明に無関係なら（AB でも BA でも証明に関係しない場合）、それを考慮しないということである。
抽象解釈はシステムをまず単純化してから証明しようとする。単純化されたシステムは本来のシステムと等価な属性を持たないので、詳細化の工程が必須となる。一般に抽象化は「健全」でなければならない（抽象化されたシステムで証明された属性は本来のシステムでも真であること）。プログラムの抽象化の例として、ブーリアン以外の変数を無視し、ブーリアンの変数とプログラムの制御構造だけを考慮する場合がある。このような抽象化は劣悪のように見えるが、相互排他の属性を証明するには十分である。

モデル検査は当初、離散状態系の論理的正当性を調べるために開発されたが、リアルタイムシステムや限定された形式のハイブリッドシステムにも対応できるよう拡張されてきている。

参考文献

Automatic verification of finite state concurrent systems using temporal logic, E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems, 8(2), pp. 244–263, 1986年.

Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0792393805, オンライン版
Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999年.
Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004年. DOI

外部リンク

記事

An Introduction to Model Checking at embedded.com

研究グループ