The Mondex Case Study with Alloy

I have been attending a research internship since March 6th, until August 26th, 2006, at MIT (Massachusetts Institute of Technology), precisely CSAIL (Computer Science & Artificial Intelligence Laboratory), within the Software Design group led by Daniel Jackson. This research group aims at developing a specification language, called Alloy and based on first-order logic and relational calculus including transitive closures, and a tool, called Alloy Analyzer and based on model-finding through SAT-solving, to analyze specifications in this language.

The aim of this internship was to show the capabilities of the Alloy specification language and the Alloy Analyzer in automated specification checking, by tackling the proof of the specification (initially in the Z specification language) of the Mondex electronic purse system as a case study.

After discovering the Mondex case study through the first workshop on January 16th and 17th, and after discovering the Alloy formal method at the beginning of my internship, I modeled the Mondex system using the Alloy specification language and checked it for small scopes with the Alloy Analyzer, finding some bugs I showed in England at the second Mondex workshop on May 25th and 26th at Cosener's House, a dependency of Rutherford Appleton Laboratory (England). When I came back on June 6th, I improved that initial version to produce a more complete, rigorous Alloy specification of the Mondex system, before trying to generalize the results to any scope through external methods such as automated first-order theorem proving.

I would like to acknowledge all the SDG members for their useful help - sometimes overnight - throughout this internship and for the spirit of the laboratory which allowed me to discover an overview of some Computer Science research topics which are not tackled in France through visiting the laboratories and attending talks led by researchers from all over the world.

Final work (as of September 2006)

Publications

• Mondex, an electronic purse : specification and refinement checks with the Alloy model-finding method
  FACJ (Formal Aspects of Computing journal), special issue 20.1, January 2008.
  The official version is available here at www.springer.com.

Documents

• Summary of my work (PDF), to be included in a paper gathering all the different methods tackling the Mondex case study.
• Slides for the presentation at the University of York (PDF), on October 5th and 6th. Also in OpenDocument Presentation (ODP) format.
• Slides for the presentation at ENS (PDF) on September 20th. Also in OpenDocument Presentation (ODP) format.
• Internship report (PDF)

Source files

• Alloy source files for the final Mondex model. See section 4 of the internship report for further details
• Source files for the direct FOL attempt (section 6.1 of the internship report) ("TP" : Theorem Provers). Undocumented.
• Source files for the "lifted" FOL attempt (section 6.2 of the internship report) ("FOBAR" : First-Order with Bounded-Arity Relations). Undocumented.

Work as of May 2006

Here is the material I presented on May 25th at the Cosener's House, a dependency of RAL.

• Slides for the presentation at the Cosener's House (PPT) on May 25th.
• Alloy source files for the initial Mondex model (as of May), not described in the internship report

Miscellaneous

• L_YX and L^AT_EX sources and figures for the report and the paper

Last modified November 6th, 2007