| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2012-01-26 11:45 SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察 ○新村勇人・宮本俊幸（阪大）  MSS2011-58 SS2011-43 |
|
| 抄録 | （和） | 近年，記号モデル検査\cite{SMC}の有効な手法として命題論理式の充足可能性問題 (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 / / / | |
| 文献情報 | 信学技報, vol. 111, no. 405, MSS2011-58, pp. 21-26, 2012年1月. | |
| 資料番号 | MSS2011-58 | |
| 発行日 | 2012-01-19 (MSS, SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2011-58 SS2011-43 |
|
| 研究会情報 | |
| 研究会 | SS MSS |
| 開催期間 | 2012-01-26 - 2012-01-27 |
| 開催地（和） | 高知市文化プラザかるぽーと |
| 開催地（英） | Kochi City Culture-Plaza Cul-Port |
| テーマ（和） | 一般 |
| テーマ（英） | General topics |
| 講演論文情報の詳細 | |
| 申込み研究会 | MSS |
| 会議コード | 2012-01-SS-MSS |
| 本文の言語 | 日本語 |
| タイトル（和） | 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 |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 新村 勇人 / Hayato Niimura / ニイムラ ハヤト |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 宮本 俊幸 / Toshiyuki Miyamoto / ミヤモト トシユキ |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2012-01-26 11:45:00 |
| 発表時間 | 30分 |
| 申込先研究会 | MSS |
| 資料番号 | MSS2011-58, SS2011-43 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | no.405(MSS), no.406(SS) |
| ページ範囲 | pp.21-26 |
| ページ数 | 6 |
| 発行日 | 2012-01-19 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]