| 講演名 | 2016-01-25 線形時相論理式からイベントベースオートマトンへの変換を利用したペトリネット検証ツールHiPS向けon-the-flyモデル検査器 張江 洋次朗(信州大), 和崎 克己(信州大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では，ペトリネットより生成される状態空間を対象に，線形時相論理式による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 |
| 資料番号 | MSS2015-46,SS2015-55 |
| 発行日 | 2016-01-18 (MSS, SS) |
| 研究会情報 | |
| 研究会 | SS / MSS |
|---|---|
| 開催期間 | 2016/1/25(から2日開催) |
| 開催地（和） | しいのき迎賓館 セミナールームB |
| 開催地（英） | Shiinoki-Geihin-Kan |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 結縁 祥治(名大) / 山根 智(金沢大) |
| 委員長氏名（英） | Shoji Yuen(Nagoya Univ.) / Satoshi Yamane(Kanazawa Univ.) |
| 副委員長氏名（和） | 緒方 和博(北陸先端大) / 名嘉村 盛和(琉球大) |
| 副委員長氏名（英） | Kazuhiro Ogata(JAIST) / Morikazu Nakamura(Univ. of Ryukyus) |
| 幹事氏名（和） | 小林 隆志(東工大) / 鷲崎 弘宜(早大) / 中田 充(山口大) / 豊嶋 伊知郎(東芝) |
| 幹事氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Hironobu Washizaki(Waseda Univ.) / Mitsuru Nakata(Yamaguchi Univ.) / Ichiro Toyoshima(Toshiba) |
| 幹事補佐氏名（和） | 肥後 芳樹(阪大) / 金城 秀樹(沖縄大) |
| 幹事補佐氏名（英） | Yoshiki Higo(Osaka Univ.) / Hideki Kinjo(Okinawa Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science / Technical Committee on Mathematical Systems Science and its applications |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 線形時相論理式からイベントベースオートマトンへの変換を利用したペトリネット検証ツール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 |
| 第 1 著者 氏名（和/英） | 張江 洋次朗 / Yojiro Harie |
| 第 1 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 第 2 著者 氏名（和/英） | 和崎 克己 / Katsumi Wasaki |
| 第 2 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 発表年月日 | 2016-01-25 |
| 資料番号 | MSS2015-46,SS2015-55 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | MSS-419,SS-420 |
| ページ範囲 | pp.63-68(MSS), pp.63-68(SS), |
| ページ数 | 6 |
| 発行日 | 2016-01-18 (MSS, SS) |