PAT (Process Analysis Toolkit) is a self-contained framework
for composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It includes user interfaces, model editor and animated simulator. PAT implements various
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
techniques catering for different properties such as freedom from
deadlock and
divergence
In vector calculus, divergence is a vector operator that operates on a vector field, producing a scalar field giving the quantity of the vector field's source at each point. More technically, the divergence represents the volume density of the ...
, reachability,
LTL properties with
fairness assumption
Fairness or being fair can refer to:
* Justice
* The character in the award-nominated musical comedy '' A Theory of Justice: The Musical.''
* Equity (law), a legal principle allowing for the use of discretion and fairness when applying justice ...
s, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g.
partial order reduction In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking or automated planning and scheduling algorithm. It exploits the commutativity of concurrently executed transitio ...
symmetry reduction process counter abstraction.
References
{{Reflist, refs =
[J. Sun, Y. Liu, A. Roychoudhury, S. Liu and J. S. Dong.(2009)]
Fair Model Checking with Process Counter Abstraction
''FM '09 Proceedings of the 2nd World Congress on Formal Methods''. doibr>10.1007/978-3-642-05089-3_9
/ref>
[Yang Liu, Jun Sun and Jin Song Dong.(2011)]
An Extensible Architecture for Building Multi-domain Model Checker
''ISSRE 2011
External links
PAT Website
PAT Forum
Model checkers