Sciweavers

FAC
2008
97views more  FAC 2008»
13 years 11 months ago
A functional formalization of on chip communications
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...
Julien Schmaltz, Dominique Borrione
FAC
2008
80views more  FAC 2008»
13 years 11 months ago
Verification of Mondex electronic purses with KIV: from transactions to a security protocol
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...
FAC
2008
67views more  FAC 2008»
13 years 11 months ago
Specification, proof, and model checking of the Mondex electronic purse using RAISE
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...
Chris George, Anne Elisabeth Haxthausen
FAC
2008
127views more  FAC 2008»
13 years 11 months ago
Mechanising Mondex with Z/Eves
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 ...
Leo Freitas, Jim Woodcock
FAC
2008
178views more  FAC 2008»
13 years 11 months ago
Modeling and validating Mondex scenarios described in UML and OCL with USE
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...
Mirco Kuhlmann, Martin Gogolla
FAC
2008
70views more  FAC 2008»
13 years 11 months ago
Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method
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...
Tahina Ramananandro
FAC
2008
107views more  FAC 2008»
13 years 11 months ago
An incremental development of the Mondex system in Event-B
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...
Michael Butler, Divakar Yadav