Note: Only introduce global variables to verify a property when remoterefs simply are not adequate.

1. (20 points) Consider again the elevator model from Homework 3 Problem 2. Re-verify each property using never claims. There should be one never claim for each of the four properties. As before, indicate if a property is a safety or liveness property. Modify your model as needed so each property passes.

2. (20 points) Consider again Homework 3 Problem 3. Re-verify each property using never claims. Be sure to indicate which properties are liveness. Verify the additional property that if a process request access to the inner sanctum, then it eventually reaches the inner sanctum.

3. (15 points) Consider again Homework 3 Problem 4. Re-verify each of the properties using never claims.

4. (20 points) Consider again Homework 2 Problem 4 to model Dijkstra's Token Termination algorithm. Verify the following properties using never claims on your model. Modify the model as needed so the algorithm passes verification. Check each property for several number of nodes N and messages M.

• A process when black eventually becomes white
• A process only turns black if it receives a message or sends a message to a process with a smaller ID
• A process receiving a token eventually sends out the token
• The system only terminates when there are no outstanding messages

5. (20 points) Explain the difference between the accept and progress labels. Write a PROMELA verification model to illustrate the difference and show the output from SPIN.