ATM Example

In this example, we define the structure and behavior of an automated teller machine (ATM) in a UML model and validate the model’s functional correctness by defining and executing test cases.

For withdrawing money from an ATM system, the client puts his card into the ATM and enters the PIN of the card, as well as the amount of money that should be withdrawn from the client’s bank account. The ATM system then checks whether the entered PIN is valid and whether the withdrawal is possible, i.e., whether the balance of the client’s bank account exceeds the amount of money to be withdrawn. If the withdrawal is possible, the balance of the account is accordingly updated.

UML Model

The class diagram defining the structure of the ATM system is depicted in Figure 1. It defines several classes: Card, Account, ATM, Transaction, Record, Deposit, and Withdrawal. The class Card owns two Integer attributes number and pin and is associated with the class Account, which owns two Integer attributes number and balance. The described withdrawal functionality is defined by the operation withdraw() of the class ATM, the operation validatePin() of the class Card, as well as the operation makeWithdrawal() of the class Account. The activities defining the behavior of these three operations are depicted in Figure 2 (ATM::withdraw()), Figure 3 (Card::validatePin()), and Figure 4 (Account::makeWithdrawal()).

The activity ATM.Withdraw (Figure 2) defining the behavior of the operation ATM::withdraw() gets as input the card, the pin, and the amount of money to be withdrawn entered by the client. It first starts a new transaction by calling the operation ATM::startTransaction(), then calls the operation Card::validatePin() for validating the pin entered by the client. If the pin is valid, the account associated with the provided card is obtained, and the operation Account::makeWithdrawal() is called to perform the withdrawal of the provided amount of money from the account. Finally, the operation ATM::endTransaction() is called to end the current transaction, and add it to the completed transactions of the ATM.

The activity Card.ValidatePin (Figure 3) defines the behavior of operation Card::validatePin() and checks whether the pin stored on the card matches the provided pin. If this is the case, true is provided as output, otherwise false is provided. If the call of the operation Card::validatePin() provides false as output, the activity ATM.Withdraw also provides false as output indicating an unsuccessful withdrawal. Otherwise, the withdrawal is carried out by calling the operation Account::makeWithdrawal() (Figure 2 action makeWithdrawal) for the account associated with the provided card whose behavior is defined by the activity Account.MakeWithdrawal.

The activity Account.MakeWithdrawal (Figure 4) first checks whether the account’s balance exceeds the amount of money to be withdrawn. If this is the case, the balance is reduced by this amount, a new withdrawal record is created (action createNewWithdrawal), and the activity provides true as output indicating the successful update of the account’s balance. Otherwise false is provided as output. If the activity Account.MakeWithdrawal provides true as output, the activity ATM.Withdraw (Figure 2) also provides true as output indicating the successful withdrawal, otherwise false is provided.

Figure 1: Class diagram of the ATM system

Figure 2: Activity for operation ATM::withdraw()

Figure 3. Activity for operation Card::validatePin()

Figure 4: Activity for operation Account::makeWithdrawal()

Test Suite

To validate the correct behavior of the activity ATM.Withdraw, we defined the test suite depicted in Listing 1.

The test scenario defines one ATM object atmTD, one Account object accountTD with the balance 100, one Card object cardTD with the pin 1985, and a link between the objects cardTD and accountTD. Furthermore, it defines one Deposit object depositTD with the amount 100, and a link between the objects accountTD and depositTD.

Test case 1 atmTransactionTest is used for testing that if the correct pin is provided and the amount of money to be withdrawn does not exceed the balance of the associated account, the balance is accordingly updated and true is provided as output indicating a successful withdrawal. Further, it checks whether the pin is validated before the account is updated.

The test case defines the activity ATM.Withdraw as activity under test. The object atmTD is defined as context object (i.e., the activity shall be executed for this object). As input the object cardTD defined in the test scenario as well as the Integer values 1985 and 100 are provided for the parameters card, pin, and amount. The test case consists of one execution order assertion and two state assertions.

