モデル検査

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

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

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

問題を形式的に表現すると次のようになる。時相論理の論理式 p で表される属性について、初期状態 s のモデル M があるとき、 が成り立つかどうかを決定する。ハードウェアの場合のように 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

 関連項目 

 抽象解釈
 自動定理証明
 静的コード解析

 モデル検査ツール 
 SPIN

 外部リンク 
 記事 
 An Introduction to Model Checking at embedded.com

 研究グループ 
 Software Design Group at MIT
 Model Checking at Carnegie Mellon University
 Software Verification and Validation at UT Austin
 SAnToS Laboratory at K-State
 Automated Software Engineering at Nasa Ames Research Center
 NASA/JPL Laboratory for Reliable Software
 VLSI/CAD Research group - University of Colorado at Boulder
 Verification and Validation - Brigham Young University, Provo, Utah
 ParaDiSe Laboratory - Masaryk University in Brno
 VASY Research team - INRIA Rhône-Alpes, France
 Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands
 Software Modeling and Verification (MOVES) group  at RWTH Aachen University, Germany

 モデル検査ツール 
 EmbeddedValidator, The Matlab/Simulink/Stateflow/Targetlink Formal Verification Environment
 Statemate ModelChecker, Statemate Models Robustness Checking
 Statemate ModelCertifier, Statemate Models Requirements Certification
 Alloy language
 APMC
 LoTREC
 Bogor
 CADP
 CBMC, C/C++ プログラムの制限モデル検査
 GEAR, CTL、μ計算、specification patterns を用いたゲーム意味論ベースのモデル検査ツール
 Java Pathfinder
 LASH, Liège Automata-based Symbolic Handler
 LTSA
 MOPED
 MOPS, セキュリティに関するモデル検査プログラム
 NuSMV: a new symbolic model checker
 ORIS, CTL風の時相論理を使用したリアルタイム指向のシステム
 ProB
 ProofPower
 RAVEN (Real-Time Analysis and Verification Environment)
 RuleBase
 SATABS, C/C++ プログラムの述語抽象化
 Symbolic Model Checker (SMV)
 Verification Interacting with Synthesis (VIS)
 Database of Verification and Model Checking Tools (Yahoda)

Category:理論計算機科学
Category:形式手法
Category:数学に関する記事