The Algorithms for the feasible test are shown as follows.

The Algorithm for model checking is shown as follows.

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

The Algorithms for the feasible test are shown as follows.

The Algorithm for model checking is shown as follows.

A veriaty of systems have been analysized using PAT. Also, we have built-in some of the examples (with model description and user options) for user convenience. More may be expected in the future. You can also find more experiments in our Publications.

- newly developed population protocols, e.g., self-stablizing leader protocols for complete network, network rings, rooted tree, etc.
- the pace maker system from the pace maker challenge.
- security protocols, e.g., multi-party contract signing protocol.
- concurrent algorithms, e.g., concurrent stack, queue, the mailbox problem, etc.
- real applications: lift system, keyless car system.
- benchmark systems like dining philosophers, Milner’s cyclic scheduler, Peterson’s algorithm, etc.

The following are some experiment results obtained using PAT version 1.3.0. As we are actively developing PAT, the number may not be exact now. The data is obtained on Windows XP platform with Core 2 CPU 6600 at 2.4 GHZ and 2GB Memory. It shows the verification statistics over recent population protocols, namely self stablizing leader election for complete networks, for rooted trees, for odd sized rings, for network rings and token circulation for network rings. Correctness of all these examples relies on some form of fairness.

The following shows verification statistics of benchmark systems to show other aspects of PAT. Because of the deadlock state, the dining philosophers model (dp(N) for N philosophers and forks) does not guarantee that a philosopher always eventually eats ([]<> eat0) whether under no fairness or the strongest fairness. This experiment shows textsc{Pat} takes little extra time for handling the fairness assumption. Notice that SPIN finds a counterexample (under no fairness) quickly. This is due to the particular order of exploration as well as its nested depth-first-search algorithm. Milner’s cyclic scheduler algorithm (ms(N) for N processes) is a showcase for the effectiveness of partial order reduction. We apply fairness in two different ways, i.e., one applying strong local fairness to the whole system (slf-whole) and the other applying only to inter-process communications (slf-action). In the latter case, partial order reduction allows us to prove the property over a much larger number of processes (e.g., 200 vs 12). Peterson’s mutual exclusive algorithm (peterson(N)) requires process-level weak fairness to guarantee bounded by-pass. The property is verified under weak fairness in PAT and process-level weak fairness in SPIN. PAT outperforms SPIN in this setting.

Experiment results of PAT 1.2.6 build 4600 on linearizability testing based on the refinement relations are shown in the following figure. The testbed is a PC with 2.83GHz Intel Core Quad Q9550 CPU and 4 GB memory.

In the experiments, the number of states and the running time increase rapidly with increasing data size or the number of processes, e.g., 3 processes (in the Register , Stack or Queue) vs. 2 processes. Nonetheless, because of partial order reduction (as well as other built-in optimization techniques), our algorithm is more robust to the data size. The partial order reduction can effectively reduce the search space and running time in most of the cases (Mailbox, Stack, Queue). However, in Register , partial order reduction produces fewer states but bigger normalized states, which increases running time when the number of states increases. The counterexamples in the Buggy Queue are detected quickly by searching part of the state space. Compared with the results in other method, our solution is much more scalable to handle all the possible interleaving of operations. In summary, PAT is effective and can handle millions of states in hours.