Sciweavers

Share
FAC
2008

Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method

8 years 10 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, initially written in Z. After describing the payment protocol between two electronic purses, and presenting an overview of the Alloy modelfinding method, this paper explains how technical issues about integers and conceptual issues about the object layout in Z have been tackled in Alloy, giving general methods that can be used in most case studies with Alloy. This work has also pointed out some significant bugs in the original Z specification such as reasoning bugs in the proofs, and proposes a way to solve them.
Tahina Ramananandro
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FAC
Authors Tahina Ramananandro
Comments (0)
books