This page’s menu:

Some of the source files refered to from this page are unfortunately missing. We are working on relocating the files and make them available again.

Run-Time Data for Uppaal

<TABLE BORDER="0" SUMMARY="HEADLINE_INFO">
Versionverifyta-3.1.64
OS Solaris
MachineSparc 450 MHz / 4GB main memory
TIME is in seconds
SPACE is in KB/MB as denoted
**aborted computations point to the longest tried time
Available Run-Time Examples:
Fischer's Mutex
CSMA/CD Protocol
Token Ring FDDI Protocol
Philips Audio Protocol
Bang & Olufsen Collision Detection Protocol
Bang & Olufsen Power Down Protocol


The performance of Uppaal’s model-checking engine is heavily dependent on the enabling/disabling of various optimization options.

The standard switch settings -Was suppress deadlock warnings (W), enable active clock reduction (a) and suppress a progress counter (s).

The full option list is

  -A  Use convex-hull approximation.
  -C  Disable use of compact data structures (normally enabled).
  -Q  Display warnings as queries.
  -H size
      Change size of hash table in passed list (default = 17609).
  -S <0|1|2>
      Optimize space consumption (0 = none, 1 = default, 2 = most)
  -T  Optimize time consumption when several properties are examined.
  -U  Unpack reduced constraint systems before relation test.
  -Z  Use bit-state hashing.
  -a  Detect active/inactive clocks.
  -b  Use breadth-first search of the state space. (default)
  -d  Use depth-first search of the state space.
  -g  Show CDD garbage collection info.
  -h  Print this message.
  -q  Do not display the copyright message.
  -s  Run silently, i.e. do not display the progress indicator.
  -t  Generate diagnostic information on stdout.
  -y  Display traces symbolically.

Note that -A is an over-approximation. However, safety properties (invariants, declared as A[] invariant) can be verified faithfully:

If the bad state is reached in the over-approximation, this means that the invariant is possibly violated. In this case, the output of verifyta reports the result MAYBE satisifed. If verifyta reports an invariant to be satisfied in the over-approximation, it is satisfied in the the original system as well.



Note that the run-times are not averaged over several runs; instead, the best detected run-time of one or more runs was taken (context switches and usage of swap can easily increase measured run-time, but it is hard to “cheat” on the fastest run). The memory usage is deterministic.

Small differences (like the fraction of a second) are not to be considered significant. Sometimes the ‘best’ options vary with increasing Size, simply because the measured run-times were nearly identical. You can get the complete time- or space-chart of measurements by following the link under the best found switch-settings in the corresponding line.

The memtime utility version 1.2 - (thanks to Johan Bengtsson) - was used for all the measurements.


Fischer

This conceptually simple and elegant mutual exclusion algorithm is due to Michael Fischer. The basic idea is that the participants write their (unique) identifier to a shared variable, then wait some amount of time, and if their number is still on the blackboard, the proceed to the critical region. Otherwise, they go back to start. A detailed description can be found e.g. in the article [AL92].

Though this example behaves ‘odd’ in many respects, it is often used as a benchmark problem for timed model-checking systems.

Note that there are various versions of Fischer around, in particular the time of the delay k (here: 2) can vary and potentially affect the model-checking performance.
In the case of Uppaal, changing this constant k amounts to adjusting the bounds in the symbolic representation of clock evaluation by a factor. Here the model-checking times are robust with respect to variations of k.

The inputs were generated by this file. There is also a (generic) graphical version for Uppaal.

(For Size > 9, the search for good options was no longer exhaustive).

Size Prop with default option -Was best time best space
2 .q .01 1464KB -WasA .00 912KB -WsS2d .02 712KB
3 .q .03 912KB -WasS0A .01 912KB -WasC .03 720KB
4 .q .23 2688KB -WasA .06 912KB -WasA .06 912KB
5 .q 5.09 4600KB -WasA .29 2656KB -WasS2Ad .60 2608KB
6 .q 310.97 29096KB -WsAC 1.34 3456KB -WasS2Ad 5.32 2840KB
7 .q 51598.17 385392KB -WsS0AC 5.89 6160KB -WasS2Ad 43.58 3624KB
8 .q **14394.25 **312432KB -WsS0AC 25.83 16576KB -WasS2Ad 534.83 6248KB
9 .q **60942.63 **401776KB -WsA 113.53 55544KB -WasS2Ad 8034.69 14672KB
10 .q **14397.04 **500104KB -WsA 498.88 199904KB -WasS2A 681.52 79088KB
11 .q **12619.08 **852024KB -WsAC 2525.31 722136KB -WasS2A 3005.60 272824KB
12 .q **6084.95 **853480KB   **15801.35 **743176KB   **15801.35 **743176KB


