非同期並行システムに対するSATに基づくモデル検査
スポンサーリンク
概要
- 論文の詳細を見る
新しい自動検証手法として,論理式の充足可能性判定(SAT)を利用した限定モデル検査(Bounded Model Checking)と呼ばれる手法が注目されている.しかし従来の限定モデル検査手法には,非同期的に動作する並行システムを対象とした場合,判定する論理式が複雑になるため検証時間が非常に大きくなるという問題があった.そこで本論文では,非同期並行システムのモデルであるペトリネットを対象として,新しい論理式の生成手法を提案する.提案手法を用いてシステムの動作を簡潔な論理式で表現することによって,実用的な時間での検証が可能となる.実際の並行プログラムをモデル化したペトリネットの例を用いて提案法の有効性を実験的に示す.
- 2002-10-11
論文 | ランダム
- Comment on Higuchi's Paper "Is the Human Brain Running away?"
- 妊婦と抗菌剤の選択 (妊婦と感染)
- 腎生検による各種腎疾患の電子顕微鏡所見とその鑑別診断上の意義
- 平成21年度に向けた飼料作物の種子の動向
- 平成20年度に向けた飼料作物の種子の動向