VVS: model checking

Traffic Lights


We want to model the following problem in Promela and verify some properties about the system. We have a simple road intersection with two directions, we will call horizontal and vertical, and a pair of traffic lights per each direction, as shown in this picture:


We will only model one traffic light per each direction (the second one just repeats the same behaviour). For instance, in the picture above, the vertical light is green and the horizontal one is red. Initially, both directions are red. When a car arrives, it is detected by a sensor and its corresponding light turns to green. However, this only happens if the other direction is still in red; otherwise, it will wait until the other direction is closed. Once any direction is in green, it will turn next to orange (there is a timer, but we will not model the delay) and then it will turn to red again.

What to do

Using the initial marking depicted above:
  • Formalise the problem in Promela
  • Deadlock: check that your encoding does not generate a deadlock
  • Safety: check that a situation in which both traffic lights are not red is not reachable. Explain the obtained result.
  • Liveness: check whether both traffic lights can reach each color infinitely often. Explain the obtained result.
For formalising the problem, you must create two processes, P[0] and P[1] and the corresponding variables light[0] and light[1]. Each process P[i] will contain an infinite loop where light[i] makes the cyclic changes green -> orange -> red, but waiting when needed. You will have to model some kind of synchronisation to avoid situations in which both directions are open (i.e. they are not in red at the same time).

Assessment & delivery

The maximum grade for this exercise is 2 points. Use the MOODLE platform to upload your work as a single .zip file containing all the files with pml code and explanations. Exercises can be made by two students at most. If so, the students' names must be included in the first lines of each file and only one of the students needs to upload the files to his MOODLE account.

The deadline for delivery is Friday,  May 11th,  2018 (23:59).