TABLE OF CONTENT
1. Introduction
2. Machine description
3. Fuel machine - Artelier B CODE:
4. Credit machine
5. Credit machine - Artelier B CODE:
6. Operations:
7. Credit Machine's Function
8. Fuel Machine's Function
9. Operations of credit machine
10. Operations of fuel machine
11. Refinement
12. Limitations
13. Conclusion
Introduction
The report includes the design and implementation of the
machine called The_Petrol_Station_Club. The machine is designed used Atelier B
software. The B methods are being implemented in this project that is design of
two separate machines for the Gas Station. The machines are assigned with
different task and they are made to synchronize with each other to get the
information. The machines record and implement different operations with number
of functions. The two machines are as given below:
·
Fuel Machine
·
Credit Machine
MACHINE DESCRIPTION
Fuel machine are designed and deployed with fuel pump
machine that gives the permission of assigned fuel. This machine provides the
card members direct access to the fuel as per the request. The amount is
deduced from the credit on the card which is registered in the credit machine.
The data are being synchronized with other machine. The machine verifies if the
amount is appropriate with the fuel request and cut the credit according to the
fuel withdrawal. The code for the fuel machine are as given below:
Fuel machine - Artelier B CODE:
/* fuel_machine
* Author: Naif Filemban
* Creation date: 12-Nov-15
*/
MACHINE
fuel_machine
SETS
FUELTYPE = {petrol, diesel};
VARIABLES
FUEL
credit
fuel_price
INVARIANT
FUEL : FUELTYPE --> NAT &
credit /: {FUEL_price}
INITIALISATION
credit /= 100
END
Credit
machine
The Credit machine is designed to register and update the
account with amount for the fuel withdrawal. The operations that are being
carried out in the machine are to register the unregistered person. The new
membership card is being provided with appropriate account number and the
record is made alone with the card database separately. The field of amount
that are being stored for the purchase of fuel cannot be less than 100. The
machine is capable of evaluating the account number and the credit left. The code
for the design of the machine are as below:
Credit machine - Artelier B CODE:
/*
credit_machine
*
Author: Naif Filemban
*
Creation date: 12-Nov-15
*/
MACHINE
credit_machine
SETS
person={registered,
unregistered}; credit, fueltype={petrol,
diesel};
VARIABLES
Money,
Fuel
INVARIANT
money
<: NAT1 &
Fuel
: FUELTYPE
INITIALISATION
Fuel
:- FUELTYPE * {0} ||
money
:- {}
END
Operations:
Any one wish to join the member club of the station has to
credit the account not less than 100.
The credit amount is deposited at the credit machine that
checks for the withdrawal of the fuel
The fuel machine checks for the amount and provides the fuel
when the value of credit is not less than 100.
The functions that are being defined are as given below:
CREDIT MACHINE’S FUNCTIONS
·
The function Check_card checks the card number
and verifies if it registered or not.
·
The function Check_credit checks the card credit
·
The function desposit_credit makes the deposal
of amount into the particular credit account
·
The function Register_member makes the
registration of the person and assigns the card number.
FUEL MACHINE’S FUNCTIONS
·
The function check_card verifies the card
·
The function credit_limit check the credit
amount that shouldn’t be less than 100.
·
The function Fuel_withdraw provides the assigned
fuel as per the request of the card member after checking all the above
functions.
OPERATIONS OF CREDIT MACHINE
IF
person = {unregistered}
OPERATIONS
Register_member() =
PRE
Person = {unregistered}
THEN
Person = {registered}
END;
ELSE
PRE
check_card := NAT1
THEN
deposit_credit() = NAT
OPERATIONS OF FUEL MACHINE
IF
credit_limit >= 100
OPERATIONS
Fuel_withdraw()
END;
ELSE
OPERATIONS
failed()
Refinement
Figure 1 - fuel stock and withdraw
Petrol
|
Diesel
|
200
|
500
|
Table 1 - Stock_list table
The mapping table is being presented with the information of
the above figure. The index is mapped with the fuel type and the stock that are
being available on the particular station.
Stock : FUELTYPE → NAT
|
|
Tmap~
|
Stock_list()
|
FUELTYPE → index
|
Index → NAT
|
Table 2 - Stock table
INVARIANTS
Stock_list : seq(NAT)
&
Dom(stock_list) = index &
(tmap~;stock_list) = stock
withdraw: FUELTYPE → NAT
|
|
Tmap~
|
Withdraw()
|
FUELTYPE → index
|
Index → NAT
|
Table 3 - withdraw table
INVARIANTS
withdraw : seq (NAT)
&
Dom(withdraw) = index &
(tmap~; withdraw) = withdraw
The translation of the specification is done into the
Abstract machine notation. These notation are being used for the development of
the machine that includes the following:
·
Validation of the amount and the fuel
·
Synchronization of the database
·
Limitation of the fuel in the fuel pump with the
amount
Limitations
·
The machine that are designed in the Abstract
machine notation in B atelier has the syntax sensitivity.
·
The user input is required to withdraw the fuel
and that should be validated by the card holder.
·
The card is made to have limited amount of 100
in order to withdraw the fuel as per the requirement.
Problems that were encountered during the development
·
The programming is based on the B methods and it
requires special syntax and case sensitivity.
Conclusion
The machine are being designed with the B methods in the
Atelier B software. The information are translated into Abstract Machine Notations.
The necessary validation is undertaken in order to withdraw fuel from the
stations. These machine was made synchronize with each other for the appropriate
implementation of the system. The whole system is based on these two types of
machine. One handles the credit information along with the cash and the other
one is for withdrawal of the fuel and its choice along with the necessary
validation. The validation is undertaken for the amount contained in the card
and the fuel request. It also validate the amount that shouldn’t be less than
100.
No comments:
Post a Comment