Software Engineering Methodologies: Z-Notation Assignment 2

This assignment focuses on applying Z-notation, a formal specification language, to model the Uber Eats system. The solution begins with an overview of the state information and required operations, including user and company registration, cart functionality, payment processing, and order management. The document then defines the state space for users, companies, and drivers and presents schemas for key operations like adding users, companies, and drivers. Further, it includes schemas for looking up phone numbers and removing companies from the database. The assignment also provides a Z specification for card information and explores schema calculus to create a robust lookup schema. Finally, it analyzes potential risks associated with the system, such as location identification failures and driver unavailability, providing corresponding error handling mechanisms. The solution concludes by emphasizing the usefulness of Z-notation in representing predicates, providing calculative solutions, and facilitating the understanding and design of large software systems.

Software Engineering and Methodologies
Z-Notation
Assignment-2
The state information and the operations
that are likely to be needed for the food
order.
Answer A) The state information for the food order is as follows:
The UBER Eats is being developed for the users who are using smart phones and are not
much interested in going out for lunch or dinner. A user wants to have some delicious
food can order at its ease just using his/her smart phone and the UBER Eats driver will
take that order from the desired restaurant and deliver it to user’s doorstep.
The operations that are likely to be needed for the food order are as follows:
1. User Registration: A user needs to first register with UBER Eats by filling a
membership form on UBER Eats App or Website
2. Company Registration: The interested companies can register their business with
UBER Eats so that it can appear in the list of restaurants in App
3. Cart Functionality: The Shopping Cart functionality will be provided in app for the
users to select and add the food to be ordered in to the shopping cart
4. Checkout and Payment: When the user selects and confirms his/her order and
ready to checkout, the payment options will appear and on successful payment the
order is confirmed
5. Receiving Notifications: The restaurant will receive the notification for the order
placed by the user and starts preparing the packet in the due course the driver will
receive the notification with details of the order picking and delivery timings
6. Packing the Order: The restaurant when prepares and packs the order ready to
be picked up updates the status to “Order Ready” so that the driver can come and
take it up for delivery
7. Picking of Order: The driver in the meantime the order is being prepared reach
the restaurant and pick the packet and updates the same in app so that the user
gets the status of his/her order
8. Delivering the Order: Once reached the destination the driver handovers the
order packet to the user and updates the order status as delivered in the app
Ite
m
Schema Explanation Algorithm

A Description for the
state of the system
and presentation in
the Z specification
language
state space description
of the system in Z
specification language
State space for User:
[Name, Email, Phone_no, location]
UserBook
ub: Phone_no ↔Email
ub: Email-> Name, Location
State space for Company:
[Name, Email, Phone_no, location]
CompanyBook
cb: Phone_no ↔Email
cb: Email-> Name, Location
State space for Driver:
[Name, Email, Phone_no, V_number , Area]
DriverBook
db: Phone_no ↔V_number
db: V_number-> Name, Area,Email
B Three possible
schemas for Add
User, Add Driver, Add
Company
When the user selects
and confirms his/her
order and ready to
checkout, the payment
options will appear and
on successful payment
the order is confirmed
Add User:
DUserBook
Name? : NAME
Email? : EMAIL
Phone_no? : PHONE
Location? : ADDRESS
Email? Ï dom(ub)
Phone_no?Ï dom(ub)
user’= user U { Phone_no? ↔ email? -
>name?->location?}
[Name, Email, Phone_no, location]
Add Company:
DCompanyBook
Name? : NAME
Email? : EMAIL
Phone_no? : PHONE
Location? : ADDRESS
Email? Ï dom(cb)
Phone_no?Ï dom(cb)
Company’ = Company U {Phone_no?
↔Email?-> Name? -> Loacation?}
Add Driver:
DDriverBook
Name? : NAME
Email? : EMAIL
Phone_no? : PHONE
V_number ? : NUMBER
Area ? : ADDRESS
V_number Ï dom(db)
Phone_no?Ï dom(db)

