状態遷移モデルに基づくプロセス仕様の到達可能性解析の効率化
高原 大介 (9551058)
筆者の属する研究グループでは, 工業製品に組み込まれたマイコンソフトを対
象とした仕様検証システムを開発している. 本システムでは, 検証法として到達
可能性解析が用いられている. これは, 入力された仕様か
ら到達可能性グラフを作成し, そのグラフを探索することにより, 検証したい
要求(検証項目)が成り立つかどうかを調べるという手法である.
ところが, 検証対象の仕様の規模が大きくなると, 作成される到達可能
性グラフのサイズが大きくなるという「状態爆発」の問題を抱えている.
このため, 計算機上で実用規模の仕様の検証を行うことは困難であることが多い.
これに対し, 本論文では, 与えられた仕様から検証項目に関連す
る部分だけを抽出し, その部分仕様に対する到達可能性グラフを作成して検証
を行う手法を提案する. 具体的には, 検証項目(論理式) φが全称閉
論理式のある部分クラスに属するとき, 条件「φが部分仕様に対して
成り立つならば, 全体仕様に対しても成り立つ」を満たす
部分仕様の抽出法を与えている.
さらに, 実際の空調機用マイコンソフトを例
としてとりあげ, その機能要求を, 上記の部分クラスの論理式で書き下す実験,
および本手法を用いて部分仕様を抽出する実験を行い, 本手法の
有効性を確認した.
本論文では, この実験内容と結果について詳しく説明する.