Experiments of Improving
Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry
Reduction
This
webpage is used to give more details of the experiments in Improving Model Checking Stateful Timed CSP with non-Zenoness through
Clock-Symmetry Reduction. All the experiment files and data in this paper
are available in this page.
We construct experiments to evaluate efficiency of our
method proposed in paper. All the experiments are run on a PC with 2 Intel® Xeon® CPUs @2.13GHz and 32GB RAM, on a 64-bit
Windows system and PAT version 3.5.0 (Download). They
are shown as follows:
·
Experiments
results for STCSP.
(Click here to download RTS models)
This
page is maintained by Yang Liu.
PAT 3.5.0 requires .NET Framework 4.0 or above, please
download here.
PAT 3.5.0 is a direct executable in Windows. After downloading it, unzip and
click PAT 3.exe to start.
How to run TA and RTS models with the proposed model checking
algorithms:
1. Open PAT 3.exe.
2. Choose models from the menu Examples: Timed Automata Examples
or Real-Time System Examples or open the models downloaded from this website.
3. Press 'Verification' or F7 to display the verification UI.
4. Select an LTL assertion, choose 'Non-Zeno only' from the option
of Admissible Behavior, choose one verification engine and press 'Verify'.
Please contact with us if you
have any question about this webpage or these experiments. We will reply your
enquiries as soon as possible.
We
evaluate the efficiency of our method using five examples. The first three are
benchmark real-time systems: Fischer’s mutual exclusion algorithm, the railway
control system [1] and the CSMA/CD
protocol [2], described as follows. In
addition, we model and verify two hierarchical systems: a simplified pacemaker [3], and a multi-lift system, described in the
paper.
Explanations of models:
Mutual exclusion protocol was
first proposed by Fischer in 1985. To assure mutual exclusion, Fischer's
protocol assumes atomic reads and writes to a shared variable. Mutual exclusion
in Fischer's Protocol is guaranteed by carefully placing bounds on the
execution time of the instructions, leading to a protocol which is very simple,
and relies heavily on time aspects.
Railway control systems
automatically control trains passing a critical point such as a bridge. It uses
a computer to guide trains from several tracks crossing a single bridge instead
of building many bridges. Obviously, a safety-property of such a system is to
avoid the situation where more than one train is crossing the bridge at the
same time. Our model consists of three components: a train, a gate and a
controller. The gate is lowered to allow trains to cross the bridge and up when
there is no train crossing the bridge. The controller monitors the approaching
of a train, and instructs the gate to be lowered within the appropriate time.
The train is modeled abstractly with nearing, entering and leaving behaviors.
CSMA/CD protocol (Carrier
Sense, Multiple-Access with Collision Detection) describes a solution to the
problem of assigning the bus to only one of many competing stations arises in a
broadcast network with a multi-access bus. Roughly, whenever a station has data
to send, it first listens to the bus. If the bus is idle (i.e., no other
station is transmitting), the station begins to send a message. If it detects a
busy bus in this process, it waits a random amount of time and then repeats the
operation. When a collision occurs, because several stations transmit
simultaneously, then all of them detect it, abort their transmissions
immediately and wait a random time to start all over again. Our model consists
of two components, i.e., bus and station. It specifies the behaviors of bus
such as idle, busy and conflicting, the behaviors of stations like waiting for
messages, sending messages, finish sending messages and receiving conflicting
messages.
Experiment results:
The table below summarizes the experiment results. Column RZG shows the verification statistics based on constructing RZG (which renames clocks but not anonymize them). Column K shows the maximum number of overlapping clocks. Column +Zeno shows the verification time without the non-Zenoness assumption, and -Zeno shows the verification time with the non-Zenoness assumption. Similarly, column QAG shows the verification statistics based on constructing QAG. Column OH shows the overhead of non-Zenoness check and column Speedup shows the improvement. Note that ‘-’ means that the data is not available (either out of memory or running for more than 8 hours).
|
Model
|
K |
RZG |
QAG |
Speedup |
||||||
|
States |
+Zeno(s) |
-Zeno(s) |
States |
+Zeno(s) |
-Zeno(s) |
OH |
+Zeno |
-Zeno |
||
|
Fischer*5 |
5 |
1.1M |
180 |
361 |
36K |
3 |
4 |
33% |
60 |
90.25 |
|
Fischer*6 |
6 |
- |
- |
- |
291K |
50 |
73 |
46% |
- |
- |
|
Fischer*7 |
7 |
- |
- |
- |
2.6M |
1557 |
4522 |
190% |
- |
- |
|
Railway*6 |
4 |
158K |
14 |
16 |
74K |
6 |
6 |
0% |
2.33 |
2.67 |
|
Railway*7 |
4 |
1.1M |
143 |
203 |
527K |
44 |
53 |
15% |
3.25 |
2.83 |
|
Railway*8 |
4 |
9.1M |
4895 |
8104 |
4.3M |
818 |
1339 |
64% |
5.98 |
13.55 |
|
CSMA*6 |
5 |
30K |
4 |
5 |
15K |
2 |
2 |
0% |
2 |
2.5 |
|
CSMA*8 |
5 |
237K |
46 |
54 |
119K |
20 |
21 |
5% |
2.3 |
2.57 |
|
CSMA*10 |
5 |
1.6M |
1012 |
1291 |
803K |
239 |
338 |
64% |
4.23 |
3.82 |
|
Pacemaker |
- |
- |
- |
- |
1.2M |
8711 |
- |
- |
- |
- |
|
Lift*2*2 |
4 |
8.7M |
12271 |
22260 |
756K |
297 |
728 |
145% |
42.31 |
30.57 |
Discussion:
A few observations can be
made based on the results. Firstly, it can be shown from the data that non-Zenoness
checking incurs some overhead. The theoretical study shows that in the worst
case the state space could be enlarged by a factor of 1 + K2,
whereas in all the experiments, model checking with non-Zenoness takes less
than three times the time needed for model checking without non-Zenoness. In
average, the overhead is 58% of the verification time without non-Zenoness.
Secondly, the experiment results confirm that the verification is significantly
faster compared to [6, 7]
in all cases, because clock symmetry reduction is combined with non-Zenoness
check. The speedup ranges from 2 to 90.25 times. In average, the speedup is 17
for this set of experiments. It can be further noticed that though in theory
that the more clocks, the more potential speedup there is, the actual speedup
depends on the particular models.
[1]
Yi, W., Pettersson, P., and Daniels,
M. 1994. Automatic Verification of Real-time Communicating Systems by
Constraint-Solving. In 7th IFIP WG6.1
International Conference on Formal Description Techniques (FORTE). IFIP
Conference Proceedings, vol. 6. Chapman & Hall, 243–258.
[2] Bozga,
M., Daws, C., Maler, O., Olivero, A., Tripakis, S., and Yovine, S. 1998. Kronos:
A Model-Checking Tool for Real-Time Systems. In 10th International Conference on Computer Aided Verification (CAV).
Lecture Notes in Computer Science, vol. 1427. Springer, 546–550.
[3] S. S.
Barold, R. X. Stroopbandt, and A. F. Sinnaeve. Cardiac Pacemakers Step by Step: an Illustrated Guide.. Blachwell
Publishing, 2004.
[4] Jun
Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, and ´ Etienne Andr´e. Modeling
and verifying hierarchical real-time systems using stateful timed csp. ACM
Transactions on Software Engineering and Methodology (TOSEM), 22(1):3, 2013.