モデル検査のソースを表示

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

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

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

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

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

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

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

== 参考文献 ==
* [http://doi.acm.org/10.1145/5397.5399 ''Automatic verification of finite state concurrent systems using temporal logic''],  [[エドムンド・クラーク|E.M. Clarke]], [[アレン・エマーソン|E.A. Emerson]], and A.P. Sistla, [[Association for Computing Machinery|ACM]] Trans. on Programming Languages and Systems, 8(2), pp. 244&ndash;263, [[1986年]].

* ''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, ISBN 0792393805, [http://www.kenmcmil.com/thesis.html オンライン版]
* ''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年]].  [https://doi.org/10.2277/052154310X DOI]

== 関連項目 ==
<!-- === 関連技術 === -->
* [[抽象解釈]]
* [[自動定理証明]]
* [[静的コード解析]]

=== モデル検査ツール ===
* [[SPINモデルチェッカ|SPIN]]
<!-- リンク先があまりまともな内容ではないのでコメントアウト（訳者）
* [[BLAST|BLAST (Berkeley Lazy Abstraction Software Verification Tool)]]
* [[BOOP Toolkit]]
* [[Cadena]]
* [[Cadence SMV]]
* [[CHIC (electronics)|CHIC]]
* [[COSPAN]]
* [[Coverity]]
* [[HOL theorem prover]]
* [[Probabilistic Symbolic Model Checker]]
* [[PROSPER]]
* [[Rabbit Model Checker|Rabbit]]
* [[Symbolic Analysis Laboratory|SAL]]
* [[SLAM project]]
* [[Uppaal Model Checker|UPPAAL]]
* [[Markov Reward Model Checker (MRMC)]]
-->

== 外部リンク ==
=== 記事 ===
* [http://www.embedded.com/showArticle.jhtml?articleID=17603352 ''An Introduction to Model Checking''] at embedded.com

=== 研究グループ ===
* [http://sdg.lcs.mit.edu/ ''Software Design Group at MIT'']
* [http://www-2.cs.cmu.edu/~modelcheck/ ''Model Checking at Carnegie Mellon University'']
* [http://svvat.ece.utexas.edu/ ''Software Verification and Validation at UT Austin'']
* [http://www.cis.ksu.edu/santos/ ''SAnToS Laboratory at K-State'']
* [http://ase.arc.nasa.gov/ ''Automated Software Engineering at Nasa Ames Research Center'']
* [http://eis.jpl.nasa.gov/lars/ ''NASA/JPL Laboratory for Reliable Software'']
* [http://vlsi.colorado.edu/ ''VLSI/CAD Research group - University of Colorado at Boulder'']
* [http://vv.cs.byu.edu/ ''Verification and Validation - Brigham Young University, Provo, Utah'']
* [http://www.fi.muni.cz/paradise/ ''ParaDiSe Laboratory - Masaryk University in Brno'']
* [http://www.inrialpes.fr/vasy ''VASY Research team - INRIA Rhône-Alpes, France'']
* [http://fmt.cs.utwente.nl ''Formal Methods & Tools (FMT) group at The University of Twente, The Netherlands'']
* [http://www-i2.informatik.rwth-aachen.de ''Software Modeling and Verification (MOVES) group  at RWTH Aachen University, Germany'']

=== モデル検査ツール ===
* [http://www.osc-es.de/index.php?lang=2&idcat=18 '''EmbeddedValidator''', The Matlab/Simulink/Stateflow/Targetlink Formal Verification Environment]
* [http://www.osc-es.de/index.php?lang=2&idcat=19 '''Statemate ModelChecker''', Statemate Models Robustness Checking]
* [http://www.osc-es.de/index.php?lang=2&idcat=20 '''Statemate ModelCertifier''', Statemate Models Requirements Certification]
* [http://alloy.mit.edu/ Alloy language]
* [http://apmc.berbiqui.org/ APMC]
* [http://www.irit.fr/ACTIVITES/LILaC/Lotrec/modelchecking/index.htm LoTREC]
* [http://bogor.projects.cis.ksu.edu/ Bogor]
* [http://www.inrialpes.fr/vasy/cadp/ CADP]
* [https://www.cs.cmu.edu/~modelcheck/cbmc/ CBMC], C/C++ プログラムの制限モデル検査
* [http://jabc.cs.uni-dortmund.de/modelchecking/ GEAR], CTL、[[μ計算]]、[http://patterns.projects.cis.ksu.edu/ specification patterns] を用いた[[ゲーム意味論]]ベースのモデル検査ツール
* [http://javapathfinder.sourceforge.net/ Java Pathfinder]
* [http://www.montefiore.ulg.ac.be/~boigelot/research/lash/ LASH], Liège Automata-based Symbolic Handler
* [http://www.doc.ic.ac.uk/ltsa/ LTSA]
* [http://www.fmi.uni-stuttgart.de/szs/tools/moped/ MOPED]
* [http://www.cs.berkeley.edu/~daw/mops/ MOPS], セキュリティに関するモデル検査プログラム
* [http://nusmv.itc.it/ NuSMV: a new symbolic model checker]
* [http://www.stlab.dsi.unifi.it/oris/ ORIS], [[計算木論理|CTL]]風の[[時相論理]]を使用したリアルタイム指向のシステム
* [http://www.ecs.soton.ac.uk/~mal/systems/prob.html ProB]
* [http://www.lemma-one.com/ProofPower/index/ ProofPower]
* [http://www-ti.informatik.uni-tuebingen.de/~fmg/raven/raven.html RAVEN (Real-Time Analysis and Verification Environment)]
* [http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ RuleBase]
* [http://www.verify.ethz.ch/satabs/ SATABS], C/C++ プログラムの述語抽象化
* [https://www.cs.cmu.edu/~modelcheck/smv.html Symbolic Model Checker (SMV)]
* [http://vlsi.colorado.edu/~vis/ Verification Interacting with Synthesis (VIS)]
* [http://anna.fi.muni.cz/yahoda/ Database of Verification and Model Checking Tools] (Yahoda)

{{FOLDOC}}
{{DEFAULTSORT:もてるけんさ}}

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