Specifying safety and critical real-time systems in Z

As a case study, An Automated Teller Machine (ATM) is a safety-critical and real time system. According to requirements of ATM system we have different machine state status, and four different operations: Withdrawal, Deposit, Transfer, and Inquiry. A key part of early design phases are specifications, which span from requirement, to functional, to design, specifications. This paper describes the conceptual and formal models of the ATM. The formal model of the ATM is specified by using formal specification language. We have used the proper specification language i.e. Z notation. For writing the Z-schemas and the notations we have used the Z-word tool. Which support almost all Z symbols are on the Z-Palette. This model is finally checked using Z/EVES toolset. Therefore this paper attempts to formalize an event-based automation system using formal specification method.