Patrick Tullmann, 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 class 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 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. (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.

patrick tullmann
Last updated on Wednesday, November 03, 2010