Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo 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:

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.


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
  • 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