|
|
|
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. |
| installed at: | harald:/users/btools/CWB-7.1 |
| documentation: |
manual
(postscript) Web Pages 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) 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 http://www.cs.auc.dk/~behrmann/iben/. 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 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
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 harald:/users/btools/SPIN/Xspin3.2 |
| 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. |
| examples: |
|
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/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. Caveats:
|
||||||||||||
| examples: | You'll need all three files for each
example. Load the .xta
file into Uppaal.
| ||||||||||||
| 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 possible. 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. |
|
|
 |
Oliver Möller - Last modified: Tue May 1 16:41:53 2001 |