The Formal Design Model of an Automatic Teller Machine (ATM)

The Formal Design Model of an Automatic Teller Machine (ATM)

Yingxu Wang, Yanan Zhang, Philip C.Y. Sheu, Xuhui Li, Hong Guo
Copyright: © 2010 |Pages: 30
DOI: 10.4018/jssci.2010101907
OnDemand:
(Individual Articles)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

An Automated Teller Machine (ATM) is a safety-critical and real-time system that is highly complicated in design and implementation. This article presents the formal design, specification, and modeling of the ATM system using a denotational mathematics known as Real-Time Process Algebra (RTPA). The conceptual model of the ATM system is introduced as the initial requirements for the system. The architectural model of the ATM system is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs), which share a generic mathematical model of tuples. The static behaviors of the ATM system are specified and refined by a set of Unified Process Models (UPMs) for the ATM transition processing and system supporting processes. The dynamic behaviors of the ATM system are specified and refined by process priority allocation, process deployment, and process dispatch models. Based on the formal design models of the ATM system, code can be automatically generated using the RTPA Code Generator (RTPA-CG), or be seamlessly transformed into programs by programmers. The formal models of ATM may not only serve as a formal design paradigm of real-time software systems, but also a test bench for the expressive power and modeling capability of exiting formal methods in software engineering.
Article Preview
Top

The Conceptual Model Of The Atm System

An ATM system is a real-time front terminal of automatic teller services with the support of a central bank server and a centralized account database. This paper models an ATM that provides money withdraw and account balance management services. The architecture of the ATM system, as shown in Figure 1, encompasses an ATM processor, a system clock, a remote account database, and a set of peripheral devices such as the card reader, monitor, keypad, bills storage, and bills disburser.

Figure 1.

The conceptual model of the ATM system

jssci.2010101907.f01

Complete Article List

Search this Journal:
Reset
Volume 16: 1 Issue (2024)
Volume 15: 1 Issue (2023)
Volume 14: 4 Issues (2022): 1 Released, 3 Forthcoming
Volume 13: 4 Issues (2021)
Volume 12: 4 Issues (2020)
Volume 11: 4 Issues (2019)
Volume 10: 4 Issues (2018)
Volume 9: 4 Issues (2017)
Volume 8: 4 Issues (2016)
Volume 7: 4 Issues (2015)
Volume 6: 4 Issues (2014)
Volume 5: 4 Issues (2013)
Volume 4: 4 Issues (2012)
Volume 3: 4 Issues (2011)
Volume 2: 4 Issues (2010)
Volume 1: 4 Issues (2009)
View Complete Journal Contents Listing