Formal description of an ATM system by RTPA

An automated teller machine (ATM) is a safety-critical and real-time system. The modeling and description of an ATM is a classical real-world case because its conceptual model is well known as a working project in real-time system design. For ensuring correctness and dependability, real-time process algebra (RTPA) is adopted to specify a formal model of the ATM. By using RTPA, the architecture, static and dynamic behaviors of the ATM can be described formally, precisely, and consistently. This paper describes the conceptual and formal models of the ATM. The conceptual model of the ATM is described by a finite state machine (FSM), and the formal model is specified by RTPA. This paper demonstrates that the ATM can be formally described by a set of real-time processes in RTPA. It also shows the relationship between the RTPA model and the FSM model of the ATM system.