抄録

◎金子　舟・千代英一郎（成蹊大）

モデル検査とは，検査対象となるシステムの振る舞いを反映したモデルを用いて計算機上で検査を行う手法である．状態やイベントに対する網羅的な検査が可能であり，高信頼システムの実現手法のひとつとして注目されている．モデル検査の実利用上の課題のひとつに，検査に必要となるモデルを正しく作成することの難しさがある．この問題に対し我々はシステムの正しい振る舞いを表す具体的な遷移例からプロセス式によるモデルを学習により自動生成する手法について検討している．本発表では，自動生成手法の実用化にあたり，利便性の点から必要とされるモデル生成の高速化に関する検討結果および予備評価について報告する．