Verification of money atomicity in digital cash based payment system

Abstract

Digital cash, analogous to the paper cash, is a certificate that carries a value. It is issued by an authorized entity and is verifiable by all. It can be used as an instrument for making payments or purchases. Unlike paper cash, being a digital data, it may be easily replicated which gives a scope for duplicate spending of the cash certificates. Digital cash based payment systems can be classified as business critical systems as any failure may lead to loss of trust. Verification of critical requirements of such systems is therefore essential. In this paper, we present refinement approach for construction of the models of the digital cash based payment system using Event-B, wherein we verify how money atomicity property can be preserved in these systems. This ensures that money is neither generated nor destroyed in the electronic payment transactions. © Springer-Verlag 2012.