| 講演名 | 2012-01-26 SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察 新村 勇人, 宮本 俊幸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 近年,記号モデル検査の有効な手法として命題論理式の充足可能性問題(satisfiability,SAT)を利用する有界モデル検査が注目を集めている.データを含む分散システムの有界モデル検査手法において,SATソルバーではなくSMTソルバー(SAT modulo theories)を用いるとより効率的であることが知られている.また,我々はSOAに基づくシステムを設計・検証するためのUMLサブセットとして,cbUMLを提案した.よって本論文では,cbUMLにおける状態機械のSMTソルバーを用いる有界モデル検査手法を考察する. |
| 抄録(英) | Recently, SAT-based bounded model checking has received attention as an efficient symbolic model checking technique. It is known that for model checking of distributed systems with data SMT solvers is more effective than SAT solvers. We have proposed cbUML as a subset of UML to design and verify systems based on SOA. In this paper, we study a bounded model checking technique using SMT solvers to verify state machines of cbUML. |
| キーワード(和) | SOA / UML / 状態機械図 / 同期・非同期 / 有界モデル検査 |
| キーワード(英) | SOA / UML / state machine diagram / synchronous and asynchronous / bounded model checking |
| 資料番号 | MSS2011-58,SS2011-43 |
| 発行日 |
| 研究会情報 | |
| 研究会 | MSS |
|---|---|
| 開催期間 | 2012/1/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Mathematical Systems Science and its applications(MSS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察 |
| サブタイトル（和） | |
| タイトル（英） | A Study for Bounded Model Checking of UML State Machines Using SMT Solvers |
| サブタイトル（和） | |
| キーワード(1)（和/英） | SOA / SOA |
| キーワード(2)（和/英） | UML / UML |
| キーワード(3)（和/英） | 状態機械図 / state machine diagram |
| キーワード(4)（和/英） | 同期・非同期 / synchronous and asynchronous |
| キーワード(5)（和/英） | 有界モデル検査 / bounded model checking |
| 第 1 著者 氏名（和/英） | 新村 勇人 / Hayato NIIMURA |
| 第 1 著者 所属（和/英） | 大阪大学大学院工学研究科 Graduate School of Engineering, Osaka University |
| 第 2 著者 氏名（和/英） | 宮本 俊幸 / Toshiyuki MIYAMOTO |
| 第 2 著者 所属（和/英） | 大阪大学大学院工学研究科 Graduate School of Engineering, Osaka University |
| 発表年月日 | 2012-01-26 |
| 資料番号 | MSS2011-58,SS2011-43 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | 405 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |