摘要：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.
