PAT: Process Analysis Toolkit

PAT 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.

We design PAT as an extensible and modularized framework, which allows user to build customized model checkers easily. We provide a library of model checking algorithms as well as the support for customizing language syntax, semantics, model checking algorithms and reduction techniques, graphic user interfaces, and domain specific abstraction techniques. Delightfully, PAT has been growing up to eleven modules today to deal with problems in different domains including Real Time Systems, Web Service Models, Probability Models, and Sensor Networks etc. In order to be state-of-the-art, we are actively developing PAT to cope with latest formal-automated system analysis techniques.

The latest version of PAT can be downloaded through the following links.

The main PAT website is at: http://sav.sutd.edu.sg/PAT/