講演抄録/キーワード |
講演名 |
2016-11-24 13:25
ペトリネット検証ツールHiPS向けon-the-flyモデル検査器の実現と評価 ○張江洋次朗・和﨑克己(信州大) CAS2016-63 MSS2016-43 |
抄録 |
(和) |
ペトリネットモデルより生成される状態空間のイベントに着目した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 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
CAS2016-63 MSS2016-43 |