Z Notation for UBER App: Formal Strategies for Enterprise Security

This document discusses the use of Z notation for securing and calculating the time estimate in the UBER app for food delivery. It explains the schema and operations for creating and deleting customer and driver details. It also covers the cancellation and payment processes. The document highlights the benefits of using Z notation in managing the operations of the UBER Company.

2019
Software Engineering
Methodologies
[Type the document subtitle]
[Type the author name]
[ T Y P E T H E C O M P A N Y A D D R E S S ]

Student Number: ________________
ABSTRACT
For increasing the security of the network framework formal strategies are being
used for the commercial enterprise uses of the UBER app which deals in food
delivery. It helps to protect the risks for the base facts. We had used app-based
enterprise protection. We had used Z notation for making use to explain the online enterprise clients in
the UBER case. Here the UBER is the app that is used to deliver the food to the online clients. We had
used Z notations for securing and calculating the time estimate between receiving delivering the food.
This time duration is calculated by the taxi driver.
Z Notation Schema
1. For Modeling the UBER, Company has created the schema. This will only contain clients. Following
tasks are being performed in this notation:
Add Company
UBER
Known: L Name
ID: L ID
Known =dom ID
1 | P a g e

Student Number: ________________
Add Order
Add Order
Δ UBER
CustomerName? : NAME
CustomerNo? : ISBN
Date ? : DATE
ItemList? : List
Address ? : Address
Payment?:Amount
ISBN
CustomerName? ∈ Known
CustomerNo? ∈ Known
Cost? ∈ Known
Address? ∈ Address
ItemList? ∈ List
Payment?: ∈ Amount
Customer ′=Customer { CustomerName?→ CustomerNo?}∪
2 | P a g e

Student Number: ________________
In the above, we can see the operation of an order, where we can see the details of the customer name,
the customer no, date and item list and address and payment details. In the item list, we can store the
details of the order food list and in payment, we can store the total amount.
Add a Driver
Driver
Known : L Name
DId: L ID
DAddess: L ADDESS
DEmail :L EMAIL
DPhone : L Phone
DDob : L DOB
DKnown =dom ID
Delivery Request
3 | P a g e

Student Number: ________________
Δ Member
CustomerName? : NAME
CustomerNo? : ISBN
Date ? : DATE
Location? :Loc
ISBN
CustomerName? ∈ Known
CustomerNo? ∈ Known
Delivery ′= Delivery ∪{ CustomerName?→ CustomerNo?, CustomerNo? →Date?,
Address? → Address? }
Remove a order
Get Customer First
4 | P a g e

Student Number: ________________
FINDCustomer
ΞUBER
CustomerName? : NAME
BookingNo? : ID
ISBN
CustomerNo !′={ n : CustomerNo | (n→ CustomerName? )∈ Customer}
Remove Customer
REMOVE Customer
ΔUBER
CustomerName? : NAME
CustomerNo? : ID
ISBN
Customer ′=Customer ⧹{ CustomerName?→ CustomerNo?}
In the above notation, we can see the operation of the remove customer from database where we can
customer details.
5 | P a g e

Student Number: ________________
Delete Deriver
Find driver
FindDriver
ΞUBER
DriverName? : NAME
DriverID? : ID
ISBN
DriverID!′={ dn : DriverID | (dn → DriverName? ) ∈ Driver}
Receive order
RecieveOrder
Δ Member
CustomerName? : NAME
CustomerNo? : ID
OrderID?:ID
Date ? : DATE
Status?:Recived/Not recieved
ISBN
CustomerName? ∈ Known
CustomerNo? ∈ Known
RecieveOrder ′= RecieveOrder ∪{ CustomerName?→ CustomerNo?, CustomerNo? →Date?
,StatusReceived,OrderID:OID}
6 | P a g e

Student Number: ________________
In the above notation, we can see the operation of the order where we can see the order and customer
details.
Deliver Message
CalculatePayment
Δ UBER
DriverID? : ID
CustomerID? : ID
CustomerName? : NAME
CalculatePayment?:Amount
Rep!: MESSAGE
ISBN
(CustomerName?→ OrderID?) ∈ Order
Ststus ′=Recieved ∪{ CustomerID?}
Driver ′= Driver ⧹{ DriverID?}
CalculatePayment =Driver⧹{ DriverID?}
Rep!: OK
In the above process, we can see the calculation of payment will be made after the delivery of the food
by the driver and after complete the month cycle, payment will be released by the UBER.
Order Cancelation
7 | P a g e

