Experiments of Modeling and Verifying
Hierarchical Real-time Systems
using Stateful Timed CSP
This webpage
is used to give more details of the experiments in Modeling and Verifying Hierarchical Real-time Systems using Stateful
Timed CSP. Stateful Timed CSP is the modeling language of RTS module of PAT model checker. All the experiment
files (PAT tool, PAT models, UPPAAL tool, UPPAAL models, and
experiments data) in this paper are available here.
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.3. They are shown as
follows:
·
Experiments on verification
of real time models
·
Experiments compared with
UPPAAL
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.
The verified models
in our experiments include the pacemaker model, the lift system, and benchmark
real-time systems like Fischer’s mutual exclusion algorithm, the railway
control system [1] , the CSMA/CD protocol
[2], and the Fiber Distributed Data
Interface (FDDI) [3].
Explanations of
models:
·
Pacemaker
A pacemaker is an electronic device used to
treat patients who have symptoms caused by abnormally slow heartbeats. A
pacemaker is capable of keeping track of the patient's heartbeats. If the
patient's heart is beating too slowly, the pacemaker will generate electrical
signals similar to the heart's natural signals, causing the heart to beat
faster. The purpose of the pacemaker is to maintain heartbeats so that adequate
oxygen and nutrients are delivered through the blood to the organs of the body.
The pacemaker in this example has several
operating modes that address different malfunctions of the natural pacemaker.
The operating modes of the device are classified using a code consisting of
three or four characters. For example, the code elements in our model are:
chamber(s) paced (O for none, A for atrium, V for ventricle, D for both),
chamber(s) sensed (same codes) and a final optional R to indicate the presence
of rate modulation in response to the physical activity of the patient as
measured by the accelerometer. We consider all 16 operating modes of the
pacemaker.
·
Lift
systems
The lift system consists of a building,
multiple lifts and a central controller. A building consists of multiple floors
and each floor is equipped with one button panel on the wall so that a user can
make an external request to traveling upwards or downwards. A button can
be pushed at any time. Once pushed, the button is on until the requested
service is provided. Each lift consists of four components, i.e., a door for
allowing access to and from the lift, a shaft for transporting the lift, an
internal queue for determining the lift itinerary and a controller to
coordinate the behaviors of the other components. The central controller is
responsible for assigning external requests to specific lifts. Upon receiving
the message from a lift, the central controller checks the pool of external
requests and decides whether to assign an external request to the lift. Once
the lift controller received the new destination from the central controller,
its behaviors diverge.
·
Fischer’s
Protocol for Mutual Exclusion
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 system
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
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.
·
Fiber Distributed
Data Interface(FDDI)
Fiber Distributed Data Interface (FDDI) is a
high-performance fiber-optic token ring Local Area Network. An FDDI network is
composed by N identical stations and a ring, where the stations can communicate
by synchronous messages with high priority or asynchronous messages with low
priority. Our model consists of two components, i.e., token ring and station.
The behavior of ring is modeled as sending a token to a station, passing the token to next station when receiving release token message of the station.
Station can communicate asynchronous messages only when there is time for it
transmitting.
Experiment
results:
All properties in the experiment are verified with or without the assumption of Non-Zenoness. The verification time without non-Zenoness is shown in column Z and the time with non-Zenoness is shown in column NZ. Column #St shows the number states in the zone graphs. Column #Clock shows the maximum number of clocks created during the verification.
|
Model |
Property |
#St |
#Clock |
Z(s) |
NZ(s) |
|
Pacemaker |
reachability |
450K |
2 |
21 |
21 |
|
Lift (2floor; 2lift) |
reachability |
197K |
4 |
54 |
53 |
|
Lift (3floor; 2lift) |
reachability |
943K |
4 |
310 |
305 |
|
Lift (2floor; 2 lift) |
LTL |
748K |
4 |
345 |
305 |
|
Lift (3floor; 2lift) |
LTL |
4.3M |
4 |
6102 |
3948 |
|
Fischer* 5 |
LTL |
15K |
5 |
1 |
1 |
|
Fischer* 7 |
LTL |
857K |
7 |
229 |
105 |
|
Railway*4 |
LTL |
2K |
4 |
<1 |
<1 |
|
Railway*6 |
LTL |
74K |
4 |
6 |
6 |
|
Railway*8 |
LTL |
4.3M |
4 |
1536 |
1200 |
|
CSMA*6 |
LTL |
14K |
5 |
2 |
2 |
|
CSMA*9 |
LTL |
295K |
5 |
75 |
71 |
|
CSMA*12 |
LTL |
4.7M |
5 |
11475 |
9303 |
|
FDDI*4 |
LTL |
46K |
6 |
10 |
8 |
|
FDDI*5 |
LTL |
6.4M |
7 |
1461 |
1438 |
Discussion:
A number of observations can be obtained
from the data. Firstly, PAT currently handles in average 20K states per second (i.e., the total number of visited states - not
new states - divided by the total number of seconds), which is reasonable
compared to existing model checkers [3, 4, 5]. Secondly, model
checking with non-Zenoness has little or no computational overhead and may be
even more efficient. Compared to other work on model checking with non-Zenoness
[6, 7, 8, 9], this is a clear
advantage. Thirdly, for some models, the number of clocks remains constant when
the system size increases, e.g., the railway control system and the CSMA/CD
protocol.
UPPAAL is popular in modeling and
verifying real-time systems. The semantic model of this kind of system is Timed
Automata. In this part, we conducted experiments to compare performance of PAT
and UPPAAL. We choose some benchmark systems in real-time domain
such as Fischer’s mutual exclusion, railway control system and CSMA/CD
protocol. Note that “-“denotes that the experiment is aborted due to out of
memory or running more than 4 hours, UPPAAL(s)
denotes the verification time using UPPAAL, with all optimization
techniques, UPPAAL+ τ-o shows the verification time using
UPPAAL without extrapolation (and with the same extra
τ -transitions so that the models in PAT and UPPAAL
have similar state spaces).
|
Model |
#Clocks |
Without
Non-Zenoness |
|||
|
PAT |
UPPAAL |
PAT(s) |
UPPAAL(s) |
UPPAAL+
τ-o(s) |
|
|
Fischer*5 |
5 |
5 |
<1 |
<1 |
696 |
|
Fischer*6 |
6 |
6 |
7 |
1 |
- |
|
Railway*6 |
4 |
6 |
2 |
<1 |
- |
|
Railway*7 |
4 |
7 |
15 |
6 |
- |
|
CSMA*6 |
5 |
7 |
1 |
<1 |
- |
|
CSMA*8 |
5 |
9 |
11 |
5 |
- |
|
CSMA*10 |
5 |
11 |
97 |
18 |
- |
Discussion:
From the above experiments, we could claim that PAT often outperforms UPPAAL without extrapolation. However, PAT is slower than UPPAAL simply because some effective optimization techniques are currently missing. One particular example is extrapolation. One of our future works is to implement these powerful optimization techniques in PAT.
[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] Larsen, K. G.,
Pettersson, P., and Wang, Y. 1997. Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer 1, 1-2, 134–152.
[4] Holzmann, G. J.
2003. The SPIN Model Checker: Primer and
Reference Manual. Addison Wesley.
[5] Roscoe, A. W.,
Gardiner, P. H. B., Goldsmith, M., Hulance, J. R., Jackson, D. M., and
Scattergood, J. B. 1995. Hierarchical Compression for Model-Checking CSP or How
to Check 1020 Dining Philosophers for Deadlock. In First International Workshop on Tools and Algorithms for Construction
and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol.
1019. Springer, 133-152.
[6] Tripakis, S.
1999. Verifying Progress in Timed Systems. In 5th International AMAST Workshop ARTS on Formal Methods for Real-Time
and Probabilistic Systems. Lecture Notes in Computer Science, vol. 1601.
Springer, 299-314.
[7] GÓmez, R. and Bowman, H. 2007. Efficient Detection of Zeno Runs in Timed Automata. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 4763. Springer, 195-210.
[8]
Herbreteau, F. and Srivathsan, B.
2010. Efficient On-The-Fly Emptiness Check for Timed Büchi Automata. In 8th International Symposium on Automated
Technology for Verification and Analysis (AVTA). Lecture Notes in Computer
Science. Springer.
[9] Herbreteau, F.,
Srivathsan, B., and Walukiewicz, I. 2010. Efficient Emptiness Check for Timed
Büchi Automata. In 22nd International
Conference on Computer Aided Verification (CAV). Lecture Notes in Computer
Science, vol. 6174. Springer, 148-161.