PAT (モデルチェッカー)

パット
開発者	シンガポール国立大学
初回リリース	2008
安定版リリース	3.5.1 / 2013年8月13日; 11年前
書かれた	C#
オペレーティング·システム	Microsoft Windows、Linux、Unix、Mono搭載Mac OS X
プラットフォーム	.Net 3.0
利用可能	英語; 中国語(簡体); 中国語(繁体); 日本語; ドイツ語; ベトナム語
タイプ	モデルチェック
Webサイト	翻訳：

PAT (プロセス分析ツールキット)は、並行システム、リアルタイムシステム、およびその他のドメインの構成、シミュレーション、推論のための自己完結型フレームワーク^{[1]です。ユーザーインターフェイス、モデルエディター、アニメーションシミュレータが含まれています。PAT は、}デッドロックや発散の回避、到達可能性、公平性仮定によるLTLプロパティ、リファインメントチェック、確率モデルチェックなど、さまざまなプロパティに対応するさまざまなモデルチェック手法を実装しています。優れたパフォーマンスを実現するために、PAT には、部分順序削減、対称性削減、プロセスカウンター抽象化などの高度な最適化手法が実装されています。 ^[2]

参考文献

^ Yang Liu、Jun Sun、Jin Song Dong (2011)、マルチドメインモデルチェッカーを構築するための拡張可能なアーキテクチャ。ISSRE 2011
^ J. Sun、Y. Liu、A. Roychoudhury、S. Liu、JS Dong (2009)、プロセスカウンター抽象化による公平なモデル検査。FM '09 Proceedings of the 2nd World Congress on Formal Methods。doi : 10.1007 /978-3-642-05089-3_9