SIMULATION AND VERIFICATION OF ATOMICITY PROPERTIES FOR AN ELECTRONIC CASH SYSTEM
Panagiotis Katsaros, Vasilis Odontidis, Maria Ch. Gousidou-Koutita · 2005
An electronic cash system as any distributed system is subject to site and communication failures, as well as potential security attacks. This work focuses on simulation and verification of three important correctness properties, for ensuring failure resilience or detecting potential property violation scenarios. We refer to the NetBill electronic cash system and the properties to be checked are money atomicity, goods atomicity and certified delivery. We introduce a Colored Petri Net that models NetBill, in the presence of site or communication failures and all possible transaction abort cases. The presented model has been implemented in CPN Tools, a graphical ML-based tool for analyzing Colored Petri Nets. This allows us to combine the provided state space exploration functions and the supported Computation Tree like temporal logic (CTL), for model checking the forenamed atomicity properties. At the same time, it is possible to exploit the provided interactive simulation facilities to explore potential property violation scenarios and correct the protocol's design.