情報処理学会 第76回全国大会講演要旨

形式手法の一つであるモデル検査は近年のコンピュータの処理速度の向上によって形式手法の中でもより実用的な検証手段として期待されている。
従来、モデル検査は通信プロトコルや航空系などクリティカルなシステムへの適用が多く、適用範囲が限られたてきた。
そこで、本研究では組込みソフトウェア開発における、モデル駆動開発の手本としてUMTP　JAPANから提供されるモデルカタログから目標制御モデルを例に取り、目標制御モデルを使用した開発にモデル検査を適用しその過程をまとめ事例として報告する。