Student Number: ________________
CancelOrder
OrderID?: OrderID
Status?: Cancel
CustiID?:ID
oo′=oo ⊕{ OrderID? → Status?}
In the above process, customers can cancel the order and after canceling the order, the system will
update status to cancel.
Card Payment
Card_Payment
ΔCC
CVV?:cvvnumber
CardNumber?:Card number
Expriry?:ExpiryDtae
amount ?:N
if CC!=valid
Stop Process
Else
Content + amount ?<= Balance
Contents′ = Balance+amount
Tocken:Generated
8 | P a g e

Student Number: ________________
In the above notation, we can see the card payment process where the user will enter the card number,
CVV, and other details. If the card is valid then it allows you to make the payment otherwise it will be
denied the process.
The schema with consistent and work
With the unified schema, the Z modulation and its intercommunication with the addition of other
objects are designed. We need to check the consistency. Regarding the Z modulator schema, its
configuration semantics defined for above all the checking. This will do if and only if the sequence is
stable along with a Z modulator. We need to mark the semantic associations with accordant Consistency
rules that have been expressed in Z notation.
 In the Z notation plan method, the name in the communication must be fit.
 The corresponding plan must be made with every aim within the representation of Z notation.
 The manipulation of the recipient objects must be related to the information
on the representation of the sequence of Z notation.
Cancel Order
CancelOrder
OrderID?: OrderID
Status?: Cancel
ISBN
bb′=bb ⊕{ OrderID? → Status?}
The canceled order which changes the status of the order is represented in the above example. This is
consistent which changes the status of the order.
9 | P a g e

Student Number: ________________
Schema
Nowadays, the craze of online ordering of food is increasing day by day. UBER is one of the best apps in
this regard. This craze of this app is increasing day by day because of the use of advanced and high
technology. It is very much convenient with the use of the internet. Here we had used Z notation for
providing the blueprint for understanding the requirement and provide the consistency to maintain the
code. Our main goal is to write the Z notation for UBER Company where clients can make the order of
food. We have written the Z notation for creating the company. Our Z notation also represents the
operation for creating the customer details and deleting the same. Our Z notation also represents the
operation for creating the driver details and deleting the same. After making the order from the
customer, the driver picks the order details from the app and calculating the time for picking the food
order from the restaurant and deliver to the customer. The driver will get the payment in a monthly
cycle. Customers can also cancel the order. After receiving the food from the driver system will change
the status of delivery to receive. Z notation is a natural language that helps to understand all the
operations of the UBER Company and helps to manage the operation.
Z specification can be used with the help of the Z tool. This will help to get the targeted goal.
1. New customers can be added with the help of Add Customer schema to the UBER system.
Borrower customers can also be added here by using this schema.
2. Through the UBER, the CANCEL command can change the status of the customers; this will be
done when the client needs to cancel the order.
3. We can search the clients by using the prototype.
Conclusion:
In this assignment, I have written z notation for the UBER system. It is interesting to learn new stuff in
the z notation. We can make it better by adding new features like notification and delivery messages etc.
Z notation also represents the operation for creating the customer details and deleting the same. Our Z
notation also represents the operation for creating the driver details and deleting the same. We know
10 | P a g e

Student Number: ________________
that Uber is a restaurant where customers can make an online order for food and the driver will pick the
location of delivery from the app. After picking the location, the driver calculates the time for picking the
order from the restaurant and time to delivery from the restaurant.
REFERENCES
Ainsworth M., Cruickshank A.H., (2012) , Viewpoint speciation and Z. Inform. Software Technol.
Ainsworth M., Riddle S., Wallis P.J.L. , (2012), Formal validation of viewpoint speciation’s, Software
Eng. J.
Ainsworth M., January 2013 ,Co-refinement, in D. Till (Ed.), Proc. of the 6th Refinement Workshop,
City University, London, January
Arthan R.D., 2012, on free type definitions in Z, in J.E. Nicholls (Ed.), Z User Workshop, York 2012,
Workshops in Computing, Springer, Berlin,
Boiten E, Derrick J., Bowman H., Steen M., March 2012, Consistency and refinement for partial
speciation in Z, in M.-C. Gaudel, J. Woodcock (Eds.), Industrial Benet of Formal Methods, 3rd
Internat. Symp. of Formal Methods Europe, Lecture Notes in Computer Science, Springer, Berlin,
March 2012.
Michael b.,Michael l., Stéphane p. Furthermore Phillip t. 2013, The utilization from claiming formal
systems in the examination of trust. ITrust, pp. 333-339.
John f.& subside l, 2013, Formal determination systems in the business advancement methodology.
ICSE-17 workshop once formal routines requisition for product building act.
11 | P a g e

Student Number: ________________
Anthony H., 2012, Accuracy toward Construction: coordination convention under a business
improvement transforms. FME 2012: formal techniques - Getting it Right, LNCS 2391, Springer, pp.
224-233.
12 | P a g e