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.

 


 

 

 

 

 

Experiments compared with SPIN model checker

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.


 

Experiments compared with UPPAAL model checker            UPPAAL models are available here.

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.

 


 

 

Experiments compared with PRISM model checker              PRISM models are available here.

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.

 


 

References

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.