演繹的モデル検査による自動詳細化検証手法

スポンサーリンク

概要

論文の詳細を見る
有限の状態遷移システム間において, 詳細化の簡単な場合である模倣関係の自動検証手法は, 既に開発されている. また, システムが無限の状態を有する状態遷移システムである場合は, Mannaらなどの演繹的手法によって検証することができる. しかしながら, 演繹的手法による検証作業には手作業が必要であり, 自動化が困難であるため, 大規模システムの検証作業は困難となる. そこで, 本稿では, Sipmaらの演繹的モデル検査手法を用いることで, 無限な状態遷移システム間の模倣関係を自動的に検証する方法について考察する.
2001-05-21

著者

関連論文

スポンサーリンク