IA169: Model Checking
Seminar 2
Exercise 1 A two-bit counter is a system with two atomic propositions
(b1, b0) that represent two bits of a single binary number. The initial state of
the system is ¬b1, ¬b0 and its computation proceeds like this
1. ¬b0, ¬b1 (i.e. 00)
2. ¬b0, b1 (i.e. 01)
3. b0, ¬b1 (i.e. 10)
4. b0, b1 (i.e. 11)
5. ¬b0, ¬b1 (i.e. 00)
6. . . .
Model the system in the smv language and use nuXmv to simulate it.
Then come up with some true and some false properties of the system and
use nuXmv to check them.
Exercise 2 Recall the aquarium with Alice and Bob from the previous
seminar. Model the system in the smv language and use nuXmv to check
the given ltl properties.
Exercise 3 Recall the mutual exclusion protocol from the lecture:
cobegin P0 ∥ P1 coend
P0:: l0: while true do
NC0: wait (turn = 0);
CR0: turn := 1
end while
P1:: l1: while true do
NC1: wait (turn = 1);
CR1: turn := 0
end while
and its state space diagram
ia169: model checking 2
turn = 0
⊥, ⊥
turn = 0
l0, l1
turn = 0
l0, NC1
turn = 0
NC0, l1
turn = 0
NC0, NC1
turn = 0
CR0, l1
turn = 0
CR0, NC1
turn = 1
⊥, ⊥
turn = 1
l0, l1
turn = 1
l0, NC1
turn = 1
NC0, l1
turn = 1
l0, CR1
turn = 1
NC0, NC1
turn = 1
NC0, CR1
Model the system in the smv language and use nuXmv to check the ltl
properties:
• G¬(CR0 ∧ CR1)
• GF(turn = 0) ∧ GF(turn = 1)
Exercise 4 Add reasonable fairness constraints to the previous system and
check the ltl properties again.