Our goal was to develop a model of Fluke's IPC mechanism in Promela and verify freedom from deadlock, avoidance of livelock, and other features with SPIN.
Our paper, published in the proceedings of HotOS-VI is now available from the Flux paper server (Full paper, gzip'd postscript) (Abstract, html). Our class project report in postscript, is also available.
A tarball (122K) of our sources (including
the HotOS paper,
So far, three presentations on this project have been given. One is a short 15 minute overview. (PowerPoint, HTML) The second is a longer 1 hour review. (PowerPoint, HTML) The third is the HotOS presentation (10 minutes plus some backup slides.) (PowerPoint, HTML)
In the process of using SPIN to model our system, we developed several tools. (Well, tools is a strong word, perhaps hacks is a better word.) For more information on Fluke, see the Flux Project home page.
For more information on SPIN, see the NetLib SPIN archive.