The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge f...
Dominik Haneberg, Gerhard Schellhorn, Holger Grand...
This paper describes the Mondex case study with UML class diagrams and restricting OCL constraints. The constraints have been formulated either as OCL class invariants or as OCL pr...
Abstract. The Mondex case study concerns the formal development and verification of an electronic purse protocol. Several groups have worked on its specification and mechanical ver...