This paper presents a formal model and a systematic approach to the validation of communication tures at a high level of abstraction. This model is described mathematically by a fu...
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 how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by...
We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach ...
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...
This paper explains how the Alloy model-finding method has been used to check the specification of an electronic purse (also called smart card) system, called the Mondex case study...
A development of the Mondex system was undertaken using Event-B and its associated proof tools. mental approach was used whereby the refinement between the abstract specification o...