Introduction to Model-Checking; Theory and Practice


Handouts

  1. Introduction  

  2. Petri nets  

  3. Model-Checking Linear Time Properties  


Exercises

  1. Modeling with automata  

  2. Modeling with P/T nets: introduction  

  3. Modeling with P/T nets: a longer example using asynchronous message-passing and composition  

  4. Modeling with P/T nets: parameterized systems  

  5. Model-Checking LTL  


Practical work

The course lectures and the practical works rely on Tina, a model-checking toolbox for Petri nets and their extensions. Most of the work requires the use of nd (NetDraw); an editor and GUI for Petri nets and Automata.

  Download TINA.

Installation

Simply download the right executable for your OS, unpack it, and put it in a place where it can be found by your shell (this may include updating your PATH variables).

  On windows machine, make sure to avoid installing the software on a directory that contains white-spaces or unicode characters (always a sensible thing to do with Windows).

  On mac, slide application nd.app into the Applications folder; the binaries are found in nd.app/Contents/MacOS/bin. On versions of MacOS with GateKeeper enabled (10.8,9,…), GateKeeper will prevent installing tina and pretend that the application is damaged. It is not; it is simply that tina is not signed by a registered Apple developper.

On such systems, tina can be installed as follows:

  1. remove any installed version of tina

  2. disable GateKeeper in System Preferences

    • On 10.10 for instance, this is done by: System Preferences > Security & Privacy > General > Allow apps downloaded from: > Anywhere

    • On 10.12 (Sierra), you need first to make “Anywhere” appear again by typing the following line in a terminal: sudo spctl --master-disable

  3. download a suitable version of tina

  4. install tina and launch it

  5. re-enable GateKeeper