Formal Model of Automated Teller Machine System Using Z notation

In this paper, importance of formal methods has been demonstrated by applying them in the software development of safety critical systems such as automated teller machine system. We have demonstrated the application and integration of formal methods in existing software engineering life cycle. We have used the proper specification language i.e. Z notation, to ensure the correctness, reliability and consistency at analysis and design stage, before we start the actual implementation of the software system. Z notation is based on set theory and first order predicate logic. A formal model at abstract level has been developed in Z specification language. This model is finally checked using Z/EVES toolset.