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

本発表では,プリエンティブなマルチタスク環境で動作する組込み制御ソフトウェアにおけるデータの整合性を検証する環境を提案する.組込み制御ソフトウェアではMATLAB/Simulinkなどを用いたシミュレーションにより,制御ロジックの検証は可能になっている.一方,マルチタスク構成のソフトウェアの振る舞いの検証は自動化できるに至っていない.本発表ではモデル検査ツールSPINを用いて組込み制御ソフトウェアのデータの整合性を検証する手法と,UML記述されたソフトウェアモデルからデータ整合性検証のためのPromelaコードを生成するツールを提案する.これにより組込み制御ソフトウェアの開発効率向上を目指す.