A research on auto teller machine (ATM) with Vdm

1.0       INTRODUCTION

In this 21^st century, industries are faced with the challenges of releasing commercial software projects of high quality and within the budget. Some software is delivered with errors, lack of complete functionality and overrun cost. Formal method has been introduced to be an effective way of helping developers to understand the users’ requirements by specifically defining functions, data resources, and basic limitations in a well-organized structure. In this paper, an in-depth analysis on the auto teller machine (ATM) system with vdm and its user specification and requirements will give a better understanding of formal methods in software development.

1.1    Proposal

1. CIMB Bank Malaysia 

76 Jalan Cerdas
Taman Connaught, Cheras
56000 Kuala Lumpur 
Wilayah Persekutuan

2. Front view of CIMB bank taman Connaught

3. ATM view of CIMB taman Connaught.

4. The machines as shown in view [3] has the following

·         3 ATM withdrawal machine

·         2 ATM deposit machine

·         1 cheque deposit/self service (SST) machine

5. With a picture view we would see the features in on selected ATM withdrawal machine.
   

·         1 is the ATM card slot in port.

·         2 is the ATM keypad input platform

·         3 is the ATM service screen

·         4 is the list of cards accepted by the ATM system

·         5 is the ATM cash dispenser slot.

·         6 is the ATM receipt dispenser slot.

6. From the above view in [3] the ATM machine can only process one request at a time making it a total of six active users in the bank branch.
7. The machine operates from 5 am to 12 pm daily
8. This paper will focus more on the CIMB withdrawal ATM, showing its constraints and functionality.

1.1.1   Software development life cycle (SDLC)

The Software development life cycle (SDLC) is a general term used to define the technique and procedure used in software development process.

FIG I.

As shown in the figure above is an SDLC process and without this process a software development is likely to face the following challenges:

·         Low Quality

·         Risk to time management

·         High cost of development, etc.

1.2       Formal Method

Formal methods are mathematics based languages, techniques and tools that can be applied at any part of a software program lifecycle (Pandey et al 2013). This simply defines the application of the Mathematical based approach in software development which uses filtration techniques at any stage to ensure the accuracy, completeness and stability of the specification.

            Another name used for formal methods is called formal specification languages, which are built on set theory and first order predicate calculus. The language has a formal semantics which are used to define express specifications in a clear and plain manner. A formal specification language can be used to model the most difficult systems using a simple mathematical approach, such as sets, relations and functions.

1.3       Uses of Formal method in SDLC

In SDLC, formal methods are used in various ways, but the two basic uses of formal method in SDLC are as below;

·         Specification (Requirement Analysis)

·         Verification (Testing).

1.3.1   Specification (Requirement Analysis): Requirement Analysis is a major process in the software development life cycle (SDLC) because it defines the system properties completely (i.e. Functional behavior, timing behavior, internal configuration, and performance features etc.). It also specifies the behavior of sequential and concurrent systems in formal methods such as (Z, VDM, Larch) and (CSP, CCS, State charts, Temporal Logic, Lamport and I/O automata) respectively.

1.3.2 Verification (Testing): This is a process of verifying or proving a system meets the correct formal method specification. And just like requirement analysis is important in software development life cycle (SDLC), verification is also very important because it helps to determine the quality, reliability and eliminate error in software development.

2.0       Constraint of ATM systems

To identify the necessary constraints of an ATM system based on the operation and safety, it is important to understand the operational base properly which then elaborate more on the safety. In the transition diagram below is an ATM operational behavior.

FIG II.                                                                                                            (Wang et al 2010)

As seen in the diagram above is an ATM operational behavior and with this a look at some of the operation and safety constraint are as below:

·         High Level Description Constraints

·         Functional Constraints

·         Data Constraints

·         Design and Interface Constraints

·         Quality Constraints

2.1       High Level Description Constraints:

1.    A client must make a cash withdrawal from any account connected to a card and authorization must be acquired from the bank before money is dispensed.

2.    A client can only have the capacity to make a balance request of any account connected to the card.

2.2       Functional Constraints:

1.    An ATM machine only acknowledges a card from a client when the client inputs a Personal Identification Number (PIN) to validate the client's identity.

2.    The ATM only follows up on the request as per the response got from the Bank framework for identity validation. Possible activities for granted requests include the following:

·         Dispense cash

·         Acknowledge deposit

·         Show or print account balance

·         Pay a bill

·         Perform an Electronic Funds Transfer (EFT)

2.3       Data Constraints:

1.    PINs are four digits long.

2.    Each card has its unique card number

3.    Non-sufficient funds in an account ought to bring about the dismissal of a withdrawal demand or cash advance exchange.

4.    ATM cards may connect to more than one account.

