産業クリティカルシステムに対するフォーマルメソッドの応用に関する会議FMICSの動向
MRI
石黒正揮
2015/6/23開催
情報源
http://web.archive.org/web/20150421095044/http://fmics2015.org/welcome.html
概要
FMICS(International Workshop on Formal Methods for Industrial Critical Systems)は、産業クリティカルシステムに対するフォーマルメソッドの応用に関する研究者、技術者の議論の場として1996年から毎年開催されている。フォーマルメソッドの代表的な国際会議International Symposium on Formal Methodsに併設開催されている。2015年のFMICSでは、セッションは、産業応用、プロトコル、仕様と解析、検証などから構成されており、フォーマルメソッドを用いた設計、仕様、コード生成、テスト、認証、ツール、ケーススタディ、影響効果などに係る研究発表が行われている。産業応用に関しては、自動車分野におけるモデル検査の適用に関する研究が注目される。オックスフォード大学Peter Schrammelの研究"Successful Use of Incremental BMC in the Automotive Industry"においては、ソフトウェアモデルチェッカーCBMCを拡張しインクリメンタルBMCに対応させることで、自動車の制御ソフトウェアの検証において、従来のBMCよりも１桁の高速化が実現できることを示している。インクリメンタルBMCは、時間フレーム0～(k+1)までのモデル検査を繰り返し行う際に、時間(k+1)のモデル検査において、0～kまでのモデル検査で生成した内部状態を活用することにより高速化を図る技術である。
コメント
ERCIM(European Research Consortium for Informatics and Mathematics)が主体となり欧州のフォーマルメソッド関係者が中心となって20年近くに渡り開催されている。フォーマルメソッドの産業分野への応用は長年の目標である。
このページの先頭へ戻る