A-012
ペトリネット検証ツール HiPS における on-the-fly LTLモデル検査器の実装

◎張江洋次朗・和崎克己（信州大）

本稿では，ペトリネットより生成される状態空間を対象に，線形時相論理式によるon-the-flyモデル検査器の設計について記す．ペトリネット設計・検証ツールHiPSには，発火系列により構成される，ペトリネットの初期マーキングを根とする状態空間を生成する機能が備わっている．HiPSは外部ツールと連携することで，状態空間に対するモデル検査を行うことができる．モデル検査を適用するために全ての状態空間の生成を行わなくてはならず，物理的，時間的制約から大規模モデルへの適用は難しい．状態爆発に対するモデル検査の効率化にon-the-fly手法が挙げられる．on-the-fly手法は，状態空間構築と並列して検査を実行する手法である．モデル検査時にHiPSの機能である状態空間生成プロセスとIPCチャンネルによるプロセス間通信を行う．検査部と状態空間生成部を互いに独立して動作をさせることでon-the-fly検証を実現した．