The execution order assertion (line 20) defines that the operation Card::validatePin() shall be called (action validatePin) before the operation Account::makeWithdrawal() is called (action makeWithdrawal).

The first state assertion (lines 21-23) checks that once a transaction is created for the withdrawal (i.e., a link for the reference ATM.currentTransaction is created), this transaction is in the end of the execution finished (i.e., the link for the reference ATM.currentTransaction is destroyed) and added to the completed transactions of the ATM system (i.e., a link for the reference ATM.completedTransactions is created). For expressing these assertions OCL constraints are used. These constraints are defined in a separate file and are depcited in Listing 2. OCL constraints are invoked by name within state assertions and can be used for both defining asertions on the state of the system and defining temporal expressions (cf. Listing 1 lines 21-23).

The second state assertion (lines 24-29) checks that in the end of the execution of the activity, the account’s balance was updated to 0 and true was provided as output. Furthermore, the OCL constraints NumOfWithdrawsSuccess and BalanceRecords (Listing 2) are evaluated on the account object. NumOfWithdrawsSuccess checks that in the end of the execution one withdrawal record was added to the account. BalanceRecords checks that in the end of the execution the balance of the account is equal to the difference between the sum of all deposit records and the sum of all withdrawal records of the account.

Test case 2 atmTransactionFail is used to validate that if the amount of money to be withdrawn exceeds the account’s balance, the withdrawal is not carried out (i.e., the account’s balance remains unchanged) and false is provided as output indicating an unsuccessful withdrawal. To test this requirement, we specify 200 as input for the amount of money to be withdrawn and define a state assertion (lines 39-44) which checks that after the last action was executed, the balance of the account is unchanged (100) and false is provided as output.

1  import banking.structure.*
2  scenario BankingTestData[
3    object atmTD: ATM {}
4    object accountTD: Account {Account.balance = 100;}
5    object cardTD: Card {Card.pin = 1985;}
6    object depositTD: Deposit {Record.amount = 100;}

7  link card_account {
8   source card_account.card = cardTD;
9   target card_account.account = accountTD;
10 }

11 link account_record {
12  source account_record.account = accountTD; 
13   target account_record.records = depositTD;
14 }
15]

16 test atmTransactionTest activity ATM.Withdraw (ATM.Withdraw.card
17   = BankingTestData.cardTD, ATM.Withdraw.pin = 1985, ATM.Withdraw.amount = 100) 
18   on BankingTestData.atmTD{
19  initialize BankingTestData;
20  assertOrder *, ATM.Withdraw.validatePin, *, ATM.Withdraw.makeWithdrawal, *;

21  assertState eventually after constraint 'TransactionCreated' {
22    check 'TransactionEnded', 'TransactionAdded';
23  }
24  finally {
25   ATM.Withdraw.readAccount.result::Account.balance = 0;
26   ATM.Withdraw.success = true;
27   check 'NumOfWithdrawsSuccess', 'BalanceRecords'
28     on ATM.Withdraw.readAccount.result;
29  }
30 }

31 test atmTransactionFail activity ATM.Withdraw (ATM.Withdraw.card
32   = BankingTestData.cardTD, ATM.Withdraw.pin = 1985, ATM.Withdraw.amount = 200) 
33     on BankingTestData.atmTD{
34   initialize BankingTestData;
35   assertOrder *, ATM.Withdraw.validatePin, *, ATM.Withdraw.makeWithdrawal, *;
36   assertState eventually after constraint 'TransactionCreated' {
37     check 'TransactionEnded', 'TransactionAdded';
38   }
39   finally {
40     ATM.Withdraw.readAccount.result::Account.balance = 100;
41     ATM.Withdraw.success = false;
42     check 'NumOfWithdrawsFail', 'BalanceRecords'
43       on ATM.Withdraw.readAccount.result;
44   }
45 }