5.    PINs and account numbers are issued by the appropriate financial institutions.

2.4       Design and interface Constraints:

1.    The card reader ought to be the "swipe" type which shouldn’t be withheld by the machine in any transaction, and the interface must match with the bank's current financial system.

2.    The ATM machines won't correspond with each other, but the bank's financial system will handle the correspondence with other financial systems.

2.5       Quality Constraint:

1.    The system ought to react to requests in under five seconds and should be accessible for communication 97% of the time on a 24/7/365 basis.

2.    An individual ATM ought to process requests not involving dispensing funds when the cash hampers are empty.

3.    Cash hampers ought to be routinely serviced to keep up the comfort of bank clients

4.    Displays should be easy to read and touch pads simple to utilize.

3.0       Mind Map

The above is a mind map of Cimb banking showing all the departments, offices and facilities in the banking branch and services they offer.

The above is a Mind map of an ATM machine showing all the functionalities and features of the machine.

4.0    Class Diagram

As shown above is a class diagram showing the main attributes and operation of an auto teller machine (ATM) system and as per above mind map and class diagram below is a more elaborate diagram for the who auto teller machine (ATM) system.

ATM

+Bank +Customer +Account +Transcations

+Getbankname() +getcustomername() +depostcash() +withdrawcash() +insertcard() +getpin() +getbalance()

4.1       Class Diagram and relationship of the Bank.

4.2 Class Diagram of a cash withdrawal ATM

5.0    VDM Specification

The fundamental thoughts on this approach is first to formalize the requirements and afterward to complete a testing. At the point when formalizing the requirements, we abstract the program under testing into an arrangement of operations, each characterizing an autonomous administration, for example, Withdraw or Deposit in an automated teller machine (ATM) programming. The objective of the formalization is in this manner to compose a formal specification for every operation. To this end, we have to focus the signature of every operation, including the input variables, output variables, and the related outer variables (or state variables)

Functional Senario of ATM

A software system for a simplified Automated Teller Machine (ATM) needs to give two services to customers. The services incorporate withdrawing money from the customer's ledger and request for the account balance. To withdraw money, the customer's card and password as well as the requested sum are needed. The bank strategy does not permit overdraft when the service for withdrawal is used. For a request about the customer's account balance, the system should give the current balance of the customer's account.

5.1    Specification

5.1.1   Process Withdraw (Cardln: cardnumber,  numberIn : AccNum, amountIn: Amount)

ext wr accounts: AccNumAccount

pre exists! [acc: accounts]

            Ù (accounts(numberIn)).balance - amountIn  ≥ - (accounts(numberIn)).limit

post let  bal = (acount(numberIn)).balance

in

let trans = ( account (numberIn)).transactions

in

let newTrans = make-Transaction(dateIn, amountIn,< withdrawal>)

in

accounts  =  account  † {numberIn a

                                    m(account (numberIn),

balance a bal - amountIn,  transactions  a trans ^ [newTrans])}

5.1.2   Change limit (numberIn : AccNum, limit :amountln)

Ext wr Account: AccNum Account

Pre numberIn Î accounts Ù limitIn ³ 0

Ù accounts(numberIn).balance ³ - limitIn

Post accounts =  account † {number In a

m(account (numberIn), limit a limitIn)}

5.1.3   Check Balance (numberIn : AccNum, Balanceln)

Ext wr Account: AccNum Account

Pre numberIn Î accounts Ù balanceln ³ 0

            Ù accounts(numberIn).balance

Post accounts =  account † {numberIn a

            m(account (numberIn), Balance a balanceln)}

5.1.4   Change Pin (numberIn : AccNum, ChangePin :pinln)

Ext wr Account: AccNum Account

Pre numberIn Î accounts Ù pinln

            Ù accounts(numberIn).balance ³ - pinln

Post accounts =  account † {numberIn a

            m(account (numberIn), ChangePin a pinln)}

6.0    Conclusion

Formal method plays a very important role in software development because it monitors the whole software process and in the case of this project topic, it monitors all sessions on the software development ranging from design to the implementation. With the help of the formal method, future error is systems are being eliminated, giving a more standard and quality software.

7.0    References

Pandey, S. K., & Batra, M. (2013). Formal Methods in Requirements Phase of SDLC. International Journal of Computer Applications. Published by Foundation of Computer Science. New York. USA.

Wang, Y., Zhang, Y., Sheu, P. C., Li, X., & Guo, H. (2010). The Formal Design Model of an Automatic Teller Machine (ATM). International Journal of Software Science and Computational Intelligence (IJSSCI)

Liu, S., & Shen, W. (2012, May). A formal approach to testing programs in practice. In Systems and Informatics (ICSAI), 2012 International Conference on (pp. 2509-2515). IEEE.