| 講演名 | 2011-10-20 上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査(ネットワーク環境でのディペンダビリティ,及び一般) 井上 裕之, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | モデル検査において上界のない整数型変数を有するシステムを対象とした場合,状態数は無限となるため,状態全てを個々に探索することは不可能である.そこで,k帰納法を用いたモデル検査によって,この無限状態の検証を行う方法を議論する.SMTソルバを用いて,上界のない整数型変数を含む式の充足可能性判定を行うことで,k帰納法を実現することができる.しかし,並行プログラムを対象とした場合,検証に時間がかかってしまうことが多い.この原因は,並行プログラムのような非同期システムでは,遷移関係を表す論理式の簡潔な表現が得られないためである.そこで本研究では,その問題を解決するため,よりコンパクトな遷移関係の式表現を用いた手法を提案する. |
| 抄録(英) | We discuss k-induction-based model checking that uses a Satisfiability Modulo Theories (SMT) solver. The state space of a system with unbounded integer variables is infinite; thus it is impossible to visit all of its states. K-induction is one of the model checking approaches that can be used to reason about such an infinite state space. In this approach, the problem of model checking is reduced to the satisfiability problem that can be solved by an SMT solver. However, this approach does not work effectively when applied to concurrent programs, because the formula representing the behaviors of systems with high concurrency tends to become very large. To overcome this problem, we propose an alternative approach that uses more compact formulas. |
| キーワード(和) | モデル検査 / k帰納法 / SMT / 並行システム |
| キーワード(英) | model checking / k-induction / SMT / concurrent systems |
| 資料番号 | DC2011-20 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2011/10/13(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査(ネットワーク環境でのディペンダビリティ,及び一般) |
| サブタイトル（和） | |
| タイトル（英） | K-induction-based model checking of concurrent systems with unbounded integer variables |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | k帰納法 / k-induction |
| キーワード(3)（和/英） | SMT / SMT |
| キーワード(4)（和/英） | 並行システム / concurrent systems |
| 第 1 著者 氏名（和/英） | 井上 裕之 / Hiroyuki INOUE |
| 第 1 著者 所属（和/英） | 大阪大学 Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro TSUCHIYA |
| 第 2 著者 所属（和/英） | 大阪大学 Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru KIKUNO |
| 第 3 著者 所属（和/英） | 大阪大学 Osaka University |
| 発表年月日 | 2011-10-20 |
| 資料番号 | DC2011-20 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | 252 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |