Experiments of An Analytical Study on Non-Zenoness

Checking for Timed Automata

                                           

This webpage is used to give more details of the experiments in An Analytical Study on Non-Zenoness Checking for Timed Automata. 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.4.1 (Download). They are shown as follows:

 

¡¤         Experiments for CUB-TA emptiness check (TA models download)

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 for CUB-TA emptiness check

The verified models in our experiments include all models in the UPPAAL distribution as well as models which we can find online or published in previous work, i.e., the Fischer¡¯s mutual exclusion algorithm, the railway control system[1], the Lynch-Shavit¡¯s algorithm[8], box sorter unit[9], a simple two door example[10], the TTA model[11], the CSMA/CD protocol [2], and the Fiber Distributed Data Interface (FDDI) [3] and the bridge crossing puzzle[12].

Explanations of models:

¡¤         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.

 

¡¤         Lynch-Shavit Mutual Exclusion

In the original Fischer¡¯s algorithm, two numeral parameters A, B guarantee its correctness provided that B > A. On the contrary, Lynch-Shavit¡¯s algorithm does not depend on constraints on the parameters A and B in order to guarantee the mutual exclusion property. Yet it does rely on them in order to ensure some sort of deadlock freedom. The key point is to add a Boolean variable v2 in order to check whether the value of another process wishing to enter the critical region was overwritten.

¡¤         The TTA Protocol

The Time Triggered Architecture (TTA) enables distributed components to communicate in a fault-tolerant safety-critical way; it is employed in control units of cars and aircrafts. A TTA system is composed of host computers (the nodes) connected over a shared bus. Because many nodes share the bus, a time slot of equal duration is assigned to them, so that each node has to await for its turn in order to transmit - this is called a ¡¯time-division multiple-access strategy¡¯ (TDMA). Moreover, since no global clock signal exists in the system, each node relies only on its local clock in order to know when its turn starts. The goal of the start-up protocol is to synchronize local clocks so that each clock agrees with the others on the owner of the current slot. The basic idea of the protocol is that, when a node receives a packet (carrying the sender¡¯s identity in the global variable origin), it knows the position of the TDMA schedule for the current time and consequently can appropriately set its clock (the local variable c). From this event, a new transmission is going to start every interval with duration equal to the slot time.

 

¡¤         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.

 

¡¤         Two doors example

A room has two doors which can not be open at the same time. A door starts to open if its button is pushed. The door opens for six seconds, thereafter it stays open for at least four seconds, but no more than eight seconds. The door takes six seconds to close and it stays closed for at least five seconds.

 

¡¤         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:

We model check the nine models using our approach as well as the previous approaches based on adding one extra clock[5] and based on adding states in the zone graph [6,7]. For fairness, we reimplemented the previous approaches so that all three algorithms are written in the same programming language (i.e., C#), running on the same platform, built on the same underlying data structure (e.g., the DBM library). The figure below shows the experiment result, where the horizontal axis represents the models used in the experiments; the vertical axis represents the verification time, where ¡®infinity¡¯ means out of memory or more than 2 hours; the columns with different shading represent the the verification time for different method.

 

Discussion:

 

A few observations can be made on the verification results. Firstly, Zeno counterexamples do occur (e.g., in the TTA model and the FDDI model), which shows that model checking with non-Zenoness is necessary. Furthermore, depending the model and the non-Zenoness checking algorithm, model checking with non-Zenoness incurs minor to significant computational overhead. Secondly, the performance of the three approaches varies on different models. The average time cost for GZG over CUB, SNZ over CUB and SNZ over GZG are 255%, 333139% and 234269% respectively. In all the cases, the approach based on adding an extra clock is significantly slower. This is because not only there is one additional clock, additional accepting states must be added so as to make sure one time unit is elapsed during any accepting loop in the zone graph. Notice that the number of additional states equals the number of accepting states in the original model, which is the number of states in the setting of TSA. In all 17 cases, CUB won 12 cases, while GZG won the rest 5. A closer investigation of the models reveals that among the nine systems, six are CUB-TA, whereas the railway control system, the CSMA/CD protocol and the FDDI protocol are not. This suggests that the restriction on non-decreasing upper bounds is not particularly restrictive and, as a result, our CUB-TA based approach could be useful. Furthermore, when a property is valid, the GZG approach has similar performance as ours. This is due to the heuristics proposed in GZG approach, which allows the algorithm to avoid adding states into the zone graph in certain cases. In all the cases when a property is invalid, our algorithm performs significantly better, e.g., GZG over CUB is 302%. The observation is that whenever it is necessary to expand the zone graph (i.e., to build a part of GZG rather than only the zone graph) in order to check non-Zenoness, the GZG approach suffers. This is expected as for CUB-TA, the CUB approach solves the non-Zenoness problem without introducing any clock or state. For the three models which are not CUB-TA, the GZG approach outperforms CUB for the FDDI model. It is because several extra states are introduced during the process of transforming the model into an equivalent CUB-TA. However, if the number of added states is small, the CUB approach may still perform better than the GZG approach. This is exactly the case for the Railway model and the CSMA model, which only introduces one extra state for each automaton to make it CUB.

References

[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¨C258.

[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¨C550.

[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¨C152.

[4]   S. S. Barold, R. X. Stroopbandt, and A. F. Sinnaeve. Cardiac Pacemakers Step by Step: an Illustrated Guide.. Blachwell Publishing, 2004.

[5]   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.

[6]   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.

[7]   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.

[8]   N. A. Lynch and N. Shavit. Timing-based mutual exclusion. In Proc. of IEEE Real-Time Systems Symposium pages 2-11, 1992.

[9]   Kim G. Larsen, Paul Pettersson and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer (STTT) pages 134-152(1), 1997.

[10]  G. Bernat, A. Burns. Combining (mn)-hard deadlines and dual priority scheduling. In 18th international Real-Time Systems Symposium pages 46-57, 1997.

[11]  B. Dutertre and M. Sorea. Timed systems in SAL. Technical Report SRI-SDL-04-03, SRI International, Menlo Park, CA, 2004.

[12]  http://en.wikipedia.org/wiki/Bridge_and_torch_problem#cite_note-a-2.