TAPAALは、デンマークのオールボー大学コンピュータサイエンス学部で開発された、Timed-Arc Petri netのモデリング、シミュレーション、検証のためのツールであり、Linux、Windows、Mac OS Xプラットフォームで利用可能です。[ 1 ]
タイムドアークペトリネット（TAPN）は、古典的なペトリネットモデル（1962年にカール・アダム・ペトリが博士論文で発表した、分散計算の一般的なグラフィカルモデル）の時間拡張です。TAPNで考慮される時間拡張により、ネット内のトークンに関連付けられたリアルタイムを明示的に扱うことができます（各トークンには独自の経過時間があります）。また、場所から遷移へのアークには、それぞれの遷移を発火するために使用できるトークンの経過時間を制限する時間間隔がラベル付けされます。TAPAALツールでは、このモデルのさらなる拡張として、輸送アーク（例えば、以前に考慮された読み取りアークよりも表現力が高い）と阻害アークを備えた経過時間不変量が実装されています。
TAPAALツールは、TAPNモデルを描画するためのグラフィカルエディタ、設計したネットを実験するためのシミュレータ、およびCTLロジックのサブセット（基本的にネストなしのEF、EG、AF、AG式）で定式化された論理クエリに自動的に応答する検証環境を提供します。また、指定されたネットが指定された数値kに対してk-boundedであるかどうかをユーザーが確認することもできます。TAPAALには、TAPAALとともに配布される独自の検証エンジン（連続時間用[ 2 ] と離散時間用[ 3 ]）が付属しています。オプションで、ユーザーはTAPAALモデルをUPPAALに自動的に変換し、 UPPAAL検証エンジンを利用することもできます。
TAPAAL 2.2.1 スクリーンショット外部リンク
- TAPAALウェブサイト、ダウンロード
- デンマーク、オールボー大学コンピュータサイエンス学部DESユニット
- TAPAAL: 時限アーク ペトリ ネットの編集者、シミュレーター、検証者、J. Byg、KY Jørgensen、J. Srba、ATVA'09、Springer
- J. Byg、KY Jørgensen、J. Srba著「時間付きアークペトリネットの時間付きオートマタネットワークへの効率的な変換」、ICFEM'09、Springer
- 時間付き遷移システムを関連付け、TCTLモデル検査を維持するためのフレームワーク（L. Jacobsen、M. Jacobsen、MH Møller、J. Srba著、EPEW'10、Springer）
- タイムアーク ペトリ ネットの検証 (L. Jacobsen、M. Jacobsen、MH Møller、J. Srba、SOFSEM'11、Springer)
参考文献
- ↑アレクサンドル・デイヴィッド;ラッセ・ジェイコブセン。モーテン・ヤコブセン。ケネス・ヤーケ・ヨルゲンセン。ミカエル・H・モラー；イジー・スルバ (2012)。 「TAPAAL 2.0: タイムアーク ペトリ ネット用の統合開発環境」。システムの構築と分析のためのツールとアルゴリズム。 LNCS。 Vol. 7214. pp. 492–497 . doi : 10.1007/978-3-642-28756-5_36。ISBN 978-3-642-28755-8。
- ↑ Alexandre David; Lasse Jacobsen; Morten Jacobsen; Jiří Srba (2012). "A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets". Electronic Proceedings in Theoretical Computer Science . 102 : 141–155 . arXiv : 1211.6194 . doi : 10.4204/EPTCS.102.12 . S2CID 15499812 .
- ↑ M. Andersen、H.G. Larsen、J. Srba、M.G. Sørensen、J.H. Taankvist (2012). "閉じた時間付きアークペトリネットの活性特性の検証". Mathematical and Engineering Methods in Computer Science . LNCS. Vol. 7721. pp. 69–81 . doi : 10.1007/978-3-642-36046-6_8 . ISBN 978-3-642-36044-2。
