Z specifaction
Download as docx, pdf0 likes363 views
The document describes an ATM software system for a local bank. The system allows users to view account balances, withdraw and deposit funds using an ATM. The system consists of an account database, cash dispenser and deposit slot. It defines operations for user authentication, checking balances, withdrawing and depositing money, and refilling the cash dispenser. The operations ensure the correct behavior of the system and handle error cases.
Z specifaction
- 1. 1 Project Name : ATM Software System A local bank intends to install a new automated teller machine (ATM) to allow users to perform basic financial transactions .Each user can have only one account at the bank.ATM users should be able to view their account balance, withdraw cash and deposits funds. Account schema hold the record of user like his account id account pin and balance. Account account_id : account_pin : balance : balance 0 i. account _id to identify the user account ii. account _pin to verify the user iii. balance is always greater or equal to zero The amount of ATM is stored in cash dispenser which is filled on daily basis. And the maximum amount which is stored in cash dispenser is 10000. CashDespenser out_money : limit : limit = 10000 out_money = 10000 i. limit is initialize to 10000.
- 2. 2 ii. out_money is initialize to 10000. A Deposit Slot to receive the money from user and add it to his account. DepositSlot in _ money : envelop _ received : {yes , no} in _ money > 0 i. in_money to store the amount of entered amount to add in his account. ii. envelop_recived to check either user gives the amount to deposite slot or not. iii. in _money must be greater then 0. ATM consists of account, cash despenser, and a deposit slot. ATM by using database of bank verify the user. ATM Account CashDespenser userauthentication({account_idaccount_pin)} : {yes ,no} DepositSlot balance = DB_balance(account_id) i. balance is initialize with the amount stored in the bank database regarding account id.
- 3. 3 An operation to refill ATM Cash Despenser Refill ATM amount ? : reply! : MESSAGE amount + out_money limit out_money = out_money + amount Pre-Condition : By adding amount in Cash Despencer it will not exceed the limit. Add the entered amount in the out_money . An operation for verification of user. Authentication ATM account ? : pin ? : reply : MESSAGE userauhtentication({account?pin?}) = yes reply! = acess granted Pre-Condition: userauhtentication must be yes. .
- 4. 4 BadAuthentication ATM account ? : pin? : reply : MESSAGE userauhtentication({account?pin?}) = no reply! = invalid user Pre-Condition : userauhtentication must be no. MESSAGE== acess granted | invalid user Robust Authentication= Authentication BadAuthentication An operation to check the current balance. BalanceInquirey ATM showbalance ! : showbalance ! = balance SuccessfulBalanceInquire= Authentication BalanceInquirey An operation to withdraw the money.
- 5. 5 WithDraw ATM amount ? : reply ! : MESSAGE amount ? balance amount ? out _ money balance = balance amount out_money = out_monet - amount reply ! = transaction_successful Pre-Condition : i. Enter amount must be less then equal to balance. ii. Enter amount must be less then equal to out_money. Entered amount is subtracted from balance. Entered amount is subtracted from out_money. SuccessfulWithDraw= Authentication WithDraw To deal the case when user not have enough balance. BadWithDraw(1) ATM amount ? : reply ! : MESSAGE amount ? > balance reply ! = Insufficent_Balance Pre-Condition : Enter amount is grater then balance.
- 6. 6 To deal the when ATM has not have enough balance. BadWithDraw(2) ATM amount ? : reply ! : MESSAGE amount ? > out _ money reply ! = Not_enough_amount_in_ATM Pre-Condition : Enter amount is grater then out_money . MESSAGE== transaction_successful |Insufficent_Balance | Not_enough_amount_in_ATM Robust WithDraw = SuccessfulWithDraw BadWithDraw(1) BadWithDraw(2) An operation to deposit money in Account.
- 7. 7 Deposite ATM amount? : env? : envelop _ received reply! : MESSAGE env?= yes amount? > 0 balance = balance + amount reply! = Transaction_Successful Pre-Condition : User must give the envelope of money. Given amount must be grater then 0. Entered amount added in the balance of user. SuccessfulDEPOSITE= Authentication Deposite To deal with the case when user dont give the envelope of user.
- 8. 8 BadDeposite ATM amount? : env? : envelop _ received reply! : MESSAGE env?= no reply! = Plz_Give_Amount Pre-Condition: User dont give the envelope of money. MESSAGE== Transaction_Successful | Plz_Give_Amount Robust Deposite = SuccessfulDeposite BadDeposite