階層型ペトリネット設計・検証ツール：HiPS

全文

(1)組込みシステムシンポジウム2016 Embedded Systems Symposium 2016. ESS2016 2016/10/20. 階層型ペトリネット設計・検証ツール：HiPS 三井雄太1. 張江洋次朗2. 和崎克己3. 概要：階層型のペトリネット設計エントリ機能と，動的・構造的性質の検証機能を有する HiPS (Hierarchical Petri net Simulator) ツールについて紹介する．本ツールは信州大学和崎研究室によって 2008 年から開発が進められて来た．P/T-net 向けの HiPS ver.1 と，Colored ネット向けの HiPS ver.2 がある．P/T-net 向けの検証機能としては，ランダムウォーク型シミュレーション，デッドロック状態検知器，安全性・公平性解析器，構造的解析器等が実装されている．モデル検査機能としては，状態空間生成器，LTL 仕様入力支援等が実装されている．キーワード：形式手法，ペトリネット，階層型設計，動的・構造的検証，モデル検査，状態空間生成. 1. はじめにペトリネット（Petri net）とは，離散事象システムの振る舞いをモデル化することができるツールであり，振る舞いや構造の解析を行うことでシステムの様々な性質を知ることができる [1]．HiPS では，ペトリネットを階層的に設計し，シミュレーションを行うことができる [2]．また，設計したネットを検証し性質を解析する機能を有する．ペトリネットの状態空間を生成し，全状態空間の網羅的な検査. 図 1 ペトリネット設計ツール HiPS. が可能である．実装は C++，C#によって行われた．. 2. 階層化ネットの設計機能. いトークンの数を入力する．サブページの作成時にはペト. メイン画面では，編集中のペトリネットの構造，選択中. リネット設計キャンバスはタブ形式になり，タブを選択す. の要素の属性，ペトリネットの編集画面，ログの４ペイン. ることによってそのページで設計したペトリネットが表示. の構成をとっている (図 1)．“New Net”，“New Page” で，. される．各サブページでは，要素にメインのペトリネット. 新規保存 XML ファイルの作成，または，新規ページの作. とつながる入出力ポートを指定する必要がある．. 成を行う．プレースボタン（トランジションボタン）を選. 3. ランダムウォークシミュレーション. 択状態で，編集画面上にてクリックすることによって，その場所にプレース（トランジション）が追加される．アー. HiPS は，設計したペトリネットでシミュレーションが. クボタンを押した状態で，編集画面上のプレースとトラン. 可能である．発火可能なトランジションが非決定的である. ジションを順に押すと，その要素同士がアークで繋がれ. とき，発火するトランジションは発火可能なトランジショ. る．トランジションとトランジション，またはプレースと. ンの中からランダムに選択される．シミュレーションは，. プレースはアークによって繋ぐことはできない．編集画面. トランジションの発火動作として発火するトランジション. 上でトークンを設定するプレースをクリックし，プレース. が赤くなり，またプレースに設置されているトークンの遷. のプロパティ設定画面から “InitialMarking”，に設置した. 移が行われる．GUI ページのシミュレーション再生ボタンにより，設計したペトリネットでのシミュレーションが. 1. 2. 3. 信州大学大学院総合理工学研究科 Graduate School of Science and Technology，Shinshu University. 信州大学大学院総合工学系研究科 Interdisciplinaty Graduate School of Science and Technology，Shinshu University. 信州大学工学部 Faculty of Engineering，Shinshu University.. ⓒ 2016 Information Processing Society of Japan. 可能である．一度シミュレーション再生ボタンを押すと，キャンバスがシミュレーションモードに切り替わる．途中で発火不可となってしまった場合は，それ以上シミュレーションをすることができない．シミュレーションを行った際，これまでに発火したトランジションの発火系列が保持される． 96.

