Documentation

An overview of PAT

The above figure demonstrates the architecture of our tool. It contains two components: PAT and QuTL MCer.

• PAT implements the core idea of our approach (Algorithm 1, Section 4 of the paper). It contains two main procedures: the observation sequence construction using list abstraction, and the convergence detection using the partial abstract transformer.


• QuTL MCer (QuTL model checker) implements the QuTL model checking algorithms (Section 5 of the paper). When enabled, it is used to filter spurious abstract states in the process of convergence detection. It contains two main procedures: a concrete MCer is called on concrete states in the process of sequence construction. Its main purpose is to test whether the input invariant is valid or not, on the states reached up to the bound. If the concrete MCer reports a violation, then the user has to rewritten the invariant. Otherwise, the invariant will be fed to abstract MCer to filter infeasible abstract states -- those that violate the invariant (see paper for meaning).

Usage: To use our tool, the users first need to compile a P program, which is done via P compiler (See tutorial and Section 6 of the paper for more details). Then, our tool will run the verification on the compiled P program. Our tool provides rich features to perform verification. Two main features are presented as follows:

• /queue-prefix:p:: to verify a P program by specifying an unabstracted prefix of queues.


• /qutl:formula:: to verify a P program using the QuTL MCer.