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|
HomeworkPlease 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.|
Colin Stirling: Bisimulation, Model Checking and other Games
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)|
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.
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.
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 ibenEven 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
Spin is written in C, but has a nice TCL/TK frontend.
there is a slightly older version at
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.
Comprehensive Article from Larsen, Pettersson, Yi: Uppaal in a Nutshell (ps)
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/uppaal2kIt 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.
|examples:||You'll need all three files for each
example. Load the .xta
file into Uppaal.|
Model and analyse the following gossiping girls problem in
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
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.
|Oliver Möller - Last modified: Tue May 1 16:41:53 2001|