УНИВЕРСИТЕТ ИТМО
Кафедра «Технологии программирования»

Моделирование работы банкомата

© И.А. Балтийский, С.И. Гиндин

Санкт-Петербургский государственный университет информационных технологий, механики и оптики

Проектная документация
Исполняемый код (компиляционный подход)
Исходные тексты (компиляционный подход)

Аннотация

Банкомат - это автоматизированное устройство, позволяющее удаленно осуществлять операции, связанные с аутентификацией пользователя (держателя счета в банке), просмотром текущего состояния счета, снятием денег со счета и осуществлением различных платежей. В данном проекте моделируется работа банкомата, включая не только клиентскую часть, но и серверную часть, обрабатывающую запросы, а также подсистему авторизации.

Основная задача при реализации таких систем - гарантия высокого уровня надежности клиентов-пользователей банка и информационной системы банка. Отсутствие таких гарантий может повлечь за собой не только прямые расходы банка, связанные с конкретными действиями злоумышленников, но и потерю репутации. Большинство уязвимых мест в безопасности систем такого уровня связано с ошибками, допущенными при создании системы. Среди них существенную часть составляют ошибки в программном обеспечении. Для борьбы с такими ошибками необходимо применять в разработке методы, позволяющие избежать их еще на стадии проектировки. Другое требование к методу разработки заключается в наличии способа формально доказывать корректность реализации.

Все эти требования выполняются при традиционном методе разработки лишь частично. Поэтому для создания систем, подобных вышеупомянутым, необходим другой подход. Таким подходом является метод автоматного программирования, который позволяет выразить на языке автоматов логику системы. Эта логика может быть подвергнута формальной верификации. После этого по модели поведения автоматически генерируется программа. Таким образом, процесс создания кода берет на себя специализированное программное обеспечение, а разработчик задает логику системы при помощи автоматов и реализует функции входных и выходных воздействий.

В данной работе на основе автоматного подхода выполнена генерация кода на основе использования инструментального средства UniMod для решения задачи эмуляции банкомата. Пользователь может осуществлять различные действия с картой, например, узнать баланс, снять деньги или осуществить платеж за телекоммуникационные услуги. Для операций с картой пользователь должен ввести её номер и PIN-код.

Заметим, что автоматный подход к решению рассматриваемой задачи на основе схемы взаимодействия "клиент-сервер" уже применялся ранее. Данная работа отличается от предыдущих созданием более развитой и углубленной модели банковской системы. С одной стороны, возможности эмуляции банкомата с точки зрения клиента соответствуют полному набору возможностей реального банкомата. Так, например, имеется возможность совершать оплату мобильной связи, не реализованная в других работах. С другой стороны, и эмуляция работы сервера банка отражает один из вариантов реализации, применяемый на практике - в частности, выделена подсистема авторизации пользователя.

Для запуска программы необходимо скачать исполняемый код. В архиве находятся исполняемые файлы для модели банкомата и сервера банка. Сначала надо запустить сервер банка, выполнив server.bat, затем запустить банкомат, выполнив atm.bat. В операционных системах семейства Windows для корректной работы эмуляций банкомата и сервера в переменной среды (environment variable) PATH должен содержаться путь к каталогу, в котором находятся исполняемые файлы Java (JRE или JDK): например, "C:\Program Files\Java\jre1.6.0_05\bin".

База данных, которой пользуется эмуляция сервера банка, находится в папке Server/data - в ней можно посмотреть номера карточек с PIN-кодами и балансами, которые распознаются банкоматом (Cards.dat), и номера телефонов, на которые можно класть деньги (Numbers.dat).

Инструкции по запуску содержатся также в файлах readme.txt (на русском языке) и readme EN.txt (на английском языке), находящихся в том же архиве.