| 講演名 | 2015-03-06 線形ハイブリッドオートマタのCEGARを適用したSMTベースモデル検査(離散事象システム及び一般) 冨坂 征平, 柳瀬 龍, 櫻井 孝平, 山根 智, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | モデル検査では,システムの状態数に応じて計算資源を指数的に消費することで検証が停止しない状態爆発問題が発生する.E. M. Clarkeらは,システムの反例による抽象化精錬の枠組み(CEGAR)のモデル検査を提案した.これにより,モデル検査においてシステムの状態数を抑えながらの検証が可能となった.本研究では,組込みシステムをハイブリッドシステムと見なし,その仕様記述を線形ハイブリッドオートマトンにより仕様記述を行う.そして,線形ハイブリッドオートマトンに対して,CEGARの枠組みを適用しハイブリッドシステムの安全性検証を行う.また,近年注目を集めているSMT(Satisfiability Modulo Theories)ソルバを用いてCEGARの反例解析と精錬の導出を行うことで,効率的な検証を行う. |
| 抄録(英) | Model Checking is the technique to verify whether the system satisfies the safety property. The Reachability analysis is a powerful technique in the verification of the safety property. However in this method, we need a solution for the state explosion problem. For this problem, Counterexample-Guided Abstraction Refinement (CEGAR) is proposed to avoid the state explosion. In this paper, we propose the technique in order to verify the safety property by the reachability analysis for hybrid systems, and we apply the CEGAR framework, and verify them using the SMT (Satisfiability Modulo Theories)-Solver. |
| キーワード(和) | モデル検査 / 状態爆発 / ハイブリッドシステム / CEGAR / SMTソルバ |
| キーワード(英) | Model Checking / state explosion / hybrid system / CEGAR / SMT-Solver |
| 資料番号 | MSS2014-99 |
| 発行日 |
| 研究会情報 | |
| 研究会 | MSS |
|---|---|
| 開催期間 | 2015/2/26(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Mathematical Systems Science and its applications(MSS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 線形ハイブリッドオートマタのCEGARを適用したSMTベースモデル検査(離散事象システム及び一般) |
| サブタイトル（和） | |
| タイトル（英） | SMT-based Model Checking for Linear Hybrid Automata using CEGAR |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 状態爆発 / state explosion |
| キーワード(3)（和/英） | ハイブリッドシステム / hybrid system |
| キーワード(4)（和/英） | CEGAR / CEGAR |
| キーワード(5)（和/英） | SMTソルバ / SMT-Solver |
| 第 1 著者 氏名（和/英） | 冨坂 征平 / Shohei TOMISAKA |
| 第 1 著者 所属（和/英） | 金沢大学大学院自然科学研究科電子情報科学専攻 Kanazawa University Graduate School of Natural Science & Technology |
| 第 2 著者 氏名（和/英） | 柳瀬 龍 / Ryo YANASE |
| 第 2 著者 所属（和/英） | 金沢大学大学院自然科学研究科電子情報科学専攻 Kanazawa University Graduate School of Natural Science & Technology |
| 第 3 著者 氏名（和/英） | 櫻井 孝平 / Kohei SAKURAI |
| 第 3 著者 所属（和/英） | 金沢大学大学院自然科学研究科電子情報科学専攻 Kanazawa University Graduate School of Natural Science & Technology |
| 第 4 著者 氏名（和/英） | 山根 智 / Satoshi YAMANE |
| 第 4 著者 所属（和/英） | 金沢大学大学院自然科学研究科電子情報科学専攻 Kanazawa University Graduate School of Natural Science & Technology |
| 発表年月日 | 2015-03-06 |
| 資料番号 | MSS2014-99 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | 493 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |