Back to Verification Homepage

VERIFICATION TOOLS @Århus

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

Please note the supplemenatary reading material.

  Iben   NuSMV   Spin   Uppaal



Iben:
    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$ 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

NuSMV:
    NuSMV is a symbolic CTL model checker developed as a joint project between the Formal Methods group in the Automated Reasoning System division at ITC-IRST and the Model Checking group at CMU (the origin of SMV).
NuSMV provides a command-line interface to input model files and receive results of the verifications (i.e., "TRUE" or an error trace).
The implementation relies on Multi-terminal Decision Diagrams (MDDs, based on Colorado University Decision Diagram package CUDD), but this is mainly invisible to the user. One of the interesting features is the possibility to declare state-based fairness.
installed at: harald:/users/omoeller/bin/sparc/NuSMV

documentation: NuSMV Homepage
User Manual
suggested usage: Login on harald or gorm.
Then put the directory /users/omoeller/bin/sparc in your $PATH,
and include the directory /users/omoeller/src/NuSMV/lib in your $LD_LIBRARY_PATH, e.g. via bash shell

  bash$ export PATH=/users/omoeller/bin/sparc:$PATH
  bash$ export LD_LIBRARY_PATH=/users/omoeller/src/NuSMV/lib:$LD_LIBRARY_PATH

You should be able to start NuSMV now via

  bash$ NuSMV <model-file>

Even better, use a *shell* buffer within Emacs (M-x shell).
examples: Alternating bit protocol (4 bits)
download abp4.smv and abp4.ord, then start NuSMV with

  bash$ NuSMV -i abp4.ord abp4.smv

The file abp4.ord defines the order, in which the variables of the processes are constructed. This file is an optional optimization -
in this particular example, the order abp4.ord is about two times faster than the default one.
More details can be found in abp4.smv.


Find other examples here.

Spin:
    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)
PROMELA Description (Process or Protocol Meta Language)
Journal Paper 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: A Leader Election Protocol:
use the promela input leader.pro
to verify the LTL formula <>[]oneLeader, which should result in the test automaton leader.ltl

A detailled tour is given here.

Uppaal:
    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/uppaal-3.1.58

You can also download the newest Uppaal version here.
documentation: Uppaal Homepage
Comprehensive Article from Larsen, Pettersson, Yi: Uppaal in a Nutshell (ps)
suggested usage: run the Uppaal engine on harald and the Java GUI locally, i.e., log in on harald and type in one shell:

harald:bash$ ~omoeller/src/Uppaal/uppaal-3.1.58/bin-SunOS/socketserver

Then, in a shell of your local machine, make sure that you use java 1.3 (try which java - this should give you the version)
If this points to an older version, set $JAVAHOME appropriately and update your $PATH. Then start the gui:

local:bash$ ~omoeller/src/Uppaal/uppaal-3.1.58/uppaal2k

Use the XML format to save your files.
Have a look at simulator runs, in order to catch flaws early.

Caveats:

  • Keep backups!
  • monitor your Uppaal socketserver process on harald (e.g. by top);
    be prepared to kill -9 it, if it exceeds say 300MB

examples: You'll need all three files for each example. Load the .xml file into Uppaal.
Fischer's Mutex Algorithm fischer.xml fischer.q
The Soldiers' Problem soldiers.xml soldiers.q
A running engine engine.xml engine.q


homework: [ see Kim's assignment ]

Exercises 2 and 3 are to be handed in, but it is strongly suggested that you go through Exercise 1 as a warm-up.
You are of course welcome to work on the optional Exercises 4/5; Oliver can be of assistance here in week 26 (25-30 June).
hand-in: email and v01-box in office R3-334, better soon than later


Back to Verification Homepage Back to top of this page   Oliver Möller - Last modified: Fri Jun 1 10:00:08 2001