|
|
|
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 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 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 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 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:
|
|||||||||
| examples: | You'll need all three files for each
example. Load the .xml
file into Uppaal.
| |||||||||
| 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 |
|
|
 |
Oliver Möller - Last modified: Fri Jun 1 10:00:08 2001 |