Experiments of PAT 3: An Extensible Architecture
for Building Multi-domain Model Checkers
This
webpage is used to give more details of the experiments in PAT 3: An Extensible Architecture for Building Multi-domain Model
Checkers. All the PAT models used in this paper are available here.
As we have mentioned in our paper, PAT now supports many kind
of modules, so we compare PAT’s performance with state-of-the-art model
checkers in different domains. All the experiments are finished on the same PC
with 2 Intel Xeon CPUs at 2.13GHz and 32GB RAM.
·
Experiments
compared with SPIN model checker
·
Experiments
compared with UPPAAL model checker
·
Experiments
compared with PRISM model checker
This page is maintained by Yang Liu.
Please contact with us if you
have any question about this webpage or these experiments. We will reply your
enquiries as soon as possible.
In
this part, all the models are based on LTS model checking algorithm. SPIN is
widely used in model checking area since it could support full LTL formulas. In
the following experiments, we choose some benchmark examples such as Dining
Philosophy, Leader Election, token circulation
protocol and so on. Note that “-“ means either out of
32GB memory or more than 4 hours and “N/A” means either a language feature or a
property is not supported in the model checker.
|
Model |
#Proc |
Property |
PAT(s) |
SPIN(s) |
|
deadlockfree dining philosophy |
10 |
deadlock-freeness |
15.7 |
14.1 |
|
same above |
12 |
same above |
232 |
- |
|
leader election for complete network |
6 |
LTL with weak fairness |
26.7 |
229 |
|
same above |
8 |
same above |
726 |
5720 |
|
token circulation protocol for rings |
7 |
LTL with global strong fairness |
13.7 |
N/A |
|
same above |
9 |
same above |
640 |
N/A |
|
5-valued register |
2 |
linearizability |
44.9 |
N/A |
|
6-valued register |
2 |
same above |
297 |
N/A |
|
Scalable Non-Zero Indicator of size
2 |
2 |
same above |
322 |
N/A |
|
Scalable Non-Zero Indicator of size
3 |
3 |
same above |
6214 |
N/A |
The results indicate PAT overperforms SPIN in most of
the cases. PAT supports more kinds of properties such as global fairness
checking and trace refinement checking. Even in those
common properties which are supported by both tools, PAT has much better
performance than SPIN except the DP(n=10) case.
UPPAAL
is popular in modeling and verifying real-time systems. The semantic model of
this kind of system is Timed Transition Systems (TTS). We also choose some
benchmark systems in real-time domain such as Fischer’s mutual exclusion,
railway control system and CSMA/CD protocol. Note that Uppaal-o means verifying a system
with extrapolation disabled and “-“ means either out
of 32GB memory or more than 4 hours.
|
Model |
#Proc |
Property |
PAT(s) |
Uppaal(s) |
Uppaal-o(s) |
|
Fischer's mutual exclusion protocol |
4 |
mutual exclusion |
0.05 |
0.09 |
1.18 |
|
same above |
5 |
same above |
0.15 |
0.19 |
696.4 |
|
same above |
6 |
same above |
0.68 |
0.81 |
- |
|
CSMA/CD protocol |
5 |
liveness LTL |
0.22 |
0.26 |
39.15 |
|
same above |
7 |
same above |
2.63 |
6.40 |
- |
|
same above |
10 |
same above |
34.3 |
181 |
- |
|
ailway control system |
6 |
liveness LTL |
5.24 |
0.43 |
- |
|
same above |
8 |
same above |
349 |
20.7 |
- |
The data show
the experimental results on applying TTS based model checking algorithms (using
zone abstraction) to benchmark real-time systems. PAT’s performance is compared
with the UPPAAL model checker. Three benchmark real-time systems are used. The
column Uppaal shows the time of verifying the models
using Uppaal. PAT is faster than Uppaal
for the first two examples due to the effective zone abstraction technique. In
the last example, Uppaal outperforms PAT by using the
effective optimization techniques named extrapolation. The column Uppaal-o shows the result of verifying the same models with
extrapolation disabled. PAT outperforms Uppaal-o
significantly. This has lead to our ongoing work on realizing extrapolation in PAT’s
DBM package.
PRISM
is widely used in probabilistic model checking; therefore we pick some examples
PRISM has and rebuild them in PAT. PRSIM supports models which are based on Markov
Decision Processes(MDP) and Continuous Time Markov
Chains(CTMC), and in this paper we choose its MDP examples since till now MDP
is the semantic model for probabilistic model checking in PAT. In the following
are the models.
·
Mutual Exclusion (ME) model describes a probabilistic
solution to N-process mutual exclusion [1]
· Dining Philosopher (DP) model describes the probabilistic N-dining philosophers under fairness [2]
· Randomized Consensus(RC) model describes the shared coin protocol of the randomized consensus algorithm [3]
·
CSMA/CD (CS) is the IEEE 802.3 Carrier Sense, Multiple Access
with Collision Detection protocol
|
Model |
#Proc |
Property |
PAT(s) |
PRISM(s) |
|
ME |
6 |
safety: mutual exclusion |
1.161 |
0.364 |
|
ME |
8 |
same above |
8.624 |
0.937 |
|
DP |
5 |
deadlock-freeness |
2.413 |
0.156 |
|
DP |
6 |
same above |
25.775 |
0.672 |
|
RC |
4 |
liveness LTL |
0.379 |
21.9 |
|
RC |
6 |
same above |
5.854 |
1755 |
|
CS |
2 |
liveness LTL |
0.933 |
2.314 |
|
CS |
3 |
same above |
6.284 |
7.233 |
The results of the
experiments indicate that PAT has comparable performance with PRISM. The main reason
that PRISM overperforms PAT in several cases is that
PRISM is based on symbolic model checking-BDD,
which
can handle large number of states in these examples. Meanwhile, PRISM has much
longer history than PAT so that many optimizations have been implemented in it.
It is our future work to optimize the probabilistic model checking in PAT.
1.
Pnueli and L. Zuck. Verification of Multiprocess
Probabilistic Protocols. Distributed Computing, 1(1), pages 53--72.
1986.
2.
D. Lehmann and M. Rabin.On the Advantage
of Free Choice: A Symmetric and Fully Distributed Solution to the Dining
Philosophers Problem (Extended Abstract).In Proc. 8th Annual ACM
Symposium on Principles of Programming Languages (POPL'81), pages
133--138.1981.
3.
J. Aspnes and M. Herlihy.Fast
Randomized Consensus Using Shared Memory. Journal of Algorithms, 15(1),
pages 441--460.1990.