TAPAAL Model Checker とは

TAPAALは、デンマークのAalborg大学でコンピュータサイエンス学科で開発されたTimed-Arcペトリネットのモデリング、シミュレーション、検証のツールであり、Linux、Windows、Mac OS Xプラットフォームで使用できます。
Timed-Arc Petri Net(TAPN)は、古典的なペトリネットモデル(1962年のCarl Adam Petriのディスカバリーで導入された分散計算の一般的なグラフィカルモデル)の時間拡張です。 TAPNで考慮される時間延長は、ネットのトークン(各トークンは独自の年齢を有する)に関連するリアルタイムの明示的な処理を可能にし、場所からトランジションへのアークは、そのトークンの年齢を制限する時間間隔それぞれの遷移を起動するために使用することができます。 TAPAALツールでは、トランスポートアーク(これは、以前に検討されていたリードアークよりも表現力が豊富である)およびインヒビターアークを備えた、年齢不変のこのモデルのさらなる拡張が実装されています。
TAPAALツールは、TAPNモデルを描画するためのグラフィカルなエディタ、設計されたネットを実験するためのシミュレータ、CTLロジックのサブセット(本質的にEF、EG、AF、AGの入れ子式なしの式)で論理クエリに自動的に答える検証環境を提供します。また、ユーザは、所与のネットが所定の数kに対してkバウンドであるかどうかをチェックすることもできる。 TAPAALには、TAPAAL(継続時間と離散時間の1つ)と一緒に配布される独自の検証エンジンが装備されています。オプションで、ユーザーは自動的にTAPAALモデルをUPPAALに変換し、UPPAAL検証エンジンに依存することができます。