| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2014-07-29 15:40 Hash Compaction を利用したグラフ書換え系モデル検査の大規模化とその評価 ○吉田健人・小沼 賢・上田和紀（早大）  DC2014-19 |
|
| 抄録 | （和） | グラフ書換え系モデル検査とはグラフ書換え系をモデリング言語として, そのモデルが取りうる全ての状態を網羅的に探索することで, 要求された性質を満たすか否かを判定する検証手法である. グラフ書換え系はモ デルのもつ情報構造の表現力が高い. このことがモデル検査における状態数削減の効果をもたらすこともある. しかし, その半面時間・空間的に効率が悪いという欠点がある. 本稿では, グラフ書換え系モデル検査において Hash Compaction を利用した空間・時間的改善手法を LMNtal 並列モデル検査器 SLIM に実装し, 計測を行った. また Hash Compaction は完全な状態空間の再現を保証しないので, ハッシュ関数の精度が状態空間に与える影響の考察と評価を行った. |
| （英） | Graph rewriting model checking is a verification method that determines whether a model described in a graph rewriting system satisfies required properties by exploring all reachable states. Graph rewriting has a high expressive power in representing information structures of models. This often results in the reduction of the number of states in model checking. On the other hand, graphs are heavyweight data structures in terms of both space and time. In this study, we implemented a Hash Compaction method to improve space and time efficiency of the LMNtal parallel model checker SLIM and measured its performance. Since Hash Compaction does not guarantee the reproduction of complete state space, we also studied and evaluated the effect of the accuracy of the hash function on the state space. | |
| キーワード | （和） | モデル検査 / Hash Compaction / グラフ書換え系 / / / / / |
| （英） | Model Checking / Hash Compaction / Graph Rewriting / / / / / | |
| 文献情報 | 信学技報, vol. 114, no. 156, DC2014-19, pp. 9-16, 2014年7月. | |
| 資料番号 | DC2014-19 | |
| 発行日 | 2014-07-22 (DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | DC2014-19 |
|
| 研究会情報 | |
| 研究会 | CPSY DC |
| 開催期間 | 2014-07-28 - 2014-07-30 |
| 開催地（和） | 朱鷺メッセ 新潟コンベンションセンター |
| 開催地（英） | Toki Messe, Niigata |
| テーマ（和） | 並列／分散／協調とディペンダブルコンピューティングおよび一般 |
| テーマ（英） | Parallel, Distributed and Cooperative Processing |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2014-07-CPSY-DC |
| 本文の言語 | 日本語 |
| タイトル（和） | Hash Compaction を利用したグラフ書換え系モデル検査の大規模化とその評価 |
| サブタイトル（和） | |
| タイトル（英） | Evaluation of Large-scale Graph Rewriting Model Checking Using Hash Compaction |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | Hash Compaction / Hash Compaction |
| キーワード(3)（和/英） | グラフ書換え系 / Graph Rewriting |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 吉田 健人 / Taketo Yoshida / ヨシダ タケト |
| 第1著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 小沼 賢 / Masaru Onuma / オヌマ マサル |
| 第2著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 上田 和紀 / Kazunori Ueda / ウエダ カズノリ |
| 第3著者 所属（和/英） | 早稲田大学 (略称： 早大) Waseda University (略称： Waseda Univ.) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2014-07-29 15:40:00 |
| 発表時間 | 25分 |
| 申込先研究会 | DC |
| 資料番号 | DC2014-19 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | no.156 |
| ページ範囲 | pp.9-16 |
| ページ数 | 8 |
| 発行日 | 2014-07-22 (DC) |
[研究会発表申込システムのトップページに戻る]