| 講演名 | 2003/1/23 ペトリネットに対するSATを利用したモデル検査の効率化 市原 浩司, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | モデル検査は有限状態のシステムに対する自動検証手法である.近年,論理式の充足可能性判定(SAT)を利用した限定モデル検査が新しいモデル検査手法として注目されている.しかし,非同期並行システムを対象とした場合,判定する論理式が複雑になるため検証時間が非常に大きくなるという問題があった.そこで本稿では,非同期並行システムのモデルであるペトリネットを対象として,新しい論理式の生成手法を提案する.また提案法では,一度に検証できる状態空間の大きさが,検証の際に考慮するトランジションの順序に依存するという特徴を持つ.本稿では,この順番の決定法についても考察し,効果的なヒューリスティックを開発する. |
| 抄録(英) | Model checking is an automatic approach to verification of finite-state systems. Recently bounded model checking, which uses prepositional satisfiability decision procedures (SAT), has received attention as a new model checking technique. For asynchronous concurrent systems, however, this technique does not work efficiently. This is because the propositional formulas used in verification often become very large in size for such systems, thus resulting in large computation time. In this paper, we take Petri nets as a plausible model for asynchronous concurrent systems and propose a new encoding scheme to address the problem by generating more succinct formulas. When this encoding is used, the verification performance depends critically on the ordering of transitions. We also propose a heuristic for this ordering and demonstrate its effectiveness by applying it to non-trivial examples. |
| キーワード(和) | モデル検査 / 充足可能性判定 / 非同期並行システム / ペトリネット |
| キーワード(英) | Model checking / SAT / asynchronous concurrent systems / Petri nets |
| 資料番号 | SS2002-28 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2003/1/23(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | ペトリネットに対するSATを利用したモデル検査の効率化 |
| サブタイトル（和） | |
| タイトル（英） | Improving the performance of SAT-based model checking for Petri nets |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model checking |
| キーワード(2)（和/英） | 充足可能性判定 / SAT |
| キーワード(3)（和/英） | 非同期並行システム / asynchronous concurrent systems |
| キーワード(4)（和/英） | ペトリネット / Petri nets |
| 第 1 著者 氏名（和/英） | 市原 浩司 / Koji ICHIHARA |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎工学研究科情報数理系専攻 Department of Informatics and Mathematical Science Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro TSUCHIYA |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科情報システム工学専攻 Depertment of Information Systems Engineering Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru KIKUNO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科情報システム工学専攻 Depertment of Information Systems Engineering Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2003/1/23 |
| 資料番号 | SS2002-28 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 616 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |