| 講演名 | 2002/10/11 非同期並行システムに対するSATに基づくモデル検査 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 新しい自動検証手法として,論理式の充足可能性判定(SAT)を利用した限定モデル検査(Bounded Model Checking)と呼ばれる手法が注目されている.しかし従来の限定モデル検査手法には,非同期的に動作する並行システムを対象とした場合,判定する論理式が複雑になるため検証時間が非常に大きくなるという問題があった.そこで本論文では,非同期並行システムのモデルであるペトリネットを対象として,新しい論理式の生成手法を提案する.提案手法を用いてシステムの動作を簡潔な論理式で表現することによって,実用的な時間での検証が可能となる.実際の並行プログラムをモデル化したペトリネットの例を用いて提案法の有効性を実験的に示す. |
| 抄録(英) | Bounded model checking has received recent attention as an efficient verification method. The basic idea of this method is to reduce the model checking problem to the propositional satisfiability (SAT) decision problem. For asynchronous systems, however, this method does not work well because the resulting propositional formulas tend to become very large for such systems. In this paper, we take 1-bounded Petri nets as a plausible model of asynchronous systems and propose an alternative encoding method for them. This method is simple but can generate very succinct formulas, thus resulting in reduced verification times. |
| キーワード(和) | モデル検査 / 充足可能性 / 非同期システム / ペトリネット |
| キーワード(英) | Model checking / SAT / asynchronous system / Petri net |
| 資料番号 | DC2002-31 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2002/10/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 非同期並行システムに対するSATに基づくモデル検査 |
| サブタイトル（和） | |
| タイトル（英） | A SAT-based Model Checking Method for Asynchronous Concurrent Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model checking |
| キーワード(2)（和/英） | 充足可能性 / SAT |
| キーワード(3)（和/英） | 非同期システム / asynchronous system |
| キーワード(4)（和/英） | ペトリネット / Petri net |
| 第 1 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro TSUCHIYA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 菊野 亨 / Tohru KIKUNO |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2002/10/11 |
| 資料番号 | DC2002-31 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 378 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |