Experiments of Building Model Checkers Made Easy
This webpage
is used to give more details of the experiments in Building Model Checkers Made Easy. 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 |
1.17 |
0.09 |
1.18 |
same above |
5 |
same above |
23.0 |
0.09 |
696.4 |
railway control system |
6 |
liveness LTL |
7.24 |
0.43 |
- |
same above |
8 |
same above |
949 |
20.67 |
- |
probabilistic CSMA/CD protocol |
5 |
liveness LTL |
0.94 |
0.26 |
39.15 |
same above |
7 |
same above |
9.19 |
6.40 |
- |
From the above experiments, we
could claim that PAT has much better performance than UPPAAL-o in these
benchmark examples. However, UPPAAL’s extrapolation technique is very useful in
verifying such kind of system and this should be our motivation to implement it
in PAT.
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.