VVS: model checking
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
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
For formalising the problem, you must create two
processes, P and P and the corresponding variables
light and light. 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
The deadline for delivery is Friday, May 11th, 2018