ITMO University
“Programming Technologies” Department

Modeling of ATM System

© 2008. I.A. Baltiysky, S.I. Gindin

Saint-Petersburg State University of Information Technologies, Mechanics and Optics

Project documentation (russian, PDF)
Executable file (compilative approach)
Source code (compilative approach)

Annotation

Nowadays it is hard to find a person not aware of what an ATM is. Practically everyone knows that it is an automated device capable of remotely authenticating the user within the banking system and matching him or her to the bank account, checking current account status, withdrawing money from the account, and processing various payments (such as mobile phone pre-pay). This project aims to model the ATM service including not only the standalone ATM client, but also the server part processing ATM clients' requests and the authorization subsystem.

The main goal in development of such systems is to achieve a certain level of reliability which results in the safety guarantees for the clients and the bank itself. Lack of such guarantees may result in direct bank expenses to cover the losses connected with malicious access to the system; furthermore, as an even more undesirable consequence, the reputation may be damaged greatly or completely lost.

Most security issues in such systems are connected with the bugs committed during the development stage. Majority of bugs are entirely rooted in software. To prevent such types of errors, one needs to employ an approach that would allow avoiding the errors at the design stage. Furthermore, one may require the ability to formally verify the system. Conventional methods provide only partial compliance to these requirements.

In this project it is shown how to use the method that fully complies with the rules given above - the automata-based approach. With this approach, the developers only have to express the logic of the system in the language of automata; they fix bugs and may use tools for formal verification of the automata. The code is generated automatically, preventing the need of human coding, which reduces the amount of bugs in the system.

In the current project the problem of modeling an ATM module is considered. The problem is solved using the automata-based approach using the Unimod software tool.

To start a program, download executable files. The archive contains executables for the ATM model and the bank server model. It is necessary to start the server first (run server.bat), then start the ATM (run atm.bat). In Windows operation systems, ensure that environment variable PATH contains path to Java binaries (JRE or JDK), such as "C:\Program Files\Java\jre1.6.0_05\bin".

Note that the server database locates in Server/data directory - you may need it to check card numbers with PIN codes and card balances recognized by the ATM (Cards.dat) and phone numbers available for GSM pre-pay (Numbers.dat).

These instructions can be also found in readme.txt (in Russian) and readme EN.txt (in English) in the archive with executable assembly.