Mondex is an electronic purse, i.e. it contains money, and it is possible to transfer money from one card to the other. Loading and unloading a card is not modeled.
Much more information can be found on our Mondex project page.

Modeling an application is an iterative process. Here we present a linear walk-through of the documents.

Begin the walkthrough

Jump to selected documents

• Sequence diagrams
• Class and Deployment diagrams
• Activity diagram for TransferMoney
• More activity diagrams
• Generated Source code
• Generated formal model with a direct security proof, i.e. specification, ASM, and a direct (not using refinement) security proof. You can find the refinement proofs here.