An Automatic Teller machine (ATM) is an Electronic Device that provides services like balance inquiry, cash withdraw and money transfer etc. The ATM system is considered an example of a safety...

An Automatic Teller machine (ATM) is an Electronic Device that provides services like balance inquiry, cash withdraw and money transfer etc. The ATM system is considered an example of a safety critical system and hence the need to formalize its services. To formalize the ATM system we need to first declare variables to be used.
- An ATM card contains the following information CARD := cardNo | accountNo | expiryDate - After any transaction the ATM machine gives the following responses ATMRESPONSE := operationSuccessfull | operationFailed - An ATM can be in two states STATE := available | busy - For any withdraw operation the ATM machine has restrictions on the minimum and maximum amount one can withdraw. AMOUNT := minimumAmount | maximumAmount - The other important variable is the date DATE := issueDate | expiryDate | todayDate - The ATM generates the following possible error messages ERROR := invalidCard | invalidPin | invalidAmount | insufficientBalance - Below is a schema for a Bank Account
Account accountName : PNAME accountNo : PNUMBER balance : NUMBER →7N Has : NAME ↔ NUMBER domHas = accountName balance(NUMBER) ≥ 0
Use the information provided above to develop schema that describe the following ATM operations.
(a) Card reading
(b) Balance inquiry
(c) Withdraw
(d) Money transfer from one account to the other