Driver’=Driver U{ Phone_no? ↔V_number?
-> Name? -> Area? -> Email? }
C Schema with
description of
function to look up
the number for a
name
Schema describing a
function to lookup the
phone number for a
name
Lookup
Ξ UserBook
name? : Person
Phone_no? : PHONE
Phone_no? ∈ dom(ub)
name = ub(Phone_no?)
D A schema to remove a
company and the
associated
information from the
UBER Eats database
The robust schema to
remove a company and
associated information
from the UBER Eats
database
Remove Company
DCompanyBook
Name? : Person
Email? : EMAIL
Phone_no? : PHONE
Location? : ADDRESS
Phone_no ∈ dom(cb)
CompanyBook’ = { Phone_no? }
CompanyBook
E A Z specification for
card information that
includes the
information about
account numbers,
name, expiry date
and CVV number.
The Z specification for
card information
including the
information about
account number, name,
expiry date and CVV
number
DCardDetailBook
account numbers? : Number
name? : Person
expiry date ? : DATE
CVV number? : Number
account numbers? Ï dom(cdb)
CardDetailBook’ = CardDetailBook U
{ account numbers? -> name? -> expiry
date ? -> CVV number?}

F Schema in Z calculus
to get a robust
version of the lookup
schema.
The Z schema calculus
to get a robust version
of the lookup schema
Lookup
Ξ UserBook
name? : Person
Phone_no? : PHONE
Phone_no? ∈ dom(ub)
name = ub(Phone_no?)
BadLookup
Ξ UserBook
Phone_no? : PHONE
r! : LookupReply
Phone_no? Ï dom(ub)
r!=notKnown
LookupReply == ok | notknown
Success
r! : LookupReply
r! = ok
RobustLookup == (Lookup ∧ Success) ∨
BadLookup
G Extensive analysis of
various risk and
possible way to cater
the risks
The risks those are
involved are:
1. Location of the
customer not identified
2. Restaurant near the
location of customer
does not exits
3. Driver in the area of
deliver or the area of
pickup not available at
that point of time
Error:: ADDRESS UserBook NotKnown |
ADDRESS CompanyDetailBook NotKnown |
ADDRESS DriverBook NotKnown
CheckInOrder :: OrderPlaced|NotPlaced
Known User location:
ΞUserBook
Location? : ADDRESS
error!? : ERROR
Location? ∈ dom(ub)
error!= ADDRESS UserBook NotKnown
UnKnown User location:
ΞUserBook
Location? : ADDRESS
error? : ERROR
Location? Ïdom(ub)
error== ADDRESS UserBook NotKnown
Known Company Location:
ΞCompanyBook
Location? : ADDRESS
error!? : ERROR
Location? ∈ dom(cb)
error!= ADDRESS CompanyBook NotKnown
UnKnown Company Location:
ΞCompanyBook
Location? : ADDRESS
error? : ERROR

Location? Ïdom(cb)
Error== ADDRESS CompanyBook NotKnown
Known Driver Location:
DDriverBook
Area? : ADDRESS
error!? : ERROR
Area? ∈ dom(db)
Error== ADDRESS DriverBook NotKnown
UnKnown Driver Location:
DDriverBook
Area? : ADDRESS
error? : ERROR
Area? Ïdom(db)
Error== ADDRESS DriverBook NotKnown
LocationAll== KnownDriverLocation^
KnowUserLocation^KnowUserLocation
LocationM== KnownDriverLocation v
KnowUserLocation v KnowUserLocation
CheckInOrder =LocationAll V LocationM
Conclusion
Answer I) Conclusively, We understood that how the implementation of Z design in
development of schema is useful to represent predicate and providing calculative
solution for software system in symbolical & logical manner. It also helps us to
understand the large software systems and to develop schema for small parts of a
software system.
END OF ASSIGNMENT – 2