2. Specification using Linear Time Temporal Logic
Consider three processes 1, 2, and 3 processing synchronously. Each controls a variable x1, x2 and x3 respectively. Initially x1 and x2 and x3 are all true. Each process has the following behaviour. •
Process 1 sets the value of x1 in the next moment to be true if both x2 and x3 are true (now), otherwise it sets x1 to be false. •
Process 2 sets the value of x2 in the next moment to be true if either x1 or x3 are true (now), otherwise it sets x2 to be false. •
Process 3 sets the value of x3 in the next moment to be true if both x1 and x2 are false (now), otherwise it sets x3 to be false.
(a) Draw the transition system for the combined system. Make sure you draw all logically possible states (one for each possible value of x1, x2 and x3, including possibly unreachable ones).
(b) Write LTL formulae to specify the initial conditions and the three processes.
(c) Suggest one non-trivial safety property and one non-trivial liveness property which hold for the above transition system.
3. Synchronous LTL Logic Model Checking
(a) Write a NuSMV input file describing the system described in question 2. [Hint: this is similar to a system described in lecture 9.]
(b) Add to the NuSMV input file the properties mentioned in question 2 and run NuSMV to make sure the properties do hold.
(c) The property ♦(x1 ∧ x2 ∧ x3) should not hold for this system. Rewrite this property in the correct syntax for NuSMV. Add to the input file and run it. Using the output from NuSMV construct a counter model and draw this.
(d) Suggest another property that will not hold for this system. Repeat part (3c) using this property.
4. Asynchronous LTL Model Checking
Now again consider the system described in question 2 but assume it is asynchronous
(a) Draw the transition system representing the asynchronous system. [Hint: the states will be the same as for the synchronous version but the transitions will change. Also you need to consider which process’s turn it is to move. To do this give labels to the transitions indicating which process is responsible for that transition.]
(b) Write a new version of the NuSMV input file which is now asynchronous. Also specify the fairness constraint that each process gets a turn to go infinitely often. Add the two properties from question 3(b) and run NuSMV.
(c) Find a property (different from the ones you have already mentioned) that is true for the synchronous system and not for the asynchronous system with fairness (or vice versa). Run NuSMV with this property for each input file. Draw the path for the property that fails.