SucheMondex
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.
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.