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

モデル検査はシステムの仕様を有限の状態遷移モデルとして表現し，
状態遷移を網羅的に探索することで，仕様不適合や仕様の誤りを検
出することができる．一般にモデル検査の実施においては，検査対
象とするシステム自体の動作に加え，検査対象の動作に影響を与え
る外部環境の動作もモデル化しなければならない．しかし，外部環
境の動作を独立した状態遷移モデルにすると，検査対象のモデルと
の掛け合わせにより状態爆発が発生し，検査不能になりやすくなる
という問題がある．そこで本稿では，検査対象に影響を与える外部
環境の動作の種類を宣言的に記述し，検査対象のモデルに合成する
ことで，状態爆発の発生を抑える手法を提案する．