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.
We have been using PAT to model and verify a variety of systems. Ranging from recently proposed distributed algorithms, security protocols to real-world systems like multi-lift and pacemaker systems. Previously unknown bugs have been discovered. The Post to Post Links II error: No post found with slug "experiments" results show that PAT is capable of verifying systems with large number of states and outperforms the popular model checkers in some cases. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008), the 21st International Conference on Computer Aided Verification (CAV 2009), International Symposium on the Foundations of Software Engineering (FSE 2010), and the 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011).