The Mondex Case Study

  • Supervisor Dermot Cochran
  • Subject Area rigorous software engineering
  • Pre-requisite very good knowledge of Java, basic understanding of assertions and contracts, good knowledge of logic
  • Co-requisite (things you must learn along the way) the Z specification language, writing specifications in JML, using the JML tool suite and ESC/Java2
  • Subject Coverage system design and specification, applied formal methods, static analysis
  • Project Type analysis, design, and implementation
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

Mondex is a smart card electronic cash system (sometimes called an "electronic purse") that was originally developed by National Westminster Bank and subsequently sold to MasterCard International. Mondex launched in a number of markets during the 1990s, expanding from an original trial in Swindon, UK to Hong Kong and New York. It was also used on several UK university campuses from the late 1990s, including the University of Exeter (between 1997 and 2001), University of York, University of Nottingham and Aston University.

The Mondex system is an example of a critical software system since it is responsible for (in aggregate) large sums of money. Therefore, the Mondex system had to be certified to the highest level. Consultants and academics from the UK specified and proved critical behavioral and security properties about the system using a formal language called "Z" (pronounced "zed"). This formal modeling and verification helped Mondex achieve an ITSEC level E6 certification.

The Mondex system has been used in 2006 as a case study in comparing modern applied formal methods. Several groups around the world have reviewed, specified, and proven correct the Mondex system using a wide variety of different formal languages, theorem provers, and formal models.

The goal of this project is to design, specify, develop, and test a Java-based realization of the Mondex system. The Extended BON specification language will be used for high-level analysis, requirements and system structure and medium-level (formal) architecture design, the Java Modeling Language language will be used for low-level behavioral specification, and the JML tool suite and ESC/Java2 will be used to compile, document, test, and statically check the implementation's functional and security properties.

The result of this project will be submitted to the Verified Software Repository (under construction in the UK, but the QPQ site mentioned below is the prototype) and will thus be a key case study, reference, and benchmark against which future projects will be compared, particularly with respect to the use of these verification-centric tools, technologies, and process.

Note that, while the Z specification is quite large and looks intimidating (and took over a year to write and prove), modern teams have conducted this experiment in only a couple of man-weeks of work, and the Mondex architecture should only have a handful of Java classes with around fifteen invariants. I.e., Mondex is actually a very small system, from a software engineering standpoint.

Mandatory

  1. Learn basic Z so as to be able to read the Mondex specifications.
  2. Review and refine knowledge of JML already gained in Dr. Kiniry's Software Engineering modules.
  3. Review and refine knowledge of the Extended BON specification language already gained in Dr. Kiniry's Software Engineering modules.
  4. Learn the verification-centric software engineering process (the KindSoftware Process), as specified by Dr. Kiniry.
  5. Learn the basic use of the JML compiler, unit testing with JML-jUnit, and documentation generation with jmldoc.
  6. Specify the Mondex system in EBON
  7. Specify the Mondex system in JML
  8. Check the soundness of the JML specifications using ESC/Java2.
  9. Implement the Mondex system using the KindSoftware Process according to the EBON specifications and JML contracts (i.e., use Design by Contract).
  10. Submit the Mondex system to the Verified Code Repository.

Discretionary

  1. Generate and execute unit tests using JML-jUnit.
  2. Write unit tests corresponding to EBON scenarios using jUnit.
  3. Check the Mondex system implementation rigorously with ESC/Java2.

Exceptional

  1. Co-author a paper with Dr. Kiniry on this Mondex system realization.

Sources of information and preparatory reading

  1. The Mondex Case Study QPQ homepage.
  2. The Verified Software Repository Project
  3. The Mondex Wikipedia entry.
  4. The Z notation for system specification and verification
  5. The BON specification language website
  6. The Extended BON project
  7. The KindSoftware Coding Standard
  8. The JML tool suite
  9. The Extended Static Checker for Java, ESC/Java2
  10. Design by Contract