**This is an old revision of the document!**

Objectives:

• Estimate state space size in PROMELA verification models that use message passing
• Explore SPINS search and state compression techniques
• Write verification models in PROMELA that use message passing.

Problems

1. (10 points) Answer problems 1(f) through 1(k) from the SPIN Verification Examples and Exercises

2. (30 points) Answer problems 2(a) through 2(b) from the SPIN Verification Examples and Exercises. Note that the PROMELA code does not include all the transitions in the figure and it is missing transitions as well. Part of your answer should modify the PROMELA to match the diagrams. Also, for the second part, b, modify the PROMELA in S1 for both terminal A and terminal B.

3. (20 points) This problem comes from CalTech's CS 118 Assignment 4. Consider a distributed system that consists of five producers, one scheduler, and two consumers. Each producer has two tasks that need to be completed by a consumer. For each task, a producer sends a request to the scheduler. The scheduler has a queue to store up to five incoming producer requests. The scheduler, upon receiving a request, assigns the task to one of the consumers. The two consumers have their own separate queue of outstanding tasks. A consumer can only service one request at a time, but it can have up to two outstanding tasks waiting in the queue. Consumers do not acknowledge completion of tasks.

The definitions for prototypes Producer, Consumer, and init are provided below. Write the definition for prototype Scheduler for assigning tasks to the consumers. The scheduler is constrained by the following property when assigning tasks: it must balance the workloads of the two consumers. That is, a new task is always assigned to the consumer who has the fewest number of outstanding tasks in its queue. If the number of tasks currently assigned is equal, then the task could be assigned to either consumer. Prove with SPIN that your solution has the right properties.

mtype = { task }
chan prodToSched = [5] of {mtype, byte}
chan schedToCons[2] = [10] of {mtype, byte}

proctype Producer(byte me) {
}

proctype Consumer(byte me) {
byte you
do
:: timeout -> break
od
}

init {
byte i
atomic {
for (i : 0 .. 4) {
run Producer(i)
}
run Consumer(0)
run Consumer(1)
}
}

active proctype Scheduler () {
/* you write this */
}

4. (50 points) Write a PROMELA verification model for Dikstra's Token Termination Algorithm (another presentation) and use SPIN to prove that the verification model is correct. Make the verification model be parameterized by N the number of nodes participating in the system.