CIS720 – Fall 2012

Homework Assignment 1: Verify Peterson’s algorithm for mutual exclusion.

Due: August 30, 2012 – Uploaded to online.ksu.edu by 1PM

You are to use Promela and SPIN to verify that Peterson’s solution to the mutual exclusion problem is correct.

1. Document the global invariant you are verifying (mutual exclusion). Describe how it is implemented in Promela.

2. Upload both the code (with comments), and the results of the verification run.