CSMA/CD Protocol

In a broadcast network with a multi-access bus, the problem of assigning the bus to only one of many competing stations arises. The CSMA/CD protocol (Carrier Sense, Multiple-Access with Collision Detection) describes one solution. Roughly, whenever a station has data to send, if 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.

A detailed description of the (simplified) model we use is found e.g. in [Y97].

The inputs were generated by this file. The constants were adjusted to coincide with the numbers Farn Wang used as benchmarks for his RED tool.



(For Size > 9, the search for good options was no longer exhaustive).

Size Prop with default option -Was best time best space
2 .q .02 1464KB -WasAC .00 912KB -WasAdC .01 712KB
3 .q .02 912KB -WasAC .01 912KB -Was .02 912KB
4 .q .14 2608KB -WasAC .05 912KB -WasA .06 912KB
5 .q 1.22 3128KB -WsS0A .20 2680KB -WasS0AC .21 2648KB
6 .q 19.44 6960KB -WsS0AC .71 3056KB -WasS0AC .72 3008KB
7 .q 746.65 40080KB -WasS0A 2.47 4240KB -WasAd 11.47 4192KB
8 .q **14438.59 **326256KB -WsS0A 8.13 8152KB -WasAd 46.64 7936KB
9 .q **14396.02 **724360KB -WsS0A 25.58 19856KB -WasAd 174.93 19344KB
10 .q **5848.82 **854704KB -WasS0AC 76.69 53504KB -WasAd 603.80 52640KB
11 .q **3635.83 **855280KB -WsS0AC 232.92 151832KB -WasAd 2016.79 149136KB
12 .q **2121.01 **859136KB -WasA 688.91 425664KB -WasAd 6633.99 420768KB
13 .q **1876.78 **874056KB   **14451.92 **202528KB   **14451.92 **202528KB


Token Ring FDDI Protocol

The FDDI (Fiber Distributed Data Interface) is a fiber-optic token ring local area network, described e.g. in [Jain94] or [DT98]. FDDI networks are composed from N symmetric stations, that are organized in a ring.

We use a simplified model of N-ary networks for our benchmarks. One process models the ring, that hands the token in one direction to N symmetric processes, that may hand back the token in a synchronous (high-speed) or asynchronous (low priority) fashion. The ring process owns a local clock and every station owns three local clocks. The timing constants for this model are 0, 20, and 50*N+20, i.e., no delay in the token passing of the ring (td), 20 time units for high-speed communication (SA), and maximally 50*N+20 time for the asynchronous token passing (TRTT).

We verify a (true) safety property stating that the token is not at two places at the same time.

The inputs were generated by this file. The constants were adjusted to coincide with the numbers Farn Wang used as benchmarks for his RED tool.



(For Size > 9, the search for good options was no longer exhaustive).

Size Prop with default option -Was best time best space
2 .q .02 2000KB -WasS0AdC .00 912KB -WsS0d .02 712KB
3 .q .06 912KB -WasS0Ad .01 912KB -WasAC .04 712KB
4 .q .11 2560KB -WasS0Ad .03 912KB -WasS0A .07 712KB
5 .q .26 2632KB -WasS0AdC .03 912KB -WasAd .04 912KB
6 .q .83 2752KB -WasAd .07 912KB -WasS0Ad .09 712KB
7 .q 2.43 3008KB -WasS0AdC .10 1544KB -WasS0AdC .10 1544KB
8 .q 7.55 3584KB -WasS0Ad .15 912KB -WasAdC .16 912KB
9 .q 26.25 4840KB -WasAdC .21 2792KB -WasS2AdC .22 2632KB
10 .q 93.90 7680KB -WasAd .28 2872KB -WasS2Ad .31 2672KB
11 .q 354.71 13960KB -WasAd .40 2968KB -WasS2Ad .41 2696KB
12 .q 1435.25 28456KB -WasS2AdC .50 2736KB -WasS2Ad .53 2736KB
13 .q 5854.38 60000KB -WasS2Ad .66 2768KB -WasS2Ad .66 2768KB
14 .q **14427.13 **130824KB -WasS0Ad .84 3344KB -WasS2Ad .86 2808KB

Philips Audio Protocol

The Philips Audio Control Protocol is a bus protocol, where messages are received by all components on the bus. If a component receives a message not addressed to it, the messages is ignored. There is the possibility of bus collision.

The input file used for the benchmarking uses two senders on the bus. It is essentially what is presented in the CAV96-paper but with sufficiently small clock-drift to make the protocol behave correctly, and converted to a file format understood by the current version of UPPAAL.

For the benchmarks, only one (of several) safety properties is used; (since the property holds, each run corresponds to the complete symbolic expansion of the state space).

