Experiments of A Model Checker for Hierarchical
Probabilistic Real-time Systems
This
webpage is used to give more details of the experiments in A Model Checker for Hierarchical Probabilistic Real-time Systems.
All the examples are available here. The
PRTS plugin for Visual Studio 2010 can be downlodaed here.
We use our model checker PAT (Windows version can
be directly downloaded here) to fulfill these experiments on a PC runing
Windows XP with Intel P8700 CPU at 2.53GHz and 2GB RAM, and in the following
are two kinds of examples we use in our paper.
·
Experiments
compared with PRISM model checker
This page is maintained by Songzheng Song.
Please contact with us if you
have any question about this webpage or these experiments. We will reply your
enquiries as soon as possible.
As
we have described in our paper, this motivating example is based on an
interesting phenomena: sometimes a user has requested a service in multi-lift
system, but a lift traveling in the same direction passes by that user and the
user must wait for another lift to serve him. This is actually because of the
request assignment algorithm in the system and some other unpredictable reasons
such as a lift could be occupied by other users for an unexpected long
time.
Therefore, we have modeled such lifts system in order to check the probability that this phenomena could happen. To make it more reasonable, we use two assignment algorithms. The “random” algorithm means the lift system randomly picks one lift to assign the service task, while the “nearest” algorithm indicates the lift system will calculate the distances from the user to all the lifts and pick the one having the smallest distance at the current moment.
The
property is specified as a reachability property in our model. We have defined
a target status “goal” when this phenomena happens and used the assertion “#assert System reaches goal with pmax” to calculate
the maximum probability of this undesired phenomena. The results in the
following table tell us that assigning users’ requests to the “nearest” lift is
much better than to a random one. Here R is
short for random and N for nearest.
|
System |
Result-R (pmax) |
States-R |
Time-R (s) |
Result-N (pmax) |
States-N |
Time-N (s) |
|
lift=2;
floor=2; user=2 |
0.21875 |
20120 |
1.47 |
0.13889 |
12070 |
1.33 |
|
lift=2;
floor=2; user=3 |
0.47656 |
173729 |
15.04 |
0.34722 |
83026 |
6.23 |
|
lift=2;
floor=2; user=4 |
0.6792 |
777923 |
90.66 |
0.53781 |
308602 |
28.31 |
|
lift=2;
floor=2; user=5 |
0.81372 |
2175271 |
406.29 |
0.68403 |
740997 |
85.29 |
|
lift=2;
floor=3; user=2 |
0.2551 |
72458 |
5.13 |
0.18 |
38593 |
2.89 |
|
lift=2;
floor=3; user=3 |
0.54009 |
1172800 |
150.20 |
0.427 |
500897 |
48.05 |
|
lift=2;
floor=4; user=2 |
0.27 |
170808 |
13.06 |
0.19898 |
86442 |
6.11 |
|
lift=3;
floor=2; user=2 |
0.22917 |
562309 |
86.88 |
0.10938 |
266621 |
34.25 |
PRISM
is widely
used in probabilistic model checking; PRISM 4.0 supports the combination of
probability and real-time: Probabilistic Timed Automata (PTA). Therefore we
pick two protocols from PRISM’s work, and model them seperately in PRISM and
PRTS.
·
Firewire abstract (FA) is an abstraction model
of the IEEE 1394 FireWire root contention protocol. In this model, we want to
check the minimum probability of successfully
choosing a leader before a specified deadline. In PRISM, this property is
specified as “Pmin=?[F s=9]” where s=9 means a leader is chosen before the
deadline. In PAT, we specify this property using an SE-LTL formula to show the
expressiveness of our language. “System |= <>done with pmin;” here done is an event, which occurs when a leader is
chosen before the deadline.
·
Zeroconf (ZC) model describes the
Zeroconf network protocol. In this model, we want to check the maximum probability of getting an IP (might be used or
fresh) after a specific deadline. In
PRISM, this property is specified as “Pmax=?[F r=2]” where r=2 means the an IP
is obtained after deadline. In PAT, this time we specify this property using a
reachability property. “System
reaches goal with pmax;” here goal is propositions
which define the target states.
The
following table shows the results of the verifications in these models and
record the time every verification consumes. P
stands for PRTS and T stands for PTA in
PRISM.
|
System |
Result |
States-P |
Time-P (s) |
States-T |
Iterations-T |
Time-T
(s) |
|
FA(10K) |
0.94727 |
1352 |
0.15 |
1065 |
19 |
1.98 |
|
FA(20K) |
0.99849 |
5030 |
0.13 |
8663 |
34 |
65.08 |
|
FA(30K) |
0.99994 |
11023 |
0.45 |
34233 |
45 |
575.03 |
|
FA(300K) |
>0.99999 |
726407 |
30.74 |
- |
- |
- |
|
ZC(100) |
0.49934 |
404 |
0.15 |
135 |
0 |
0.28 |
|
ZC(300) |
0.01291 |
4813 |
0.65 |
2129 |
26 |
2.73 |
|
ZC(500) |
0.00027 |
12840 |
2.39 |
10484 |
44 |
63.19 |
|
ZC(700) |
1E-5 |
24058 |
5.78 |
31717 |
60 |
427.70 |
The
parameter in each case is a specified deadline; ‘-’ means that experiments
takes more than 1 hour. Iterations in
PRISM stands for the number of refinement in there stochastic game approach. In these cases PRTS is much faster, since
our approach just uses zone abstraction, while theirs should have additional
refinement procedure.