Concurrent Programming (19530-V)

Attention: Please notice that this assignment is due on Thursday again; the solution to Übung 9 will be posted to the class Web page on 25.1.2002 for you to use on this assignment. This is the last assignment for the class.

1. Exercise

Using the provided solution for Übung 9, define a progress property that asserts that at least one robot can move in at least one direction infinitely often. Use LTSA to analyze the model; did you find any progress violations? If so, describe the scenario in which the violation occurs and how you could fix the problem.

2. Exercise

Using the provided solution for Übung 9, define a safety property that asserts that a single cell is never occupied twice. Use LTSA to analyze the model; did you find any safety violations? If so, describe the scenario in which the violation occurs and how you could fix the problem.

Hint: The safety property is a little bit more difficult to create than the progress property; review the Model-based Design lecture where we discussed how to "compose" safety properties in your models. You will most likely need to modify the model slightly.