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 examples 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.