TAPAs model checker とは

TAPASは、並行システムを特定および分析するためのツールであり、その目的はプロセス代数の教授をサポートすることです。システムはプロセス代数項として記述され、ラベル付き遷移システム(LTS)にマッピングされます。特性は、具体的なシステム記述と抽象的なシステム記述の間の等価性を検査することによって、または得られたLTS上の時間的な式(μ-計算法またはACTLとして表される)をモデル検査することによって検証することができる。特に教えることに適したTAPAsの重要な特徴は、グラフィカルでもテキストでも、各システムの一貫した二重表現を維持することです。図表表記が変更された後、直ちにテキスト表記が更新されますが、テキスト表記の変更が懸念される場合は、更新を強制する必要があります。
TAPAsでは、並行システムは、システム動作の非決定論的記述であるプロセスと、プロセス構成によって得られるプロセスシステムとによって記述される。特に、プロセスは、他のプロセスまたはプロセスシステムの観点から定義することができる。プロセスとプロセスシステムは、与えられたプロセス代数の演算子を使用して構成されます。現在、TAPAsでは、2つのプロセス代数:CCSPとPEPAとみなされます。
CCSP(= CCS + CSP)は、CSPの一部の演算子を考慮してCCSから得られます。実際には、CCSPプロセスシステムを作成した後、ユーザーは以下を使用して分析することができます。
 等価性チェッカー:等価性の多くの定義に関する自動化ペアを比較することができます(バイシミュレーション、分岐二乗、装飾トレース)モデルチェッカー:システムのモデルを与えられ、このモデルが指定された仕様を満たしているかどうかを自動的にテストします。シミュレータ:システムを介した1つの可能な実行パスに従い、その結果の実行トレースをユーザに提示する。
PEPA(Performance Evaluation Process Algebra)は、1990年代にJane Hillstonによって導入されたコンピュータと通信システムをモデリングするために設計された確率的プロセス代数です。この言語は、ミルナーのCCSやHoareのCSPなどの古典的なプロセス代数を、確率的な分岐と遷移のタイミングを導入することによって拡張します。レートは指数分布から引き出され、PEPAモデルは有限状態であり、確率過程、具体的には連続時間マルコフ過程(CTMC)を生じさせる。したがって、この言語は、スループット、利用率、応答時間、デッドロックの解消などの定性的特性など、コンピュータおよび通信システムのモデルの定量的特性を調べるために使用できます。この言語は、Gordon Plotkinによって発明されたスタイルの構造化された操作セマンティクスを使用して正式に定義されています。
TAPASはピサのIEI CNRによってJACKと呼ばれ、ピサのISTI-CNRによって継続されたツールの実現によって1990年に始まった共同作業の結果です。新しいTAPAsバージョンは、フィレンツェ大学のInformaticaのDipartimento Sistemi edで開発されました。