" SOFTWAREENGINEERINGThe UberEATS application helps the customer to buy food items without leaving theirhome. The Uber drivers bring the food items which are ordered by the customers, which isavailable in the restaurants near to their area. The food ordering system module gives thefunctionality for the customers to place orders. When opening this app, all the newcustomersmust create their account in the website. So that, they can manage their account bythemselves. The customer must login to their account to order the food items and they need tospecify their location to deliver their food items.To place the order, they need to login and theycan enter the food items which they need. Thus, the required food item is delivered by the Uberdrivers. The notification regarding the customer who has ordered the food will be received viaUberEATS Application to the Uber drivers. The Uber drivers login their account to know thedetails about the ordered food and location of the customer to deliver their order. The websitefacilitates to create a new account for new drivers. The drivers are well talented to deliver the1 order within a short period of time. When the driver login to their account, they will receive thenotification. The driver accepts the trip and gets the food from the restaurant which is near to thecustomer?s location. The order Id is used to contact the customer to configure their deliverydetails. The orders will be delivered to the customer within 30 minutes. So, the customer neednot leave their home to eat their favorite restaurant food items("Bangkok Food Delivery -UberEATS", 2017). Z schema The schema refers to the specifications. From the ingredients, thespecifications are built.The usage of the specifications are to introducethe state variables, the state operation and theconstraints. Various operations of Schema comprises hiding, renaming the schema and theschema composition. Schema is a powerful implementation to describe the system specifications.The design of the schema is represented below. Figure 1 : Schema specifying a containerFigure 2 : Specification of an indicatorThe schema signature describes the entity and name introduced in the schema. In fig. 1,the introduction of the two state variables is provided. It is indicated by the natural numbers. Itshould be an integer. The range of natural number should be zero or greater than zero. The entityrelationship is established by a logical expression. The expression is always an invariant. Figure2 2 building block is corresponding with a container which provides the details of the contents.Three entities are introduced in the fig 2 named as light, danger_level and reading. In the realsystem, reading and light have physical demonstration. The system gives the informationtogether with an operator(Abbasi, 2017).Figure 3 : Storage Tank+ UBEREatsknown : P NAMEorder : USER NAME ? ITEM driver : NAME ? LOCATION|known = dom order+In Z specification, the symbol „ ?? gives the meaning as 'if and only if'. It is also equal todanger_level. The combination of the container and the indicator defines the specifications ofstoring tank. It has indicator light and some capacity. The conventions used by Z language isused to find the state variable and the specified type of schema.? If the variable name is ' followed by N (N'), it indicates the state variable value Nnext to the operation.? The name of schema is furnished with '. It initiates the dashed values of all thenames which are declared in the Z specification. ? The name of variable which ends with “!”, refers to the output. (Eg: income!'). ? The name of variable furnished with “?”, gives the meaning as input. (Eg:'name?')3 ? The Greek character used in Z specification is named as Delta (?), it gives themeaning as changing the values of one or more state variables("DevelopingFormal Specifications in Z", 2017).Mathematical ExpressionThe system specification includes the information about all the customer names and theitems they ordered. [NAME, ITEM]. This is a simple description about the objects. The main feature of the system is to narrateits state space with the schema. Normally, the schema contains a single part and the dividing linespecifies the correlation of the given variables. The description of the variables in UberEatsschema are discussed below,i. Known –It contains the names with corresponding items they ordered.ii. Order - It is a function. When a particular name is given, it provides the item details.iii. Driver - This function predicts the location for the specified user name.The centered line provides the correlation which is true in all the system states. Thedomain of the function “Order” is placed in the set “Known”. The system needs a valid name.Relationship is a steady state of the system. The value of “Known” is to be obtained from thevalue of “Order”. The derived component is to specify the system without specifies the variable“Known”.[NAME, LOCATION]The Driver function includes the location under Driver for the particular name.Theschema can be expressed in a mathematical form.Known'= known? {name?}The above expression describes the domain of the function known unioned after verifyingthe name with the set of user name state space. The name is specified in Add User, then using thesteady state confirm the specification accuracy.Known' = dom order' = dom (order ? {name? ?item?}) This expression is to denote that the driver needs to deliver the item ordered by aparticular user. Set of users {x:S|...x...}...y...4 In the input, it contains a set of users named as x.In that, y is the member of the set{x:S|...x...}. If y is a member of S, then the condition ...y..., is acquired by changing x with y. So, y ? {x:S|...x...}? y ? S ? (…y…)("Introductory Notes on Specification with Z",2017).Deliver the orderThe above expression states that, in a set of user, find a particular user y. From this, thedriver delivers the items ordered by the customers. In this system, the customers will be theregistered users.So, in this system state, m ? {n :known | order(n) = nearby driver in that location?} ?m ? known? order(n) = nearby driver in that location?If m is in output set of users!, then the system known and the order of the items is recorded bythe user. From the specified location, the driver who is located nearly, will deliver the order. The state space of the system describes the increasing count of the customer.In thisschema, the invariants which are declared allows the value of the known variable which isderived from the UberEATS values. So that, the known values are the components of the state. These variables are used to specify the known variable without using any keyword of Known. Itspecifies the known state components. All the derived components are mentioned in the aboveformat. Because, it is important to give names to all the variables in a system. To identify thefunctionality of the system, it is necessary to assign the objects to call the functions. So, it makesmore readability when describing the abstract view of the given state space system. Thedeclaration of the variables is done explicitly during implementation("Model-based 11Specification", 2017).AddUser The invariants which are declared as known are satisfied in the condition of addUser. The count of the customer or user will be assigned for the known values. Thus, it is easy to makea premature decision on the attributes of the users. While taking decision, the two customers did5 not have same account details for payment. But, the user and their address is accepted by thedriver. The decision is taken based on the condition of the name and the location of the customer. +AddUser?UBEREatsname? : NAMElocation? : LOCATION|name? ? knownorder' = order ? {name? ? location?}+ In this state space of the system, the known variables are Name and Location of thecustomer. While making decision, the name is verified in known details. It is described in theaddUser schema. The declaration part of UBEREATS gives an alert for the state change. Here,the customer or the user are in the active state. It introduces four variables. They are known,order, known' and order'. The first two variables are observation elements after the state change. The invariant variables are satisfied by using each pair of the above mentioned known variables.The variables are implicitly mentioned in the declaration part.AddDriver+ AddDriver?UBEREatsname? : NAMEage? : AGEvalid license? : VALID LICENSEhealth? : HEALTH |name? ? knownknown' = known ? {name? ? age? ? valid license? ? health?}+6 The schema description of AddDriver, represents the state change in UBEREATSsystem. The variables name, age, valid license, health are invariants. These invariants aredeclared at top part of the schema. The state change part introduces four variables. They areknown, Drivers, known', Drivers'. The pre-condition is given at the bottom of the schemaoperation. The name, age, license and Health is verified and the intersection operation isperformed with the Driver state.AddCompany+ AddCompany?UBEREatsname? : NAMElocation? : LOCATION|name? ? companiescompanies' = companies ? {name ? location?}+The AddCompany Schema describes the state change of the UBEREATS system. Theinvariants are name and location of the company. The state change part contains the variablessuch as, companies and companies'. The precondition is predicatedby using the name andlocation of the company state.PhoneBook+ PhoneBookknown : P NAMEphone number : NAME ? NUMBER|known = dom phone number+7 The UberDriver has phonebook which contains the details like customer name, ordereditems and contact information. While delivering the food items to the customer, it is necessary toverify that the items were ordered by the customers. To implement the verification process,phonebook is used. The contact details of the customer are stored in the phonebook so it is easyto get the customer details during the food delivery. In the PhoneBook schema, there are twoinvariants introduced such as known and phonenumber. Known variable is assigned for thecustomers who ordered the food and phone number is assigned to contact them while deliveringthe food. In state change of the phone book, the domain variable is assigned to phone numbers asshown below. Known = dom phone number Success+ Successrep !: report|rep !: 'okay'+The state space system of PhoneBook has two types of state. They are success andfailure. When driver gets report of the customer such as, phone number to deliver food, he mustverify the order details from the customer. So, some condition is needed for verification. If thecontact number of the customer is available in the report then, the delivering process will bedone successfully. Otherwise, the delivering process will be reported as failure. If the driverdoesn?t not get any details then, the delivery of the food item is stopped. The precondition of thestate is defined as the below mentioned condition. If the phone number of the customer is notfound in phonebook, then failure state is assigned. This state change describes that the driver didnot get the phone number of the customer. So, the verification is failed and then the deliveryprocess is halted.NotKnown+ NotKown?PhoneBookname? : NAME8 rep !: REPORT|name ? knownrep != 'name not known'+The specification of the NotKnown operation is described using two variables such as,name and rep which represents report. The predicate is that the name doesn?t not belong to theknown variable then it will report as „name not known? and then it will be halted. Another stateis Success operation. In success schema, it describes one output variable which represents thebehavior of the report. A string „okay? is assigned to a variable when the customer name isfound. So, it signifies a successful operation(Shyamasundar & Ramesh, 2010).CompaniesDBThe Z schema describes both static and dynamic aspects of the system. In the staticaspect, it occupies the states and maintains the relationship among all the invariants which aredeclared in each state and it can change from any state to any state. In dynamic aspect, allpossible operations are present and it maintains the relationship among the input and output ofthe system. The changes of the state is considered in the dynamic aspect. So that, the schema isused to represent the transformation of the state. For each instance, the pre-condition is definedto perform the desired operation. Based on the operation, the functionality is analyzed("StudentDatabase in Z Notation", 2017).+ CompaniesDB?UBEREatsknown : P NAMElocation : NAME ? LOCATION |known = dom location+9 The UberEATS application has been managing the company database. The companymaintains contract with the workers and restaurants for food supply. For company, database isassigned as the state space of the system. The UBEREATS is defined as the state variable. Theknown variable is „pname? and location. The „pname? represents the name of the partner and thelocation represents the place of the company which is located. The location is fully dependent onthe name variable input. When retrieving the partner?s details, the name of the company isenough to get further information. So, the precondition of the company is that there is need tomodify the database according to number of the partners. Thus, the location is assigned asdomain.Remove+ Remove?CompaniesDBname? : NAME|location' = {name?} ?location+To remove the database of the partner?s companies, the Remove schema is described.When contract between the companies is over then, the partnership company is removed fromthe Uber Company?s database. In companiesDB state function, Name is a variable which isintroduced at declaration part. At precondition, the attributes such as, Name and correspondinglocation are given as the inputs and then are removed from the companies? database. The abovementioned schema is used to search the name of the company based on its location. It displaysthe companies? location which is matches to the input Name. The power set of Name is a returntype. Because, it returns not only single Name.AccDetails+ AccDetails10 known : P ACC NUM \\ info : ACC NUM ? NAME ? CVV NUM ? DATE OF EXPIRY|known = dom info+For payment process, each customer has their unique account number. In accountdatabase, the duplication is not allowed. The account number, name of the account holder, expirydate of card and CVV number of the card are the attributes which are stored in the Accountdatabase. But, the name of the account holder is a partial function. This known variable maps theCVV number and Dateof Expiry. The specification should be simple. So, the Name is declaredwithout any complex. Thus, it is possible to assume the details of the account number, name,CVV number and expiry date. The initialization should be in an exact form. The preconditionstatement is that the Info is considered as domain of the state and it is assigned to the Knownvariable.AddAccDetails+ AddAccDetails?AccDetailsacc num? : ACC NUMname? : NAMEcvv number? : CVV NUMBERdate of card expired? : DATE|acc num? ? detailinfo' = info ? {cardnum? ? name? ? cvv number? ? date of card expired?}+ The AddAccDtetails schema specification describes the verification of the accountinformation. The variables AccNum, Name, DateofCardExpiry and CVV Number. The Zspecification is evaluated for the state space system. Some operations such as adding newcustomers account to the database can be performed using Z specification language. The11 precondition of the state is to verify the valid account number and account holder. Also the CVVnumber and Expiry date is examined for each account holder. If the verification is valid, then theInfo is retrieved through the Set Operation of Union.FindCard+ FindCard?AccDetailsacc num? : ACC NUMinfo !: info|acc num? ? infoname != info {acc num?}+ The FindCard schema describes the functionality of finding the card number of theaccount holder using the Account number. The variables are Info and AccNum. The preconditionis getting the Name of the account holder through the Account number. The account number isunique for all the customers. So, it is easy to calculate the account information by using therefinement of specifications. It facilitates the searching process while delivering the food items tothe customer. The customer must make payment by using their card number, account numberand CVV number. Thus, it is easy to retrieve the information from the Account details database.The Z specification is explained to find the card details.+ LookUp?PhoneBookname? : NAMEnumber !: NUMBER|number? ? dom (Phone Number)number != Phone Number (name?)12 ++ BadLookUp?PhoneBookname? : NAMErep != Lookup Reply|name? ? dom (Phone Number)rep != notknown ++ Successrep !: LookupReply|rep !: 'ok'+Look up schema has the name of member which includes the phonebook entry relatedwith a particular name. For the operation of lookup, input of (entry!)Phonebook details arelinked with the name?. The Error can occur in this lookup operation when the given name is notpresent in the phonebook. In the lookup schema, the phone number (name?) provides that thephone number is linked with the name?. A large schema can be built by the Schema calculusfrom the smaller schemas. This lookup is valid only if the phone number is a partial function andname? ?dom (phone number)("The Schema Calculus", 2017).The error can occur if name? ?dom (phone number).The extension of the lookup operation will be performed to make the robust version of thelookup operation. It provides a success indication message. Success lookup is executed and givesthe result r! = ok. LookupReply == ok | notknownRobustLookup ==BadLookuup ? (Lookup ? Success)13 In lookup schema, after the centered line portion describes a group of observations. Theseobservations states the relationship between the variables. In lookup operation, the state variableis invariant by the Lookup operation.The schema calculus gives a notation. It expresses the difficult schema to be dense. Thefirst line of the output value is associated with name?. The second line input is associated withnumber!. The information is not changed by the operation of Lookup schema(The Object-zSpecification Language, 2013).Functional risk The major risk in the Z specification language is the large and complex set of symbol?susage. The set of symbols are widely used in the Z specification language, which is materialfunction, Union ( ?), element-of-relation ( ?), Abbreviation, Enumeration(e1, . . .,en),Equivalence( ?), Conjunction ( ?).The mathematical expression should be clear. The functionsare based on this Z notations. But, the understanding of the Z notation is the major issue. Due tothis, the functional part will be affected. It uses less amount of tools, which cause the function ofspecification. The cost, quality and time effectiveness are reported. The execution delay is one ofthe property of CICS. This property cannot be handled by the Z notation("The Z Notation",2017). Design Risk The expressive design of Z notation also produces complexity.Instead of usingcomputer, the design understanding by the human is not an easy task. Design of Z notation usingthe software induces the threat. The Z language Specifications cannot be easily understood. Byusing software, the requirements of the specifications can be taken. But, the automaticconversion is not possible for the generated code.Possible way to cater the risksZ notation is used within a working environment that is not a widely known language. Toovercome this, a formal method can be used. This Z specification language is a compound of thefollowing languages such as Object constraint language, object modelling language and theunified modelling language. The modelling can be done through ERA (Entity RelationshipAttribute) Diagrams. 14 By using CADIZ, the given input is taken as ASCII file. Various instructions about Zschema are presentin this file. The specifications are checked by the file performance.Z methodspecifications are initiated for a Software engineering process. The exceptions can be handledonly implicitly("Z SPECIFICATIONS & THE SCHEMA CALCULUS", 2017).ConclusionThe study of Z notation specifications, list of operations, functions is discussed. Softwaresystem is understood to develop the schema. The UberEATS functions are done using the statespace schema. Development of Various schema process are completed. The formal design isused in Z notation. The development of schema for the food selection from the suggestedcompanies, is delivered from the company side through the Uber driver and various functions areadded. The mathematical expressions are derived for the state space using Z specificationlanguage. The schema for add user, add driver, add company are written. From the UberEATSdatabase, the card information specifications are produced. Using the schema calculus, thelookup schema robust version is obtained. Various risks occurred in Z specification language areanalyzed. The easiest way is learnt to understand the Z specification language.References Abbasi, M. (2017). A Comparative Analysis of Formal languages Based upon VariousParameters. Academia.edu. Retrieved 21 January 2017, fromhttps://www.academia.edu/9632567/A_Comparative_Analysis_of_Formal_languages_Base d_upon_Various_ParametersBangkok Food Delivery - UberEATS. (2017). Ubereats.com. Retrieved 21 January 2017, fromhttps://www.ubereats.com/bangkok/Comparing Specification Paradigms: Gypsy and Z. (2017). ftp://ftp.cs.utexas.edu/. Retrieved 21January 2017, from http://ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/045.pdfDeveloping Formal Specifications in Z. (2017). eecs.ku.edu. Retrieved 21 January 2017, fromhttps://people.eecs.ku.edu/~saiedian/Teaching/Fa09/814/Lectures/z.pdf15 Introductory Notes on Specification with Z. (2017). http://www.bowdoin.edu/. Retrieved 21January 2017, from http://www.bowdoin.edu/~allen/courses/cs260/readings/ztutorial.pdfModel-based 11 Specification. (2017). https://ifs.host.cs.st-andrews.ac.uk. Retrieved 21 January2017, from https://ifs.host.cs.st-andrews.ac.uk/Resources/Notes/FormalSpec/ModelSpec.pdfShyamasundar, R. & Ramesh, S. (2010). Real time programming (1st ed.). Singapore: WorldScientific Pub. Co.Student Database in Z Notation. (2017). Retrieved 21 January 2017, fromhttp://www.dainf.ct.utfpr.edu.br/~adolfo/Disciplinas/LogicaParaComputacao/4.Especificaca o/Exemplos/z/StudentDB.pdfThe Object-z Specification Language. (2013) (1st ed.).The Schema Calculus. (2017). http://webcourse.cs.technion.ac.il/. Retrieved 21 January 2017,from http://webcourse.cs.technion.ac.il/236368/Spring2009/ho/WCFiles/2-zedschemas.pdfThe Z Notation. (2017). https://www.cs.umd.edu. Retrieved 21 January 2017, fromhttps://www.cs.umd.edu/~mvz/handouts/z-manual.pdfZ SPECIFICATIONS & THE SCHEMA CALCULUS. (2017). Retrieved 21 January 2017, fromhttp://www.cs.ox.ac.uk/people/michael.wooldridge/teaching/soft-eng/lect12.pdf16 "