1 package structure
2 context ATM
3 inv TransactionCreated: currentTransaction <> null
4 inv TransactionEnded: currentTransaction = null
5 inv TransactionAdded: completedTransactions->size() > 0
6 context Account
7 inv NumOfWithdrawsSuccess: records->select(oclIsTypeOf(Withdrawal))->size()=1
8 inv NumOfWithdrawsFail: records->select(oclIsTypeOf(Withdrawal))->size()=0
9 inv BalanceRecords: (records -> select(oclIsTypeOf(Deposit)) ->
10    collect(Record::amount) -> sum() - records -> select(oclIsTypeOf(Withdrawal))
11    -> collect(amount) -> sum()) = balance
12 endpackage

Test Results

1 Test Suite Run: 29-10-2014 17:12:56
2 TestCase: atmTransactionTest
3 Activity: ATM.Withdraw
4 Activity context object: atmTD
5 Activity input: card = cardTD; pin = 1985; amount = 100;

6  Number of paths checked: 125
7  Number of invalid paths: 111
8  Failed path:  init, splitCard, context, readAccount, startNewTransaction,
9                makeWithdrawal, contextForEnd, endTransaction, validatePin
10 Failed path:  init, splitCard, context, readAccount, makeWithdrawal,
11               startNewTransaction, contextForEnd, endTransaction, validatePin
12 Failed path:  init, splitCard, context, readAccount, makeWithdrawal,
13               contextForEnd, startNewTransaction, endTransaction, validatePin
14 Failed path:  init, splitCard, context, readAccount, makeWithdrawal,
15               contextForEnd, endTransaction, startNewTransaction, validatePin
16 Failed path:  init, splitCard, context, startNewTransaction, readAccount,
17               makeWithdrawal, contextForEnd, endTransaction, validatePin18
18 There are 106 more failed paths.
19 Order specification: *, validatePin, *, makeWithdrawal, *
20 Matrix validation result: FAIL
21 State assertion: EVENTUALLY AFTER constraint TransactionCreated
22 Constraints checked: 2
23 Constraints failed: 1
24 Constraint: TransactionAdded State(s): endTransaction, validatePin,
25             makeWithdrawal, startNewTransaction
26 State assertion: ALWAYS AFTER action endTransaction
27 Constraints checked: 2
28 Constraints failed: 0
29 State expressions checked: 2
30 State expressions failed: 0
31 ******************
32 TestCase: atmTransactionFail
33 Activity: ATM.Withdraw
34 Activity context object: atmTD
35 Activity input: card = cardTD; pin = 1985; amount = 200;36 Number of paths checked: 125
37 Number of invalid paths: 111
38 Failed path: init, splitCard, context, readAccount, startNewTransaction,
39              makeWithdrawal, contextForEnd, endTransaction, validatePin
40 Failed path: init, splitCard, context, readAccount, makeWithdrawal,
41              startNewTransaction, contextForEnd, endTransaction, validatePin
42 Failed path: init, splitCard, context, readAccount, makeWithdrawal,
43              contextForEnd, startNewTransaction, endTransaction, validatePin
44 Failed path: init, splitCard, context, readAccount, makeWithdrawal,
45              contextForEnd, endTransaction, startNewTransaction, validatePin
46 Failed path: init, splitCard, context, startNewTransaction, readAccount,
47              makeWithdrawal, contextForEnd, endTransaction, validatePin
48 There are 106 more failed paths.
49 Order specification: *, validatePin, *, makeWithdrawal, *
50 Matrix validation result: FAIL
51 State assertion: EVENTUALLY AFTER constraint TransactionCreated
52 Constraints checked: 2
53 Constraints failed: 1
54 Constraint: TransactionAdded State(s): endTransaction, startNewTransaction,
55             validatePin, makeWithdrawal

56 State assertion: ALWAYS AFTER action endTransaction
57 Constraints checked: 2
58 Constraints failed: 0
59 State expressions checked: 2
60 State expressions failed: 0
61 ******************

Figure 5: Activity for operation ATM::withdraw() (corrected)

Resources

• Project containing the UML model and test cases