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:

 

Contact: jim@cs.york.ac.uk

Last updated: 6th December 2007