Exercises

• 14.1 Using FLTL, specify and check the exclusion safety properties for neighbors in the Dining Philosophers problem of Chapter 6. In addition, specify and check the liveness properties, including the response property that ensures that if a philosopher is hungry, he will eventually eat. Use witnesses to provide examples of property satisfaction.

• 14.2 Using FLTL, specify safety and liveness properties for the Readers – Writers problem of section 7.5. Check that these give the same results as the corresponding properties specified in Chapter 7 and for the same properties used in the verification models of Chapter 13.

• 14.3 Using FLTL, specify and check the exclusion safety properties for the warring neighbors of exercise 7.6, and for Peterson’s Algorithm for two processes of exercise 7.7. In addition, specify and check the liveness properties, including the response property that ensures that if a neighbor wants to enter the field, he will eventually gain exclusive access. Use witnesses to provide examples of property satisfaction.

• 14.4 Using FLTL, specify safety and liveness properties for the cruise control system of Chapter 8. Check these properties against the model of Chapter 8. (Hint: define fluents for each of the abstract states – active, cruising, enabled, etc. – as necessary.)

• 14.5 Using FLTL, specify a safety property to replace the property SAFE specified in section 11.3.1 for the Announcer – Listener system. (Hint: define a fluent which holds when a process registers for a pattern and note that a separate SAFE process is created in Chapter 11 for each listener process.)