" SOFTWAREENGINEERING Table of ContentsA. State information and the operations for the food order ................................................................ 2B. Mathematical description for the state space of the system and schema in the Z specificationlanguage ....................................................................................................................................................... 3C. Possible schemas for Add User, Add Driver, Add Company .......................................................... 5D. Schema that describes a function to look up the phone number for a name ................................. 6E. Robust schema to remove a company from the UberEATS database ........................................... 8F. Z specification for a card information .............................................................................................. 9G.Z schema calculus to get a robust version of the lookup schema ..................................................... 11H.Analysis of various risk and possible way to cater the risks ............................................................. 12I. Conclusion ......................................................................................................................................... 13References .................................................................................................................................................. 131 A. State information and the operations for the food orderThe application (UberEATS) is an Android mobile app. The UberEATS app is a mealdelivery service app. This app has created with the help of Uber Technologies Inc. that helps toconnect the riders and drivers to use the current network for delivering the meals within minutes.In the preferred cities, such restaurants get the order from the customers for delivering that orderwith this Uber Smartphone Application.For every delivery, the delivery time is less than 10minutes.The UberEATS team in various cities offered the distance limits for customerrequirements. This app automatically changes the "signature items" of each restaurant which hasregistered in this app. Another feature of this app is having celebrity chefs in their pop-uprestaurants.This feature is also preferred for customers when they are ordering the food. Forexample, Michael Mina is one of the partners of UberEATS for promoting his new dishes.UberEATS have 2-4 options for a meal on the daily menu. The UberEATS app is also used fortransportation. The customer can easily use this app with the menu option of this app and directlyorder the items required if the service of UberEATS is available for that area. Every city ofUberEATS has some different options such as lunch, dinner, and brunch. With the help of creditcard, the user can easily pay the charges by using their mobile phone. It is like car service app.Depending upon the place of the customer, they deliver the meals either by cars, bikes or byfoot.("Course CS5232: Formal Specification and Design Techniques", 2017).The system of this app has UberEATS, customers, Uber driver, states, and restaurants.Toorder the foods by the customer through this app, they require the states.When the customeropens this app, he must register his details on this app. The required details of the customer arethe name, address, contact number and credit card details. After completion of registration, thecustomer login to the UberEATS using their personal username and password. Then they orderthe needed food items from the options menu. After getting the customer’s order,all the requestshave given to the nearest Uber drivers for delivery.They also get the alert from the customer directly. In such situations they can contact theselected restaurants by the customer and place the order. If the items are ready, the driversdeliver it to the customer within the time limit("Bangkok Food Delivery - UberEATS", 2017).2 B. Mathematical description of the state space of the system and schema inthe Z specification languageWith respect to the Z specification language, the system of mathematical model haspresented along with the schema. The Z specification language will be supporting theincremental specification and it is built with the use of the schema based on its components. Thepresented schema based on the state space of the system with support towards the incrementalspecification. The schema for the UBER EATS has designed in terms of the following structuresof the schema like schema name, schema signature and schema predicate.+- [ PERSON, ITEM ] +--MESSAGE ::= Ok | Checked | Not_Checked3 ++ UBEREatsusers : P Persondrivers : P Personorder : Item deliver : Locationchecked : Item ? Person|checked = dom order+All the specifications have referred using the schema name that has obtained. Thesignature of the schema declares the name and the types of the entities present in the schema.The relationship of the signature schema has predicted using the logical expression. Thedeclaration made in the schema contains the specification based on the Uber Eats and the termsdeclared in the schema are as follows, users, drivers, order and checked. The first part of theschema describes about the pre-condition success process for the operation. The customer has toregister their name first, then the nearest driver takes the order and checks the order andconfirmsto the customer about the selected item and the whole process has checked thoroughlyfor the delivery of the food for the right person within the specified place within the prescribedtime.(Malik & Utting, 2005).Mathematical DescriptionS € Set of users m users n is one of the user the mathematical description is below:n € {m: S1…..m…..}? n € S ^(….n….)d € {n: Checked/Order(n)=Item? / Driver = New Location?}? d € Checked ^ Order(n) = Item? ^ Driver = New Location? The ‘€’ describes the state that does not change. The ‘n’ will be determined as one of theusers. The ‘d’ implies the delivery of the item also with some conditions present it, namely thelocation, item status and driver details. At last the delivery begins with respect to the orderfinalizing and the nearest location where the driver will be available(Saiedian, 2007).4 C. Possible schemas for Add User, Add Driver, Add CompanyWith the help of following schema, the customer can easily add their details in theUberEATS app:The alerts of UberEATS are declared by ?UberEATS which helps to show the state ofchange. This schema introduces two different variables for adding new users such as users andusers'. The first variable is used for state observations before changing the states and the secondone is used state observations after changing the states. These variables must contain both theoperations before and after which is entirely forced to fulfill the need of the user. In thedeclaration the question mark is added by convention. The pre-condition is defined for successfuloperation. The condition is each person must have one user name to access the application. If thecondition is not satisfied, the details are not shown on the application. It also shows the errormessage which is produced from this app itself. If the condition is satisfied, the second lineshows the function of new users to the given location.+AddUser?UBEREatsname? : NAMElocation? : LOCATION|name? ? usersusers' = users ? {name? ? location?}++ AddDriver?UBEREatsname? : NAMEvalid license? : VALID LICENSEability to drive? : ABILITY TO DRIVEappropiate age? : APPROPRIATE AGE|name? ? driversdrivers' = drivers ? {name? ? valid license? ? ability to drive? ? age?}++ AddCompany?UBEREatsname? : NAMElocation? : LOCATION5 funtion? : FUNCTION|name? ? companylistcompanylist' = companylist ? {name ? function?}+The declaration of ?UberEATS alerts helps to describe change in state. It consists of twovarious variables. There are Driver and Driver'. Driver variable is chosen for before state changeand Driver' variable is chosen for after state change. Both of the variables are indirectly forcedfor satisfying the user in before and after operations. The question mark is used for declaring theoutputs. In this schema, two pre-conditions are used for completing the operations successfully.The conditions of each person should have the valid license and correct age. If any of theseconditions are not satisfied, they can’t utilize this app and get the error message. If it is satisfied,they utilize this app by the function of a second line in the schema(Dongmo & Poll, 2011).In the company schema, it also has two variables for state change. The variables arecompanylist and companylist' which are used for the observations of the state before and afterchanging respectively. It checks the existing company list with the added list. If it is new, it addsthe company list into the existing list. Otherwise, it neglects it.D. Schema that describes a function to look up the phone number for a nameEvery Driver in the Uber has the details of the customer for delivering their orders. Thedetails of the customer must include the name of the customer, items ordered by the customerand contact details of the customer. At the time of delivery the Uber Driver must check the exactdetails of the customer before delivering the food items. For verifying the customer details, theUberEATS uses the Phone Book System. This system helps to contact the customer, when theDriver reaches the customer’s location. This schema consists of two different variables which areknown and phone number. The first variable known is used to identify the customer fordelivering the food items ordered by them. The second variable is used to get the domainvariable. The domain variable is ‘Known = dom ph.no’.+AddUser?UBEREats6 name? : NAMElocation? : LOCATION|name? ? usersusers' = users ? {name? ? location?}++ AddDriver?UBEREatsname? : NAMEvalid license? : VALID LICENSEability to drive? : ABILITY TO DRIVEappropiate age? : APPROPRIATE AGE|name? ? driversdrivers' = drivers ? {name? ? valid license? ? ability to drive? ? age?}++ AddCompany?UBEREatsname? : NAMElocation? : LOCATIONfuntion? : FUNCTION|name? ? companylistcompanylist' = companylist ? {name ? function?}+The Phone Book state space system has two different states such as success and failure.Phone number and the order details of the customer are important while delivering the fooditems by the Driver. Some verification is needed for delivery. So when the driver has the contactnumber of the customer, it will be easy for driver to deliver the food items. Then the process isdeclared as successful. If the food items are not delivered to the customer properly, the process isconsidered as failure. In case the driver can’t get the details of the customer, the process will bestopped. The pre-condition of this schema is the failure state is assigned, if the driver can’t getthe contact number of the customer. If the customer verification is failed, the process isstopped(Jusoh, Md Saman, & Man, 2015). 7 In Not known operation, the name and reply are the variables which are used to show thedriver can’t get the details of the customer. This operation shows the message that is ‘failure tofetch’ and it stops the process. Duringa successful operation, the reply is only one variable forindicating the process as success. It shows that the process is ‘Ok’ and it declares the process issuccessfully completed(Dr. A.K.Sharma, 2013).E. Robust schema to remove a company from the UberEATS databaseThe Z schema is used to define the dynamic and static features of the system. The staticfeature covers the states and supports the relationship of all the invariants which are specified inevery state. It easily changes the states, from any state in the system. The dynamic feature coversall the available operations, which are present in the system and support the input and outputrelationships of the system. The dynamic feature is specified as the state change in this system.This schema is also used for replacing the state of transformation. The pre-condition is describedto do the particular operation. Functionality is examined with the help of thisoperation(Farahbod, Gervasi, & Glässer, 2014).+ CompanyList?UBEREatsknown : P NAMElocation : NAME ? LOCATION? FUNCTION|known = dom location++ Remove?CompanyListname? : NAME|location' = {name?} ? location+This UberEATS app is developed for managing the company database. Every companyconsists of the contact details of the labors and restaurants which supplies the food for thecustomers. This database is acting as a state space system. The state variable of this schema isUberEATS. The available variable is PName and Location. The variable PName is used to showthe partner’s name. The variable Location is used to show the location of the company. The8 PName variable input is used to assign the location of the company. If the partner’s details areretrieved from the database, the name of the company is not enough for getting the fullinformation about the partner. The database should be modified according to the number ofcustomers. The Domain is mentioned as Location.The remove schema has designed to remove the information of the company and deletethe whole database about that company. The partnership company links are also deleted, if thecompany remove their relationship with the UberEATS. The function of a company’s databasecontains a single variable such as NAME, this variable is mentioned as declaration variable. Thecompany details are deleted from the database by inserting the variables such as NAME andLocation'. The company details are searched by using the Location' variable. This is used toshow the location of the company that matches with the input given.Finally, it removes thedatabase from the list.F. Z specification for a card informationThe customers should pay the bill for their order before delivering the ordered fooditems. They can’t pay instant cash, only through online transaction. For online transaction, thecard details of the customer must need. So the separate schema was created that is card schema.The card schema is used for getting the details of the customer’s credit card. These details mustcontain the customer’s name, account number, expiry date and CVV number. It is not easy toidentify the customer through their card number. So the name and other details are included inthat schema. The detail function is used for collecting the information on customer’s card. Thedetail is used as a domain variable which is given below(Smith, 2017).Known = dom Detail+ CarInfoknown : P CARDNUMdetail : CARDNUM? NAME? EXPIRY DATE ? CVV NUM|known = dom detail++ AddCardInfo?CardInfocardnum? : CARDNUM9 name? : NAMEexpiry date? : EXPIRY DATEcvv number? : CVV NUMBER|cardnum? ? detaildetail' = detail ? {cardnum? ? name?? expiry date? ? cvv number?}++ FindCard?CardInfocardnum? : CARDNUMdetail !: DETAIL|cardnum? ? detailname != detail {cardnum?}++ Remove?CardInfocardnum? : CARDNUM|detail' = {cardnum?} ? detail+ The declaration of ?CardInfo alerts helps to define the state change. The variables of thisschema are known and Detail'. Known variable is taken as a pre-condition which is verified it isalready existed or not for getting information. If the customer’s name is verified successfully, thedetails of the customer are received by this schema.The Detail' variable is used for collecting theinformation on the customer’s card. The find card schema is used to identify the customer’s card details in the whole list. Theknown variable and the name' variable are described for determining the information. If the cardnumber is inserted in this schema, the name of the customer will be displayed in theapplication.It is very helpful for the owners to find whose card number is this. Known variable isused to get the card number and name' variable is used to display the customer’s details. This schema was created for removing the card details of the customer in the list. Itconsists of a single variable such as Detail'. This variable is used to delete the card details of thecustomer by getting the input as card number(Saiedian, 2007). 10 G. Z schema calculus to get a robust version of the lookup schema With the help of Z schema calculus, the lookup schema was created in the robust version.For making the robust version, this lookup schema was created to expand the lookup operation.This schema was created to identify the customer’s name by giving the card number as input. Byusing Card Info schema, the customer details can be easily detected. So the lookup schema haseasily identify the name of the customer. Name has taken as a variable in this schema. If thecustomer enters the correct card number, it shows the name of the customer. The domainvariable of this schema is given as follows:Name? ?dom (Detail)+ LookUp?CardInfocardnum? : CARDNUMname !: NAME|name? ? dom (detail)++ BadLookUp?CardInfocardnum? : CARDNUMr != Lookup Reply|name? ? dom (detail)r != notknown ++ Successr !: result|r !: 'ok'+ The bad lookup schema has created for showing the reply of failure in lookup schema.This schema consists of two variables such as name and r. The variable name is used to check, ifthe name existsin the list of the customer while checking the details by using card number. Whenthey enter the unknown card number of the customer, it replies the statement as ‘not known’. The11 r variable is used to show the statement. The lookup operation using the robust version, then it iscalled bad lookup(Haghighi & Afshar, 2012). During successful operation, the r is the only variable for indicating the process assuccess. It shows that the process is ‘Ok’ and it declares the process is successfully completed. Ifthe lookup operation is successful, it goes to success operation.H. Analysis of various risk and possible way to cater the risksThe Z specification language has a large set of symbols. The structure is too complex tounderstand. There are lots of symbols used in the Z specification language. They are materialfunction, Enumeration (e1, . . .,en),element-of-relation ( ?),Union ( ?), Abbreviation,Conjunction ( ?), Equivalence( ?). It should be given as a clear mathematical expression. Thefunctions of each schema are based on the notations of Z specification. The Z notations havecomplex symbols so it cannot be understood easily. Because of its complexity, the functionalpart of the schema will be affected. In Z notation, only less amount of tools used. So thefunctionality risk has increased to specify the functions. The quality, time effective and cost hasreported at high risk. CICS has many specification properties. The execution delay is one ofthem. But the Z notation does not handle this property(Katz, 2017).The design of the Z specification language is more expressive and so the complexityincreases. This complex design is understood by computer only. The humans cannot recognizethe notations and its complex design easily. So the design becomes a threat for the Z notation.Thus the notation is not easy to understand and it leads to high risk. The requirements ofspecifications calculated by using software. So the manual calculation is impossible to generatecode.Possible ways to deduct riskZ notation is not a well-known language, but it is used within a working environment. Aformal method is used to overcome this problem. The Z specification language is a combinationof unifies modelling language, Object Constraint language and Object modelling language. TheEntity relationship diagram is used for modelling. The given input is recognized as ASCII file byusing CADIZ, in Eclipse software. This file contains instructions to use Z Specificationlanguage. By examining the file performance, the required specifications are verified. In the12 software engineering process the Z notations are initiated. So, the exceptions are handledimplicitly(Zeller, 2009).I. ConclusionThe state space system for UberEATS application is analyzed. In food ordering systemthere are lots of operations are performed by the customer, Uber driver, Restaurant and UberCompany. These operations are managed by mobile phones. The operations performed in thestate space of this system represented as the schema by using Z specification language. TheMathematical description of the states of customer, driver, company database and phonebook isderived. The UberEATS payment process has analyzed and the operation has performed by usingthe account number, name of the account holder, expiry date of card and CVV number. Theschema which was developed for this operation uses Z notations. While performing a food orderand payment operations, various risks are identified based on its function and design. Thus the Zspecification language is learned in an easiest way.ReferencesBangkok Food Delivery - UberEATS. (2017). Ubereats.com. Retrieved 21 January 2017, fromhttps://www.ubereats.com/bangkok/Course CS5232: Formal Specification and Design Techniques. (2017). Comp.nus.edu.sg.Retrieved 24 January 2017, from https://www.comp.nus.edu.sg/~dongjs/ic52z5.htmlDongmo, C. & Poll, J. (2011). Toward The Formalisation Of Use Case Maps. University OfSouth Africa.Dr. A.K.Sharma, D. (2013). Comparison of the Formal Specification Languages Based UponVarious Parameters. IOSR Journal Of Computer Engineering, 11(5), 37-39.http://dx.doi.org/10.9790/0661-1153739Farahbod, R., Gervasi, V., & Glässer, U. (2014). Executable formal specifications of complexdistributed systems with CoreASM. Science Of Computer Programming, 79, 23-38.http://dx.doi.org/10.1016/j.scico.2012.02.001Haghighi, H. & Afshar, M. (2012). A Z-Based Formalism to Specify Markov Chains. ComputerScience And Engineering, 2(3), 24-31. http://dx.doi.org/10.5923/j.computer.20120203.0413 Jusoh, J., Md Saman, M., & Man, M. (2015). Formal Specification Approach In DesigningDatabase System Using Z. ARPN Journal Of Engineering And Applied Sciences, 10(3).Katz, S. (2017). The Schema Calculus.Khalafinejad, S. & Mirian-Hosseinabadi, S. (2013). Translation of Z specifications to executablecode: Application to the database domain. Information And Software Technology, 55(6),1017-1044. http://dx.doi.org/10.1016/j.infsof.2012.12.007Malik, P. & Utting, M. (2005). CZT: A Framework for Z Tools. The University Of Waikato,Hamilton, New Zealand.Saiedian, H. (2007). Developing Formal Specifications in Z. University Of Kansas.Smith, G. (2017). The Object-Z Specification Language. Software Verification Research Centre.Stacewicz, P. (2015). Evolutionary Schema of Modeling Based on Genetic Algorithms. StudiesIn Logic, Grammar And Rhetoric, 40(1). http://dx.doi.org/10.1515/slgr-2015-0011Ulfah Siregar, M. (2016). Support for Model Checking Z Specifications. Information Reuse AndIntegration (IRI).Ulfah Siregar, M., Derrick, J., North, S., & J. H. Simons, A. (2015). Experiences usingZ2SAL. Advanced Computer Science And Information Systems (ICACSIS).Utting, M., Malik, P., & Toyn, I. (2010). Transformation Rules for Z.What is Z?. (2017). Staff.washington.edu. Retrieved 21 January 2017, fromhttps://staff.washington.edu/jon/z-book/what-is-z.htmlWoodcock, J. & Davies, J. (2017). Using Z Specification, Refinement, and Proof. University OfOxford.Z lecture notes: Schemas and Schema Calculus. (2017). Staff.washington.edu. Retrieved 24January 2017, from https://staff.washington.edu/jon/z-lectures/schema.htmlZeller, A. (2009). Formal Specification with Z. Saarland University.14 15 "