PAT (model checker)
Encyclopedia
PAT is a self-contained framework for 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. So far, PAT has 1350 registered users from 302 organizations in 41 countries and regions.
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
techniques catering for different properties such as deadlock
Deadlock
A deadlock is a situation where in two or more competing actions are each waiting for the other to finish, and thus neither ever does. It is often seen in a paradox like the "chicken or the egg"...
-freeness, divergence
Divergence (computer science)
In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge...
-freeness, reachability, LTL
Linear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
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
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 algorithm...
, symmetry reduction, process counter abstraction. So far, PAT has 1350 registered users from 302 organizations in 41 countries and regions.