(2) 組込みシステムシンポジウム2016 Embedded Systems Symposium 2016. ESS2016 2016/10/20. 4. ネット検証機能 4.1 動的性質可達性解析初期マーキングから可達な全てのマーキングと，マーキング間の遷移関係を列挙する．非有界なネットに対しては適用できない．被覆性解析初期マーキングから可達なマーキングと，マーキング間の遷移が列挙されて表示される．. 図 2. 解析画面の例. デッドロック解析フォームで指定した深さまでの可達解析を行い，デッドロックしているマーキングを見つける．デッドロッ. 5. 状態空間生成・モデル検査. クになっているマーキングが発見されると，そのマー. 5.1 状態空間生成. キングとそれに至るまでの発火系列を表示する．. k-有界性解析フォームで指定した深さまでの有界性を解析する．可逆性解析. ペトリネットにおける状態空間は有界な可達グラフとして与えられ，Labelled Transition System(LTS) として表現される．初期マーキングと接続行列の発火操作によって，有界な可達グラフ生成アルゴリズムが提案されている．. すべてのマーキングにおいて常に初期マーキングに戻. HiPS ツールの状態空間生成器は，シングルスレッドとマ. ることができるかを解析する．. ルチスレッドの二つのモードに対応している．また，メモ. 同期距離・公平性解析器同期距離の解析結果をセルに表示し，公平性の解析結. リの高効率化のために，Bloom Filter やダブルハッシュ構造・ツリー構造といったオプションに対応している．. 果をテキスと欄に表示する．解析対象のネットが B公平ネットである場合 “Bounded Fair Net”，無条件. 5.2 モデル検査. 公平ネットの場合は “Unconditional Fair Net” とテキ. モデル検査は全状態空間の網羅的な検査をする．仕様と. スト欄に表示される．また，同期距離の値をクリック. 合成した状態空間内に反例が一つでも検知された場合，そ. することによってペトリネットのトランジションの色. のシステムは仕様を満たしていないといえる．LTS はシ. を変更する．同期距離の値が有限の場合には黄緑色に. ステムで観察される事象の順序を記述するモデルであるた. 変更され，それ以外の場合には紫色に変更される．. め，事象に関する真偽を定めた (Fluent Linear Temporal. Logic)FLTL による仕様定義を行う．FLTL は事象の遷移 4.2 構造的性質. について流動を定義しなくてはならないが，ペトリネッ. T インバリアント・S インバリアント. トの単一のトランジションを変数として扱うことで，LTL. “Table” と “Text” のボタンで出力形式を選ぶことがで. と同様に記述できる．状態空間生成と検査を同時に行う. きる．各インバリアントは行ごとに表される．“view”. on-the-fly 法を導入し，実メモリ・実行速度に対する効率. ボタンを押すことによって，押した行のインバリアン. 化を図っている．. トをネットに反映することができる．T インバリアント，または S インバリアントが出現しないペトリネットで解析を行うと “No Transition.” と表示される．構造的解析器. 6. まとめ以上のように，HiPS はペトリネット解析におけるツールとして，P/T ネットの諸性質に基づいた検証機能や，モデ. 構造的有界，保存性，準保存性，反復性，準反復性，. ルの状態空間生成およびモデル検査器を提供する．今後は. 反復一致性，準反復一致性の７つの性質を解析するこ. 精緻な活性判定機能やモデル修正補助のための反例トレー. とができる．対象となるペトリネットは純粋でなけ. ス実行の導入を検討している．. ればならない．図 2 のように，性質を持っている場合，+が表示され，持っていない場合，-が表示される．. 参考文献. “Analyze counter example” をチェックした状態で解. [1]. 析することで構造的有界，保存性，反復一致性の反例を解析することができる．. ⓒ 2016 Information Processing Society of Japan. [2]. T.Murata：“Petri Nets: Properties， Analysis and Applications”，Proc. of the IEEE, 77(4), (1989) HiPS：信州大学和崎研究室， http://hips-tools.sourceforge.net/wiki/. 97.

(3)