Objectives:

  • Predict the size of a state space in a PROMELA verification model
  • Write simple PROMELA verification models that use shared variables for synchronization
  • Use PROMELA to find solutions to brain-teasers

Problems

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

2. (30 points) Model the following mutual exclusion algorithm with PROMELA (25 points) and prove its correctness or incorrectness with SPIN (5 points).

Hyman's Mutual Exclusion

void lock (int i) {
      int j = 1 - i;
      signal[i] = 1;
      while (turn != i) {
         while (signal[j]);
         turn = i;
      }
 }
 
void unlock(int i) {
   signal[i] = 0;
}

3. (30 points) Write a Promela model for the below problem (25 point) and use SPIN to find a solution (5 points).

A farmer wants to cross a river and take with him a wolf, a goat, and a cabbage. There is a boat that can fit himself plus either the wolf, the goat, or the cabbage. If the wolf and the goat are alone on one shore, the wolf will eat the goat. If the goat and the cabbage are alone on the shore, the goat will eat the cabbage. How can the farmer bring the wolf, the goat, and the cabbage across the river?

cs-486/spin-homework-1.txt · Last modified: 2020/01/06 18:41 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0