PAT (Process Analysis Toolkit) is a self-contained framework for to support composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, symmetry reduction, process counter abstraction, parallel model checking. So far, PAT has 3502+ registered users from 932+ organizations in 87 countries and regions.
The main functionalities of PAT are listed as follows:
- User friendly editing environment (multi-document, multi-language, I18N GUI and advanced syntax editing features) for introducing models
- User friendly simulator for interactively and visually simulating system behaviors; by random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
- Easy verification for deadlock-freeness analysis, reachability analysis, state/event linear temporal logic checking (with or with fairness) and refinement checking.
- A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.
The latest version of PAT can be downloaded through the following links.
- PAT 3.5.1 installation file for Windows OS 32 bit
- PAT 3.5.1 installation file for Windows OS 64 bit
- PAT 3.5.1 without installation
The main PAT website is at: http://sav.sutd.edu.sg/PAT/