上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査(ネットワーク環境でのディペンダビリティ,及び一般)

スポンサーリンク

概要

論文の詳細を見る
モデル検査において上界のない整数型変数を有するシステムを対象とした場合,状態数は無限となるため,状態全てを個々に探索することは不可能である.そこで,k帰納法を用いたモデル検査によって,この無限状態の検証を行う方法を議論する.SMTソルバを用いて,上界のない整数型変数を含む式の充足可能性判定を行うことで,k帰納法を実現することができる.しかし,並行プログラムを対象とした場合,検証に時間がかかってしまうことが多い.この原因は,並行プログラムのような非同期システムでは,遷移関係を表す論理式の簡潔な表現が得られないためである.そこで本研究では,その問題を解決するため,よりコンパクトな遷移関係の式表現を用いた手法を提案する.
2011-10-13

著者

関連論文

もっと見る

スポンサーリンク