| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-03-03 11:25 有界モデル検査を用いた複数UML図の形式的検証 ○宮崎 仁・横川智教・佐藤貞仁・佐藤洋一郎・早瀬道芳（岡山県立大）  SS2007-60 |
|
| 抄録 | （和） | 筆者らはこれまでに，システム開発における複数のUML図で記述された仕様を一つの状態機械としてモデル化し，モデル検査による検証を行う手法について検討を行ってきた．また，検証の対象となるシステムが大規模である場合に状態数が爆発的に増加する，いわゆる状態爆発問題に対し，有界モデル検査(Bounded Model Checking, BMC)を用いて状態爆発を避ける手法についても検討してきた．有界モデル検査はシステムの探索する状態をある有限のステップ数に限定することで，大規模なシステムの検証を可能とする．しかしながら，有界モデル検査を用いたとしても状態爆発が避けられない問題も存在する． そこで本論文では，状態の探索手法であるForward SearchとBackward Searchの二つを用いた検証をそれぞれ比較し，より有効な探索手法についての検討を行うことで，有界モデル検査の効率化を目指す． 比較実験として，UMLの状態遷移図とシーケンス図を用いて記述されたソフトウェアの仕様を対象として，Forward SearchとBackward Searchのそれぞれを用いて有界モデル検査を行った．また，従来の非有界モデル検査(Unbounded Model Checking, UBMC)による検証との比較についても示した． |
| （英） | In previous work, we have proposed a framework for verifying system designs by multiple UML diagrams using symbolic model checking. We have aimed to avoid state explosion problem by application of bounded modek checking which searches for a counterexample up to a fixed number of transitions. However, there are some problems which cannot be solved using bounded model checking. In this paper, we compare results of bounded model checking using two methods for searching state space, forward search and backward search, and study for effectiveness of them. We conducted comparative experiments between forward search and backward search in the case of verification of software specification described by UML statechart diagrams and a sequence diagram. We also compared the results of bounded model checking with the ones of unbounded model checking. |
|
| キーワード | （和） | 形式的検証 / UML / 有界モデル検査 / / / / / |
| （英） | Formal Verification / UML / Bounded Model Checking / / / / / | |
| 文献情報 | 信学技報, vol. 107, no. 505, SS2007-60, pp. 19-24, 2008年3月. | |
| 資料番号 | SS2007-60 | |
| 発行日 | 2008-02-25 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2007-60 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2008-03-03 - 2008-03-04 |
| 開催地（和） | 長崎大学 |
| 開催地（英） | Nagasaki Univ. |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2008-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 有界モデル検査を用いた複数UML図の形式的検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal verification of multiple UML diagrams using bounded model checking |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 形式的検証 / Formal Verification |
| キーワード(2)（和/英） | UML / UML |
| キーワード(3)（和/英） | 有界モデル検査 / Bounded Model Checking |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 宮崎 仁 / Hisashi Miyazaki / ミヤザキ ヒサシ |
| 第1著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Prefectural Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 横川 智教 / Tomoyuki Yokogawa / ヨコガワ トモユキ |
| 第2著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Prefectural Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 佐藤 貞仁 / Sadahito Sato / サトウ サダヒト |
| 第3著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Prefectural Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 佐藤 洋一郎 / Yoichiro Sato / サトウ ヨウイチロウ |
| 第4著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Prefectural Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 早瀬 道芳 / Michiyoshi Hayase / ハヤセ ミチヨシ |
| 第5著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Prefectural Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-03-03 11:25:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2007-60 |
| 巻番号（vol） | vol.107 |
| 号番号（no） | no.505 |
| ページ範囲 | pp.19-24 |
| ページ数 | 6 |
| 発行日 | 2008-02-25 (SS) |
[研究会発表申込システムのトップページに戻る]