Model-Checking Kit

university

sitemap

contact

legal notice

University of Stuttgart

	Institute of Formal Methods in Computer Science
	Model-Checking Kit: How to install the Kit

The Kit is made up from many parts - a number of model-checking tools and our program that glues them all together. We have tried to make the installation of the Kit as easy as possible; yet the diversity of the tools may introduce a few complications from time to time.

Download the binaries

The binary package contains everything you need to use the Kit. It contains precompiled versions of all the tools (except for Spin, see below). Currently, we are offering versions for Solaris and for Linux:

Binaries for Linux (current version 1.4.0)
Binaries for Solaris (old version 1.3.1)
Binaries for Linux (old version 1.2.0, for gcc versions prior to 3.2)

Download Spin

The authors of Spin allow the use of their program within the Kit but request that its installation be kept separate. You can find pointers to Spin downloads here.

In order to use Spin with the Kit you need to copy the spin executable into the mckit/tools directory. You will need to install Spin in order to use the spin-ltl and pep-ltl algorithms.

Installation

Having downloaded the binary package, do the following to install it:

Extract the package to a directory of your choice. For the purpose of these instructions, we shall assume that the Kit will be installed under /usr/local, but any directory will do. Thus, depending on your operating system, type one of these lines:
```
  gtar xfvz mckit-bin_solaris-040324.tar.gz
  gtar xfvz mckit-bin_linux-040324.tar.gz
```
This will create a directory called mckit in which all the files will be placed. Make sure that mckit and all its subdirectories are made readable and executable for the intended group of users.
Add the mckit/bin directory to your PATH variable. E.g. if you're using csh, you would type
```
  setenv PATH /usr/local/mckit/bin:${PATH}
```
Under bash, type
```
  export PATH=/usr/local/mckit/bin:${PATH}
```
That's it. You may want to test your installation by running the test script supplied with the Kit:
```
  cd /usr/local/mckit/examples
  perl test.pl
```
If all tests succeed, you are all set up to use the Kit. Please refer to the next section to see a guided sample session.

Download the sources

Below, you can download the source code of the Kit. Availability of the source for the diverse model-checking tools varies - please refer to the tools' homepages if you want to obtain them. You will need to have the binary package, too, if you want to do anything useful with the sources.

Download the source code for the current version 1.4.0 here.
Extract it into your mckit directory. The source files will be placed in a sub-directory called mckit/src.
Read the files README and Makefile for instructions how to compile etc. If you want to add other languages or algorithms, please read the chapter Extending the Kit in this documentation.

Download the documentation

You can download a copy of this web-based documentation here if you prefer to read these pages offline. Extracting this archive will create a directory mckit/web containing all the documentation; the entry page is at mckit/web/index.shtml.

Next chapter: A sample session