Spécification des Systèmes Complexes (SDSC)

(last update: Fri Nov 27 19:28:25 CET 2015)

1   This course


2   SPIN

If you want to install SPIN at home, you can download precompiled binaries for various operating systems. Remember that you can always ssh -X to the computers in room F204.

3   Installing SPIN

  1. In a Debian session, open a terminal.

  2. Create a folder in your home directory where you will install SPIN, for instance ~/bin:

    mkdir ~/bin
  3. Add that folder to your $PATH variable. For instance, add the following line to your ~/.bashrc file:

    export PATH=$PATH:$HOME/bin
  1. Download to ~/bin the SPIN tool and its graphical interface:

    cd ~/bin/
    wget 'http://spinroot.com/spin/Bin/spin644_linux32.gz'
    wget 'http://spinroot.com/spin/Src/ispin.tcl'
    gunzip spin644_linux32.gz
    ln -s spin644_linux32 spin
    chmod 755 spin644_linux32
    chmod 755 ispin.tcl

SPIN is now installed in your machine. On the terminal:

4   Fixing the Installation in the F204-xx Machines

4.1   Fixing the Installation

The SPIN release that you have previously installed is a 32 bits program. Machines in the room F204 are 64 bits. To use SPIN from the graphical interface ispin.tcl we need to use a modified version of the ispin.tcl program. Download it and install it as follows:

cd ~/bin
wget https://lipn.univ-paris13.fr/~rodriguez/teach/sdsc/2015-16/files/ispin-F204.tcl
chmod 755 ispin-F204.tcl

From now, instead of using ispin.tcl, use ispin-F204.tcl.

NOTE: Currently, SPIN only works in the F204 machines. If you are physically using a machine in another room, F205, F206... use ssh -X to remotely execute spin and ispin-F204-tcl in some machine of the room F204. For instance, we execute SPIN on the machine F204-1 while being physically logged on machine F206-3:

user@F206-3:~$ ssh -X F204-1
user@f204-1's password:
Linux F204-1 3.2.0-4-amd64 #1 SMP Debian 3.2.68-1+deb7u6 x86_64
user@F204-1:~$ spin
Spin Version 6.4.4 -- 1 November 2015
spin: error, no filename specified
user@F204-1:~$ ispin-F204.tcl

4.2   SPIN in Simulation Mode

Nothing changes.

4.3   SPIN in Verification Mode

Use the following commands instead of the ones given in the slides (the only difference is the -m32):

spin -a programme.pml
gcc -m32 pan.c -o pan
./pan -E
spin -t programme.pml

5   First Steps with SPIN and Promela

6   Model Checking, LTL

7   Homework