This is a project completed for Ganesh Gopalakrishnan's CS 611 course offered in the Fall of 1996, here at the U of U.
Patrick Tulmann, John McCorquodale, Ajay Chitturi, Godmar Back, and Jeff Turner worked on it real hard.
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 project report in postscript, is also available.
A tarball (122K) of our sources (including
the HotOS paper,
.tex source to all our documentation, and project
reports) is also available.
This has some good generic stuff
that might be good for other SPIN verification efforts. But, much of it won't make
any sense without access to the Fluke source (latest estimate is late
two months from any given day).
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. (Color Postscript, B&W Postscript, PowerPoint, HTML) The third is the HotOS presentataion (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.)
spin -adump and reformats it. It looks more like the Xspin trace after processing.
For more information on SPIN, see the NetLib SPIN archive.