| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2016-01-25 15:45 線形時相論理式からイベントベースオートマトンへの変換を利用したペトリネット検証ツールHiPS向けon-the-flyモデル検査器 ○張江洋次朗・和崎克己（信州大）  MSS2015-46 SS2015-55 |
|
| 抄録 | （和） | 本稿では，ペトリネットより生成される状態空間を対象に，線形時相論理式によるon-the-flyモデル検査器の設計について記す．筆者らの研究グループによって開発・公開されているペトリネット設計・検証ツールHiPSがある．HiPSには，発火系列により構成される，ペトリネットの初期マーキングを根とする状態空間を生成する機能が備わっている．HiPSは外部ツールと連携することで，状態空間に対するモデル検査を行うことができる．現状ではモデル検査を適用するためには全ての状態空間の生成を行わなくてはならず，物理的，時間的制約から大規模モデルへの適用は難しい．そうした状態爆発に対するモデル検査の効率化として，on-the-fly手法が挙げられる．on-the-fly手法とは，状態空間構築と並列して検査を実行する手法である．モデル検査時にHiPSの機能である状態空間生成プロセスとのIPCチャンネルを用いたプロセス間通信を行う．検査部と状態空間生成部を互いに独立して動作をさせることでon-the-fly検証を実現した． |
| （英） | This paper proposes an On-the-fly Linear Temporal Logic (LTL) model checker using state space generation based on the Petri net models. The `HiPS' tool developed by our research group at Shinshu University, is a design and verification environment for Place-Transition net. This tool features the functions to generate the state space and process trace graph which has a root and the edges as the initial marking and the firing sequences of Petri net respectively. HiPS tool can perform the exhaustive model checking for the state space by combining with external tools. However, since the order at present to apply the model checking is required for generating all of the state space, there are difficult issues to apply the large model from the physical and time constraint. Simultaneously, there is the on-the-fly model checking technique as the efficiency to against for the state explosion problem. The on-the-fly method then performs to test the events in parallel with the state space construction. In this study, we propose the parallel execution by performing the inter-process communication using the state space generation process and IPC channels on HiPS tool. This implement realizes a high-efficiency on-the-fly verification that executes independently of the verification process and the state space generation process. | |
| キーワード | （和） | ペトリネット / モデル検査 / on-the-fly / 線形時相論理 / イベントベース検査 / / / |
| （英） | Petri net / Model check / on-the-fly / Linear Temporal Logic / Event based checking / / / | |
| 文献情報 | 信学技報, vol. 115, no. 419, MSS2015-46, pp. 63-68, 2016年1月. | |
| 資料番号 | MSS2015-46 | |
| 発行日 | 2016-01-18 (MSS, SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2015-46 SS2015-55 |
|
| 研究会情報 | |
| 研究会 | SS MSS |
| 開催期間 | 2016-01-25 - 2016-01-26 |
| 開催地（和） | しいのき迎賓館 セミナールームB |
| 開催地（英） | Shiinoki-Geihin-Kan |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | MSS |
| 会議コード | 2016-01-SS-MSS |
| 本文の言語 | 日本語 |
| タイトル（和） | 線形時相論理式からイベントベースオートマトンへの変換を利用したペトリネット検証ツールHiPS向けon-the-flyモデル検査器 |
| サブタイトル（和） | |
| タイトル（英） | On-the-fly Model Checker for a Petri Net Verification Tool(HiPS) by using Replacement LTL Formula to Event-Based Automaton |
| サブタイトル（英） | |
| キーワード(1)（和/英） | ペトリネット / Petri net |
| キーワード(2)（和/英） | モデル検査 / Model check |
| キーワード(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.) |
| 講演者 | 第1著者 |
| 発表日時 | 2016-01-25 15:45:00 |
| 発表時間 | 25分 |
| 申込先研究会 | MSS |
| 資料番号 | MSS2015-46, SS2015-55 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | no.419(MSS), no.420(SS) |
| ページ範囲 | pp.63-68 |
| ページ数 | 6 |
| 発行日 | 2016-01-18 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]