1   This course

Instructors:

• Main instructor: Christine Choppy
• Practicals: César Rodríguez

2   SPIN

• SPIN home page: http://spinroot.com/spin/whatispin.html
• Promela grammar: http://spinroot.com/spin/Man/grammar.html
• Promela language reference: http://spinroot.com/spin/Man/promela.html

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

To install SPIN in a Debian machine, following these steps:

1. 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. Add the following line to your ~/.bashrc file:

   export PATH=$PATH:$HOME/bin
   

4. Close the terminal and open a new terminal. Make sure that $HOME/bin is in your path.

5. Download to ~/bin the SPIN tool and its graphical interface:

   cd ~/bin/
   wget 'https://lipn.univ-paris13.fr/~rodriguez/teach/sdsc/2016-17/files/spin645_linux64'
   wget 'https://lipn.univ-paris13.fr/~rodriguez/teach/sdsc/2016-17/files/ispin.tcl'
   chmod 755 spin645_linux64
   chmod 755 ispin.tcl
   ln -s spin645_linux64 spin
   

6. You will also need the graphviz package. This is already installed in the machines of our University. If you are installing SPIN in your computer, type:

   sudo apt-get install graphviz
   

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

• type spin to execute the SPIN tool,
• type ispin.tcl to use SPIN's graphical interface.

Make that typing spin executes the program $HOME/bin/spin. You can check this by typing type spin on the terminal, which should replay something like:

spin est haché (/export/home/use[...]/cesar/bin/spin)

4   First Steps with SPIN and Promela

• Slides and exercises.

5   Model Checking, LTL

• Slides and exercises.

• Slides and exercises.

• Here you have a Makefile for automating the commands to use spin. Before using it, you need to modify the variable T (for target) in the makefile to point to your Promela file, for instance test.pml:

  T=test.pml
  

  After that, use the following:

  • make sim (or make without arguments): SPIN in simulation mode
  • make ver: SPIN in verification mode
  • make rep: it will replay the counterexample found in verification mode
  • make pdf: generate a PDF file depicting the automata associated to each proctype

  NOTE: make ver calls pan with option -a, which makes SPIN check for LTL properties but disables the verification of assertions. Remove the -a in the Makefile to check for assertions.

6   Homework

• Deadline: 11.55pm on Friday December 9, 2016 (one week later than what we originally agreed)
• Available here.