Shandong Provincial Key Laboratory of Computer Network Shandong Computer Science Center, Jinan 250014, P. R. China

---

Abstract—Model checking is an important technique for ensuring the correctness of investigated system. However, the model checking tools subject to the state-space explosion problem, which is an ignored hurdle to the practical application of the technique. This paper presents a case study of model checking the business flow of retail banking System, through an example of verifying automatic teller machine (ATM) with SPIN. We present the specific approach to effectively abstract the related part of ATM system, and give our experiment results. The verification results show that model checking is feasible technique for verifying the ATM system.

Index Terms—Model checking, spin, verification, automatic teller machine, retail banking.

[PDF]

Cite: Huiling Shi, Wenke Ma, Meihong Yang, Xinchang Zhang, "A Case Study of Model Checking Retail Banking System with SPIN," Journal of Computers vol. 7, no. 10, pp. 2503-2510, 2012.