| 講演名 | 2002/4/12 充足可能性判定を用いたモデル検査ツールの実装 田中 崇浩, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 記号モデル検査とは,有限状態機械としてモデル化されたシステムが与えられた仕様を満足するかどうかを,論理関数処理を用いて検査する形式的検証手法である.その一手法として,論理式の充足可能性判定問題に帰着させて検証を行う限定モデル検査と呼ばれる手法が知られており,線形時間論理(LTL)というクラスの時相論理式で記述された仕様に対して検証を行うためのアルゴリズムが提案されている.しかしこれまでに公開されている検証系では,安全性と活性を表す単純なLTL式のみしか検証することができなかった.そこで本研究では,このアルゴリズムに従って,任意のLTL式に対して検証が可能なモデル検査ツールの実装を行う.実験により,従来の2分決定グラフを用いる記号モデル検査手法が効率的に動作しないような問題例に対し,比較的高速に検証を完了できる場合があることを示す. |
| 抄録(英) | Symbolic model checking is an automatic technique for verifying a system modeled as a finite state machine by the manipulation of boolean formulas. Recently, a SAT-based symbolic model checking technique, called bounded model checking, was proposed. In this paper, we describe our model checking tool implementing this technique. The basic idea of the method is to consider a counterexample of a particular length k and generate a propositional formula that is satisfisble if such a counterexample exists. Theoretically the model checking technique can deal with LTL (linear temporal logic) specifications, and BMC, a tool based on this technique, has already been publically available; however, the current version of this tool can verify simple safety and liveness properties only. In contrast, our tool can verify arbitrary LTL formulas. The result of a case study shows that our tool can be used as an alternative when traditional BDD-based symbolic model checking cannot work efficiently. |
| キーワード(和) | 限定モデル検査 / 充足可能性判定 / 線形時間論理 |
| キーワード(英) | Bounded model checking / satisfiability decision / linear temporal logic |
| 資料番号 | DC2002-1 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2002/4/12(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 充足可能性判定を用いたモデル検査ツールの実装 |
| サブタイトル（和） | |
| タイトル（英） | Implementing a SAT-Based Model Checking Tool |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 限定モデル検査 / Bounded model checking |
| キーワード(2)（和/英） | 充足可能性判定 / satisfiability decision |
| キーワード(3)（和/英） | 線形時間論理 / linear temporal logic |
| 第 1 著者 氏名（和/英） | 田中 崇浩 / Takahiro TANAKA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro TSUCHIYA |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru KIKUNO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2002/4/12 |
| 資料番号 | DC2002-1 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 28 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |