The system is composed of till which can access a central resource containing the detailed records of customers’ bank accounts. A till is used by inserting a card and typing in a Personal Identification Number (PIN) which is encoded by the till and compared with a code stored on the card. After successfully identifying themselves to the system, customers may either:

1. make a cash withdrawal or
2. ask for a balance of their account to be printed.

Withdrawals are subject to a user resources, which means the total amount that user has on account. Another restriction is that a withdrawal amount may not be greater than the value of the till local stock.

Tills may keep illegal cards, i.e. after three failed tests for the PIN.

• The case has been originally taken from the paper:
  T. Denvir, J. Oliveira, and N. Plat., The Cash-Point (ATM) ’Problem’, Formal Aspects of Computing, 12(4):211–215, 2000.
  See also Author's page
  Local copy - developers only
• Pascal Poizat, Jean-Claude Royer KADL Specification of The Cash Point Case Study
• UML – A Programmers Guide the same in the local copy

• https://ai.ia.agh.edu.pl/wiki/pl:miw:miw08_ardcase_cs:bankomat
• https://ai.ia.agh.edu.pl/wiki/hekate:bib:hekate_bibliography#kaczor2008csltr208