Mondex case study

Mondex case study

We have set up a short project to help get the grand challenge off the ground and to populate the Verified Software Repository. A number of research groups are working on the same problem in parallel. We chose as our problem the Mondex smart card work, which was originally specified and refined in Z, and proved correct by hand. The Mondex project is now ten years old, and we want to see what the current state of the art is in mechanising the specification, refinement, and proof.

Ideally, we'd like to aim for full automation. We will ask the following questions at the end of the project:

• How far did each group get?
• What did one group achieve that the others couldn't?
• How can we combine the best of each approach?

We want to help to set the research agenda in this area for the next ten to fifteen years, and we want to generate lots of artefacts for the verified software repository that we're setting up.

The following groups have committed to working on the project.

1. Daniel Jackson (MIT) Alloy ":http://people.csail.mit.edu/dnj/".
2. Michael Butler (Southampton) B ":http://www.ecs.soton.ac.uk/~mjb/".
3. Cliff Jones (Newcastle) VDM ":http://www.cs.ncl.ac.uk/people/home.php?name=cliff.jones".
4. Martin Gogolla (Bremen) OCL ":http://www.db.informatik.uni-bremen.de/~gogolla/".
5. Jim Woodcock (York) Z ":http://www.cs.york.ac.uk/people/bio.php?person=jim".
6. Chris George (Macau) Raise ":http://www.iist.unu.edu/~cwg/".
7. David Crocker (Escher) Perfect Developer ":http://www.eschertech.com/company/dc_homepage.php".

We completed a small version of the project recently (with John Fitzgerald and Peter Gorm Larsen doing the VDM work). This was very successful, and led to some interesting results. It's an existence proof that we can work together effectively and that there's some purpose to the work.

We are working with existing resources over the calendar year 2006, using an Oxford monograph containing a public version of the Mondex work":http://www-users.cs.york.ac.uk/~susan/bib/ss/z/monog.htm", as our basic reference. We held a workshop at the Rutherford Laboratory on the 16th/17th January 2006, where we had a talk on the structure of the existing Mondex specification and proof. We also had some talks from several of the groups on their methods, tools, and probable approach to the problem. We will hold another workshop at Rutherford on the 25th/26th of May.

We have approval in principle for a special issue of Formal Aspects of Computing containing eight or nine papers reporting the work: papers containing details of individual groups, and one paper comparing what each group did, summarising conclusions, and setting a public research agenda for the future. The people involved during the next year will help to form the basis of an international project contributing to the grand challenge over the next ten to fifteen years.

In January (unfortunately just after the workshop) Gerhard Schellhorn's group at Augsburg University in Germany became aware of the project to verify the Mondex case study. They took up the challenge and proved the correctness of the specification and refinement of the communication protocol, except for moving local exception logs to a central archive. The results are available as a technical report.