A detailed description of the (simplified) model we use is found in [BGK+96].

Size Prop with default option -Was best time best space
philaudio .q .56 3056KB -WasS2AC .47 2984KB -WasS2 .59 2888KB


Bando

File Prop with default option -Was best time best space
bando .q 19.04 21552KB -WasS2AC 16.82 12632KB -WasS2Ad 19.71 12568KB

Bang & Olufsen Collision Detection Protocol

This protocol is applied for the exchange of control information between audio/video units in the company’s product line. By modelling the protocol in Uppaal, a timing error in the protocol was identified by means of Uppaal’s diagnostic trace facility. The error could lead to undiscovered collisions. Following the identification of the error, the company then suggested a correction, which was included in the model and proved correct by using Uppaal. The case study is described in detail in [HSLL97].

The graphical models of the erroneous and the corrected protocol can be seen in bocdp.xml and bocdpFIXED.xml.



Detecing an error in the protocol (violated specification)

Size Prop with default option -Was best time best space
bocdp .q 7.34 9632KB -Wsad .25 2784KB -WsadC .26 2648KB


Model checking the corrected protocol (valid specification)

Size Prop with default option -Was best time best space
bocdpFIXED .q 19.36 21560KB -WsaS2A 16.99 12640KB -WasS2Ad 20.00 12576KB

Bang & Olufsen Power Down Protocol

This protocol controls the transitions between stand-by mode and power on mode in the company’s new series of products, where power consumption minimization is an important feature. The protocol was designed and verified by using Uppaal before the actual implementation work began. The company formulated 15 requirements to the model, and in particular 4 of the requirements was of the form ‘at most 1500 microseconds is allowed to elapse when reaching state B from state A’. It turned out that none of these 4 requirements were true, when interrupts from the devices were allowed to arrive with arbitrary high frequency. The company added a circuit which kept the frequency below 100 microseconds, and the properties were subsequently verified for the corrected model.

In bopdp.xml and bopdpFIXED.xml the models are given for unlimited and limited frequencies respectively. Further details are given in [HLS99].



Detecing an error in the protocol (violated specification)

Size Prop with default option -Was best time best space
bopdp .q 75.55 48128KB -WasAd .40 2944KB -WasS2Ad .44 2856KB


Model checking the corrected protocol (valid specification)
Note that the over-approximation (-A) here is too weak to imply validity; the model checking runs using -A report “MAYBE satisfied”.

Size Prop with default option -Was best time best space
bopdpFIXED .q 996.21 355016KB -WsAa 31.62 10688KB -WsAS2d 40.61 4408KB


Literature

[AL92] Martín Abadi and Leslie Lamport: An Old-Fashioned Recipe for Real Time ACM Transactions on Programming Languages and Systems 16, 5 (September 1994) 1543-1571.
Also appeared as SRC Research Report 91. A preliminary version appeared in Real-Time: Theory in Practice, J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors (1992), Springer-Verlag, 1-27.5 (1) Feb 1987, pages 1-11
URL: http://www.research.compaq.com/SRC/personal/lamport/pubs/pubs.html#lamport-old-fashioned
[BGK+96] Johan Bengtsson and W. O. David Griffioen and Kåre J. Kristoffersen and Kim G. Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi:
Verification of an Audio Protocol with Bus Collision using UPPAAL
in Proceedings of the Eighth International Conference on Computer Aided Verification (CAV), Springer, LNCS 1102, pp244-256, 1996.
Local Copy: audio_protocol_bgkllpw_253Acav96.ps.gz
[DT98] Conrado Daws and Stavros Tripakis:
Model Checking of Real-Time Reachability Properties Using Abstractions
in Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Springer, LNCS 1384, pp313-329, 1998.
[HSLL97] Klaus Havelund and Arne Skou and Kim G. Larsen and Kristian Lund:
Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal
In Proc. of 18th IEEE Real-Time Systems Symposium, pages 2-13, IEEE Computer Society Press, December 1997.
Local copy: havelund97formal.ps.gz
[HLS99] Klaus Havelund, Kim Guldstrand Larsen, and Arne Skou:
Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal
in Proc. of the 5th AMAST Workshop ARTS'99 on Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601, pages 277-298, Springer, 1999.
Local copy: havelund99formal.ps.gz
[Jain94] Raj Jain: FDDI Handbook: High-Speed Networking with Fiber and Other Media,
Addison-Wesley, Reading, MA, April 1994
[Y97] Sergio Yovine: Kronos: A Verification Tool for Real-Time Systems, Springer International Journal of Software Tools for Technology Transfer 1 (1/2) Oct 1997
URL: http://www-verimag.imag.fr/~yovine/pub.html
Local copy: kronos_sttt97.ps.gz