Formal Methods at Work
GSSI, November 2018

Welcome

The main aim of this ten-hour course is to give you hands-on experience in applying formal methods to the modelling and analysis of problems. During the course, I plan to do very little lecturing. Since what we learn we learn by doing, during most of the course sessions, you will be working in groups of two on modelling and analysis problems using the model checker UPPAAL, which is the foremost tool suite for the automatic verification of real-time systems. (The prime architects behind Uppaal have received the CAV Award 2013.

Each group can solve the given problems at its own speed. At the end of the course, each group will deliver a report describing its solution to the problem posed in the project description presented below.

At the end of the day, I hope that you will have a lot of fun in working on these problems and using Uppaal to solve them!

Recommended literature

Other recommended resources

If you want to see a proof of the fact that solving the gossiping-girls problem requires 2n-4 calls when the number of girls is n>=4, see the paper
C.A.J. Hurkens. Spreading gossip efficiently. Nieuw Archief voor Wiskunde, 5/1(2):208-210. June 2000.

Problems

More problems will be added in due course, also depending on how quick you are at solving them.

  1. How much can we lose?
  2. How much can we reach?
  3. Model the one- and two-dimensional solitaire games described here using Uppaal, check that the game can indeed be solved and find the shortest solution.
  4. Modelling of classic and real-time mutual exclusion algorithms.
  5. Coffee machine.
  6. The Little Book of Semaphores by Allen B. Downey is a treasure trove of modelling and verification exercises you might want to try. I will point out some interesting ones to those who might be interested.

Project

The project for the course is described in this PDF file.