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