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)



Source files

Work as of May 2006

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


Last modified November 6th, 2007