お知らせ 2023年度・2024年度 学生員 会費割引キャンペーン実施中です
お知らせ 技術研究報告と和文論文誌Cの同時投稿施策(掲載料1割引き)について
お知らせ 電子情報通信学会における研究会開催について
お知らせ NEW 参加費の返金について
電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
[ログイン]
技報アーカイブ
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2015-03-05 14:30
モジュラ化手法によるモデル検査の検討とモジュラ検証の実用化
宮島卓巳茨城大)・小飼 敬茨城高専)・上田賀一茨城大)・山形知行武澤隆之日立KBSE2014-56
抄録 (和) 検査対象を機械的かつ網羅的に探索するモデル検査は,探索範囲の指数的増加のため適用が困難である.そこで,検査対象を構造と振舞いの観点から結合度の低い箇所を分割することでモジュラ化を行い,別々に検証し,1回に探索する範囲を制限することでモデル検査の実用化を目指す.本研究では,列車運行システムにおいてモジュラ化の有無による実験結果を比較し,有効性を評価する. 
(英) Model checking to search mechanically and cyclopedically for inspection system is difficult because of exponential increase of the search area. Therefore, we divide target model to modules from the view-point of the structure and behavior. And we aim at practical use of the model checking by verifying a module separately. This study shows the comparison of modular method and non-modula by using a train operation system as the subject of evaluation experiment.
キーワード (和) モデル検査 / SPIN / 状態爆発 / モジュラ検証 / / / /  
(英) model checking / SPIN / state explosion / modular verification / / / /  
文献情報 信学技報, vol. 114, no. 501, KBSE2014-56, pp. 25-30, 2015年3月.
資料番号 KBSE2014-56 
発行日 2015-02-26 (KBSE) 
ISSN Print edition: ISSN 0913-5685    Online edition: ISSN 2432-6380
著作権に
ついて
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034)
PDFダウンロード KBSE2014-56

研究会情報
研究会 KBSE  
開催期間 2015-03-05 - 2015-03-06 
開催地(和) 電通大(調布, 東3号館) 
開催地(英) The University of Electro-Communications 
テーマ(和) 一般 
テーマ(英) Genaral session 
講演論文情報の詳細
申込み研究会 KBSE 
会議コード 2015-03-KBSE 
本文の言語 日本語 
タイトル(和) モジュラ化手法によるモデル検査の検討とモジュラ検証の実用化 
サブタイトル(和)  
タイトル(英) Investigation of model checking by modular approach, and practicality of modular verification 
サブタイトル(英)  
キーワード(1)(和/英) モデル検査 / model checking  
キーワード(2)(和/英) SPIN / SPIN  
キーワード(3)(和/英) 状態爆発 / state explosion  
キーワード(4)(和/英) モジュラ検証 / modular verification  
キーワード(5)(和/英) /  
キーワード(6)(和/英) /  
キーワード(7)(和/英) /  
キーワード(8)(和/英) /  
第1著者 氏名(和/英/ヨミ) 宮島 卓巳 / Takumi Miyajima / ミヤジマ タクミ
第1著者 所属(和/英) 茨城大学 (略称: 茨城大)
Ibaraki University (略称: Ibaraki Univ.)
第2著者 氏名(和/英/ヨミ) 小飼 敬 / Kei Kogai / コガイ ケイ
第2著者 所属(和/英) 茨城工業高等専門学校 (略称: 茨城高専)
Ibaraki National College of Technology (略称: INCT)
第3著者 氏名(和/英/ヨミ) 上田 賀一 / Yoshikazu Ueda / ウエダ ヨシカズ
第3著者 所属(和/英) 茨城大学 (略称: 茨城大)
Ibaraki University (略称: Ibaraki Univ.)
第4著者 氏名(和/英/ヨミ) 山形 知行 / Tomoyuki Yamagata / ヤマガタ トモユキ
第4著者 所属(和/英) 株式会社日立製作所 (略称: 日立)
Hitachi, Ltd. (略称: Hitachi)
第5著者 氏名(和/英/ヨミ) 武澤 隆之 / Takayuki Takezawa /
第5著者 所属(和/英) 株式会社日立製作所 (略称: 日立)
Hitachi, Ltd. (略称: Hitachi)
第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著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者 第1著者 
発表日時 2015-03-05 14:30:00 
発表時間 45分 
申込先研究会 KBSE 
資料番号 KBSE2014-56 
巻番号(vol) vol.114 
号番号(no) no.501 
ページ範囲 pp.25-30 
ページ数
発行日 2015-02-26 (KBSE) 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会