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">

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).

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).

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).

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

Bando

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)

Model checking the corrected protocol (valid specification)

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)

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”.

Literature