GC6: Dependable Systems Evolution

Home
Mondex
Flash
Pacemaker

Pilot Projects

What makes a good pilot project?

Joshi and Holzmann proposed that a pilot project should have the following properties (see their VSTTE paper).  It should be of sufficient

• Complexity:  that traditional methods, such as testing and code reviews, are inadequate to establish its correctness.

• Simplicity:  that specification, design and verification could be completed by a dedicated team in a relatively short time, say 2–3 years.

• Importance:  that successful completion would have an impact beyond the verification community.

Grand Challenge pilot projects

The first pilot project was the mechanisation of the proof of correctness of the Mondex smart-card protocol for exchanging value.  The second pilot project is the verification of a POSIX-compliant flash memory filestore.  Other pilot projects are being planned, and they include:

• Formalising the Apache web-server.

• Verified electronic voting.

• Pacemaker formalisation challenge.

Contact: jim@cs.york.ac.uk

Last updated: 6th December 2007