電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
技報オンライン
‥‥ (ESS/通ソ/エレソ/ISS)
技報アーカイブ
‥‥ (エレソ/通ソ)
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2016-11-24 13:25
ペトリネット検証ツールHiPS向けon-the-flyモデル検査器の実現と評価
張江洋次朗和﨑克己信州大
技報オンラインサービス実施中
抄録 (和) ペトリネットモデルより生成される状態空間のイベントに着目したon-the-flyモデル検査器の設計を行った.HiPSは筆者らの研究グループによって開発・公開されているペトリネット設計検証ツールである.HiPSには,発火系列により構成される状態空間の生成器が実装されている.ペトリネットの状態空間は発火トランジションにより遷移が決定するため,イベントの生起に着目したモデル検査を行う.大規模モデルや複雑な振る舞いをするモデルについては状態爆発という問題が生じる.状態爆発に対するモデル検査の効率化として有効なon-the-fly検証を導入した.ABPプロトコルモデルなどの複数モデルを対象に検証を行い,モデル検証器の性能評価を行った. 
(英) This paper proposes an On-the-fly Fluent Linear Temporal Logic (FLTL) model checker using state space generation based on the Petri net models.
The hierarchical Petri net simulator (HiPS) tool is a design and verification environment for Place/Transition nets that can perform model checking for a state space.
However, exhaustive model checking, which can be computationally excessive, is required to generate the complete state space.
on-the-fly model checking reduces memory space and execution time by parallelizing state space generation and sequence searching.
We introduce a on-the-fly model checker for HiPS tool and then verify the liveness properties of model for ABP model.
キーワード (和) ペトリネット / モデル検査 / on-the-fly / 線形時相論理 / イベントベース検査 / / /  
(英) Petri net / Model checking / on-the-fly / Linear temporal logic / Event based checking / / /  
文献情報 信学技報, vol. 116, no. 316, MSS2016-43, pp. 31-35, 2016年11月.
資料番号 MSS2016-43 
発行日 2016-11-17 (CAS, MSS) 
ISSN Print edition: ISSN 0913-5685  Online edition: ISSN 2432-6380

研究会情報
研究会 MSS CAS IPSJ-AL  
開催期間 2016-11-24 - 2016-11-25 
開催地(和) 神戸情報大学院大学 
開催地(英) Kobe Institute of Computing 
テーマ(和) グラフ、ペトリネット、ニューラルネット及び一般 
テーマ(英)  
講演論文情報の詳細
申込み研究会 MSS 
会議コード 2016-11-MSS-CAS-AL 
本文の言語 日本語 
タイトル(和) ペトリネット検証ツールHiPS向けon-the-flyモデル検査器の実現と評価 
サブタイトル(和)  
タイトル(英) Development and evaluation of on-the-fly model checking for a Petri net verification tool (HiPS) 
サブタイトル(英)  
キーワード(1)(和/英) ペトリネット / Petri net  
キーワード(2)(和/英) モデル検査 / Model checking  
キーワード(3)(和/英) on-the-fly / on-the-fly  
キーワード(4)(和/英) 線形時相論理 / Linear temporal logic  
キーワード(5)(和/英) イベントベース検査 / Event based checking  
キーワード(6)(和/英) /  
キーワード(7)(和/英) /  
キーワード(8)(和/英) /  
第1著者 氏名(和/英/ヨミ) 張江 洋次朗 / Yojiro Harie / ハリエ ヨウジロウ
第1著者 所属(和/英) 信州大学 (略称: 信州大)
Shinshu University (略称: Shinshu Univ.)
第2著者 氏名(和/英/ヨミ) 和﨑 克己 / Katsumi Wasaki /
第2著者 所属(和/英) 信州大学 (略称: 信州大)
Shinshu University (略称: Shinshu 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著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者
発表日時 2016-11-24 13:25:00 
発表時間 25 
申込先研究会 MSS 
資料番号 IEICE-CAS2016-63,IEICE-MSS2016-43 
巻番号(vol) IEICE-116 
号番号(no) no.315(CAS), no.316(MSS) 
ページ範囲 pp.31-35 
ページ数 IEICE-5 
発行日 IEICE-CAS-2016-11-17,IEICE-MSS-2016-11-17 


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

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


IEICE / 電子情報通信学会