Cashpoint

Description

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: make a cash withdrawal or 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.

Source: The case has been developed based on the paper: T. Denvir, J. Oliveira, and N. Plat., The Cash-Point (ATM) ’Problem’, Formal Aspects of Computing, 12(4):211–215, 2000, and the ATM use case presented in UML – A Programmers Guide.

Model

BPMN Diagram types: Process,

Source files: cashpoint.sgx, cashpoint.bpmn cashpoint-all.pdf
Diagram files: cashpoint.svg , cashpoint.pdf

Cashpoint Bimloq case BPMN model

Model logic

XTT2 logic model: cashpoint_xtt.hml