| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2010-08-04 18:00 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価 ○川端聡基・小林史佳・上田和紀（早大）  DC2010-16 |
|
| 抄録 | （和） | モデル検査は状態空間の網羅的探索に基づく自動検証手法であり，その一つであるLTL モデル検査はオートマトンの受理サイクル探索問題に帰結される．モデル検査は対象となる状態空間が組み合わせ爆発を起こしやすく，その対策として並列化手法が考えられている．多数の並列アルゴリズムが提案されており，その一つであるOWCTYreversed はバグがないモデルに対して高速に動作すると分かっている． 本研究では，探索を行うオートマトンがシステムオートマトンと性質オートマトンの同期積により生成されることと，性質オートマトンが非常に小さく強連結成分の解析が容易なことに注目した．受理状態を含まない強連結成分より生成された状態は受理サイクルを作らないと判断できるので，それらを削除する並列アルゴリズムSCC-OWCTY を設計し，性能評価を行った． |
| （英） | Model checking is an automated verification method based on exhaustivesearch.LTL model checking is reduced to the search of acceptance cyclesin B¨uchi automata.Model checking is prone to state space explosion, and we expectthat parallel processing would be a promising approach.One of the parallel algorithms, OWCTY reversed, is known to be fastfor models without bugs, but it does not use the characteristics ofthe automata used in LTL model checking. We propose a new algorithm named SCC-OWCTY that exploits the stronglyconnected components of property automata and removes those statesjudged not to form acceptance cycles from the synchronous products ofsystem and property automata.The proposed algorithm was evaluated using DiVinE. |
|
| キーワード | （和） | モデル検査 / 並列処理 / OWCTY / DiVinE / / / / |
| （英） | modelchecking / parallelization / OWCTY / DivinE / / / / | |
| 文献情報 | 信学技報, vol. 110, no. 168, DC2010-16, pp. 13-18, 2010年8月. | |
| 資料番号 | DC2010-16 | |
| 発行日 | 2010-07-28 (DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | DC2010-16 |
|
| 研究会情報 | |
| 研究会 | CPSY DC |
| 開催期間 | 2010-08-03 - 2010-08-05 |
| 開催地（和） | 金沢市文化ホール |
| 開催地（英） | Kanazawa Cultural Hall |
| テーマ（和） | 2010年並列／分散／協調処理に関する 『金沢』サマー・ワークショップ |
| テーマ（英） | Summer United Workshops on Parallel, Distributed and Cooperative Processing |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2010-08-CPSY-DC |
| 本文の言語 | 日本語 |
| タイトル（和） | 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価 |
| サブタイトル（和） | |
| タイトル（英） | Design and Performance Evaluation of the Parallel Model Checking Algorithm SCC-OWCTY using Strongly Connected Components |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / modelchecking |
| キーワード(2)（和/英） | 並列処理 / parallelization |
| キーワード(3)（和/英） | OWCTY / OWCTY |
| キーワード(4)（和/英） | DiVinE / DivinE |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 川端 聡基 / Toshiki Kawabata / カワバタ トシキ |
| 第1著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 小林 史佳 / Fumiyoshi Kobayashi / コバヤシ フミヨシ |
| 第2著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 上田 和紀 / Kazunori Ueda / ウエダ カズノリ |
| 第3著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2010-08-04 18:00:00 |
| 発表時間 | 30分 |
| 申込先研究会 | DC |
| 資料番号 | DC2010-16 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | no.168 |
| ページ範囲 | pp.13-18 |
| ページ数 | 6 |
| 発行日 | 2010-07-28 (DC) |
[研究会発表申込システムのトップページに戻る]