形式手法、ことモデル検査に関しては航空業界などで実用化されているという話。

実用化している理由として2つ挙げられている。1つには組み込みシステムの設計にモデルベース開発が浸透してきていること、もう1つには、形式検証、特にモデル検査ツールの進化である。

モデルベース開発を支えているのは、MATLAB SimulinkやEsterel Technologies SCADE Suiteなど。

モデル検査ツールは、SPIN、NuSMVほか、SMTベースのSAL、Prover Plug-Inなど。

世の中の動向として、設計言語からモデル検査ツールや定理証明ツールへのデータ変換を自動化する動きがある。

例えば、Simulink→SCADE→Lustre→SALなど。

Rockwellの著者らがNASAのファンドで開発した変換フレームワークでは、以下のデータを扱うことができる。

入力： Simulink、Stateflow、SCADEで記述されたモデル

出力： NuSMV、SAL、Prover（モデル検査）

　　　PVS、ACL2（定理証明）

　　　C、Ada（ソースコード）

上記入出力の関係は下記URLに図示されている。

http://shemesh.larc.nasa.gov/fm/fm-collins-formal-methods.html

この図は、元の論文でも使われている図である。

Miller, S. P., Whalen, M. W., and Cofer, D. D. 2010. Software model checking takes off. Commun. ACM53, 2 (Feb. 2010), 58-64. DOI= http://doi.acm.org/10.1145/1646353.1646372