| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2010-08-04 18:30 LMNtalモデル検査器における状態爆発対策 ○後町将人・上田和紀（早大）  DC2010-17 |
|
| 抄録 | （和） | システム検証技術として注目を集めるモデル検査は, 必要なメモリと時間が爆発的に増加(状態爆発)する問題を抱えており, 大規模な検証問題を解くためには状態爆発対策の導入が必要不可欠である. LMNtalモデル検査器では, 状態をバイト列へ圧縮して管理する機能を新たに導入したことで検証可能な問題の規模が拡大し, 検証の長時間化への対策が求められていた. 本論文では, LMNtalモデル検査器がこれまで扱うことが困難であった大規模な検証問題を高速に解くために開発中の共有メモリ環境下における並列処理機能の実装と, 性能評価を示す. |
| （英） | Model checking is an important technique for system verification based on exhaustive search, but large-scale model checking must address the inherent problem of state-space explosion both in terms of time and memory usage. The LMNtal model checker, based on the hierarchical graph rewriting model, has recently been improved by introducing state compression using binary strings. This enabled us to verify larger problems, which made it apparent that the verification must be speeded up by parallel processing. In this paper, we show the implementation techniques of our parallel LMNtal model checker for shared-memory multiprocessors, and evaluates its performance. | |
| キーワード | （和） | LMNtal / モデル検査 / 状態爆発 / 状態圧縮 / 共有メモリ並列化 / / / |
| （英） | LMNtal / explicit state model checking / state space explosion / state compression / parallelization / / / | |
| 文献情報 | 信学技報, vol. 110, no. 168, DC2010-17, pp. 19-24, 2010年8月. | |
| 資料番号 | DC2010-17 | |
| 発行日 | 2010-07-28 (DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | DC2010-17 |
|
| 研究会情報 | |
| 研究会 | 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 |
| 本文の言語 | 日本語 |
| タイトル（和） | LMNtalモデル検査器における状態爆発対策 |
| サブタイトル（和） | |
| タイトル（英） | An approach to state space explosion in the LMNtal model checker |
| サブタイトル（英） | |
| キーワード(1)（和/英） | LMNtal / LMNtal |
| キーワード(2)（和/英） | モデル検査 / explicit state model checking |
| キーワード(3)（和/英） | 状態爆発 / state space explosion |
| キーワード(4)（和/英） | 状態圧縮 / state compression |
| キーワード(5)（和/英） | 共有メモリ並列化 / parallelization |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 後町 将人 / Masato Gocho / ゴチョウ マサト |
| 第1著者 所属（和/英） | 早稲田大学大学院情報理工学専攻 (略称： 早大) Dept. of Computer Science and Engineering, Waseda University (略称： Waseda Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 上田 和紀 / Kazunori Ueda / ウエダ カズノリ |
| 第2著者 所属（和/英） | 早稲田大学大学院情報理工学専攻 (略称： 早大) Dept. of Computer Science and Engineering, Waseda University (略称： Waseda Univ.) |
| 第3著者 氏名（和/英/ヨミ） | / / |
| 第3著者 所属（和/英） | (略称： ) (略称： ) |
| 第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著者 |
| 発表日時 | 2010-08-04 18:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | DC |
| 資料番号 | DC2010-17 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | no.168 |
| ページ範囲 | pp.19-24 |
| ページ数 | 6 |
| 発行日 | 2010-07-28 (DC) |
[研究会発表申込システムのトップページに戻る]