Back to Verification Homepage


     This page contains helpful information on the tools used in Kim G. Larsens course Verification'00
It will grow and change according to your comments.

  Concurrency Workbench (CWB)   Iben   Spin   Uppaal


Please notice the modified homework for the Uppaal exercises.
Deadline for handing in: 29 May 2000, 10:00am

    There are two main development branches, the Edinburgh Concurrency Workbench and the North Carolina one (located at Stony Brook). We use the former one, version 7.1.
installed at: harald:/users/btools/CWB-7.1
documentation: manual (postscript)
Web Pages
Colin Stirling: Bisimulation, Model Checking and other Games

Look here! PDF slides from a CoW Tooltalk (18/05/2000)
suggested usage: use Emacs and daVinci.
You can go here for a detailed description.
examples: The homework (Mutex Algorithms)
   Ex23) Dekker
   Ex24) Dijkstra
   Ex25) Peterson

    Iben is an command-line based interface to a (RO)BDD package. It allows basic manipulation and substitution. The variable ordering is fixed by the order of declaration.
A very nice feature is the possibility to display the constructed BDDs as postscript.

The interface is written by Gerd Behrmann (Aalborg) and connects by default to Jørn Lind-Nielsen's BUDDY BDD package.
installed at: harald:/users/btools/IBEN

If you feel like, you can download and install it yourself from
In order to use the viewer, you additionally need the drawing program dot.
A gzip'ed Solaris executable is available.
documentation: README file
suggested usage: Login on harald or gorm.
Include the directory /users/btools/IBEN/bin/ in your $PATH
e.g. in bash shell via
      bash$ export PATH=$PATH:/users/btools/IBEN/bin
Start Iben now with
$bash  iben
Even better, use a *shell* buffer within Emacs (M-x shell).
Then you can directly save your session and have some extra editing options,
like e.g. M-s REGEXP to fetch an older matching input line.
examples: short sample session

    Spin is a LTL model checking tool, specifically designed for analyzing the logical consistency of asynchronous systems. Systems are modelled in a guarded command language called Promela.

Spin is written in C, but has a nice TCL/TK frontend.
installed at: harald:/users/omoeller/src/Spin3.3/Xspin3.3

there is a slightly older version at
documentation: Spin Homepage
Online Manual (HTML)
Exposition The Spin Model Checker. IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295
suggested usage: run Spin with TCL/TK frontend:
$bash  /users/omoeller/src/Spin3.3/Xspin3.3/xspin3310.tcl &
use your facourite editor to write the Promela input.

    UPPAAL is an integrated tool environment for modeling, validation and verification of real-time system.
If comes with a graphical user inface written in Java.
On the algorithmic side, it runs basically state space exploration via an efficient C/C++ engine.
installed at: harald: /users/omoeller/src/Uppaal

You can download the newest Uppaal version here.
There is an older version installed on harald: /users/btools/UPPAAL
Regretfully, this does not support local variables.
documentation: Uppaaal Homepage
Comprehensive Article from Larsen, Pettersson, Yi: Uppaal in a Nutshell (ps)
suggested usage: use a text editor to write your specification
(have a look at the example NAME.xta files to see how to do it);
then run Uppaal on harald with Java GUI:
$bash  /users/omoeller/src/Uppaal/uppaal2k
It generates a default .NAME.ugi file, you can modify the graphical layout lateron.
Have a look at the graphic representation to catch flaws early.

If it is veeeeery slow....

You can try this modified scipt: uppaal2k.
It calls the java1.3 version, which has a different (better?) implementation of the Java swing classes. Dependent on your machine, it might run faster.


  • on rare occasions, Uppaal corrupts input files. Keep backups!
  • monitor your Uppaal process; be prepared to kill -9 it, if the GUI freezes.

examples: You'll need all three files for each example. Load the .xta file into Uppaal.
Fischer's Mutex Algorithm fischer.xta .fischer.ugi fischer.q
The Soldiers' Problem soldiers.xta .soldiers.ugi soldiers.q
A running engine engine.xta .engine.ugi engine.q
NOTE: If you use newer Uppaal versions, download the .NAME.ugi files as NAME.ugi

homework: Model and analyse the following gossiping girls problem in UPPAAL. A
number of girls initially know one distinct secret each. Each girl
has access to a phone which can be used to call another girl to
share their secrets. Each time two girls talk to each other they
always exchange all secrets with each other (thus after the phone
call they both know all secrets they knew together before the phone
call). Only binary (between two girls in each phone call) is

Task 1: Use UPPAAL to find the minimal number of phone calls needed for
five girls to know all secrets.

Task 2: Find an (inductive) argument for how many phone calls
are needed to solve the gossiping girls problem for n >= 5 girls.

HINT#1: First find a good upper bound (that holds for n >= 4).
Then assume you can do better for some minimal n and
construct a way to do better for n-1 (contradiction).
HINT#2: One (but not the only) way to solve this problem is to use the
following fact: (if you want, you can also prove it)
If there is a m >= 4 for which you can do better, then
in this communication scheme no girl A calls a girl B that knows
A's secret.

Task 3: Refine your model so that each phone call requires 30 time
units to connect and additional 60 time units to complete the
transfer of one secret. Arbitrary many secrets can be exchanged
while the connection is alive. Disconnection does not take time.
Every girl can only use one phone at a time.
Find the minimum time needed to solve the gossiping girls
problem for five girls.

Back to Verification Homepage Back to top of this page   Oliver Möller - Last modified: Tue May 1 16:41:53 2001