#LyX 2.2 created this file. For more info see http://www.lyx.org/ \lyxformat 508 \begin_document \begin_header \save_transient_properties true \origin unavailable \textclass article \begin_preamble \usepackage{listings} \usepackage{xcolor} \usepackage{pdflscape} \usepackage{courier} %\usepackage{mathtools} \usepackage{graphicx} \usepackage{booktabs} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage{listings} \lstset{columns=fullflexible} \usepackage{charter} \usepackage{xspace} % Definizione intestazioni e pie' di pagina \usepackage{fancyhdr} \end_preamble \use_default_options true \begin_modules InStar graphicboxes fix-cm fixltx2e fixme customHeadersFooters pdfform \end_modules \maintain_unincluded_children false \begin_forced_local_layout Format 60 Style "In Preamble" Category "FrontMatter" Margin Static LatexType Paragraph InTitle 0 InPreamble 1 TocLevel -1000 NeedProtect 0 KeepEmpty 0 NextNoIndent 0 CommandDepth 0 LatexName "dummy" ItemCommand item LabelType No_Label EndLabelType No_Label ParagraphGroup "0" ParIndent MM ParSkip 0.4 ItemSep 0 TopSep 0 BottomSep 0 LabelBottomSep 0 ParSep 0 NewLine 1 Align Block AlignPossible Block, Center, Layout, Left, Right FreeSpacing 0 PassThru 0 ParbreakIsNewline 0 RefPrefix OFF HTMLLabelFirst 0 HTMLStyle div.standard { margin-bottom: 2ex; } EndHTMLStyle HTMLForceCSS 0 HTMLTitle 0 Spellcheck 1 ForceLocal 1 End Style "In Title" Category "FrontMatter" Margin Static LatexType Paragraph InTitle 1 InPreamble 0 TocLevel -1000 NeedProtect 0 KeepEmpty 0 NextNoIndent 0 CommandDepth 0 LatexName "dummy" ItemCommand item LabelType No_Label EndLabelType No_Label ParagraphGroup "0" ParIndent MM ParSkip 0.4 ItemSep 0 TopSep 0 BottomSep 0 LabelBottomSep 0 ParSep 0 NewLine 1 Align Block AlignPossible Block, Center, Layout, Left, Right FreeSpacing 0 PassThru 0 ParbreakIsNewline 0 RefPrefix OFF HTMLLabelFirst 0 HTMLStyle div.standard { margin-bottom: 2ex; } EndHTMLStyle HTMLForceCSS 0 HTMLTitle 0 Spellcheck 1 ForceLocal 1 End \end_forced_local_layout \language english \language_package default \inputencoding auto \fontencoding global \font_roman "default" "default" \font_sans "default" "default" \font_typewriter "default" "default" \font_math "auto" "auto" \font_default_family default \use_non_tex_fonts false \font_sc false \font_osf false \font_sf_scale 100 100 \font_tt_scale 100 100 \graphics default \default_output_format default \output_sync 0 \bibtex_command default \index_command default \float_placement H \paperfontsize default \spacing single \use_hyperref true \pdf_bookmarks true \pdf_bookmarksnumbered false \pdf_bookmarksopen false \pdf_bookmarksopenlevel 1 \pdf_breaklinks false \pdf_pdfborder false \pdf_colorlinks false \pdf_backref false \pdf_pdfusetitle true \papersize default \use_geometry true \use_package amsmath 1 \use_package amssymb 1 \use_package cancel 1 \use_package esint 1 \use_package mathdots 1 \use_package mathtools 1 \use_package mhchem 1 \use_package stackrel 1 \use_package stmaryrd 1 \use_package undertilde 1 \cite_engine basic \cite_engine_type default \biblio_style plain \use_bibtopic false \use_indices false \paperorientation portrait \suppress_date false \justification true \use_refstyle 1 \index Index \shortcut idx \color #008000 \end_index \leftmargin 2.5cm \rightmargin 2.5cm \secnumdepth 3 \tocdepth 3 \paragraph_separation indent \paragraph_indentation default \quotes_language english \papercolumns 1 \papersides 1 \paperpagestyle default \tracking_changes false \output_changes false \html_math_output 0 \html_css_as_file 0 \html_be_strict false \end_header \begin_body \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash begin{titlepage} \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \end_layout \begin_layout Plain Layout \backslash newcommand{ \backslash HRule}{ \backslash rule{ \backslash linewidth}{0.5mm}} \end_layout \begin_layout Plain Layout \backslash center \end_layout \begin_layout Plain Layout \backslash textsc{ \backslash LARGE Politecnico di Milano} \backslash \backslash [1.5cm] \backslash textsc{ \backslash Large PowerEnjoy} \backslash \backslash [0.5cm] \end_layout \begin_layout Plain Layout \backslash textsc{ \backslash Large Software Engineering 2} \backslash \backslash [0.5cm] \end_layout \begin_layout Plain Layout \end_layout \begin_layout Plain Layout \backslash HRule \backslash \backslash [0.4cm] { \backslash huge \backslash bfseries Requirements Analysis and \backslash \backslash Specification Document} \backslash \backslash [0.4cm] \backslash HRule \backslash \backslash [1.5cm] \end_layout \begin_layout Plain Layout \backslash begin{minipage}{0.4 \backslash textwidth} \backslash begin{flushleft} \backslash large \backslash emph{Authors:} \backslash \backslash Giancarlo \backslash textsc{Colaci} \backslash newline Giulio \backslash textsc{De Pasquale} \backslash newline Francesco \backslash textsc{Rinaldi} \backslash end{flushleft} \backslash end{minipage} ~ \backslash begin{minipage}{0.4 \backslash textwidth} \backslash begin{flushright} \backslash large \backslash emph{Supervisor:} \backslash \backslash Elisabetta \backslash textsc{De Nitto} \backslash end{flushright} \backslash end{minipage} \backslash \backslash [3cm] \end_layout \begin_layout Plain Layout \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Graphics filename res/img/logopm.pdf width 30text% \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash vfill \end_layout \begin_layout Plain Layout { \backslash large \backslash today} \backslash \backslash [3cm] \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash end{titlepage} \end_layout \end_inset \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash mbox{} \backslash thispagestyle{empty} \backslash newpage \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset CommandInset toc LatexCommand tableofcontents \end_inset \begin_inset ERT status open \begin_layout Plain Layout \backslash thispagestyle{empty} \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash setcounter{page}{1} \end_layout \end_inset \end_layout \begin_layout Section Introduction \end_layout \begin_layout Subsection Revision History \end_layout \begin_layout Standard \align center \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Version \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Date \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Author(s) \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Summary \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 1.3 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 22/01/2017 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Giancarlo Colaci \begin_inset Newline newline \end_inset Giulio De Pasquale \begin_inset Newline newline \end_inset Francesco Rinaldi \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Updated Alloy \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 1.2 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 14/01/2017 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Giancarlo Colaci \begin_inset Newline newline \end_inset Giulio De Pasquale \begin_inset Newline newline \end_inset Francesco Rinaldi \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Name refactoring, updated Class Diagram \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 1.1 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 12/12/2016 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Giancarlo Colaci \begin_inset Newline newline \end_inset Giulio De Pasquale \begin_inset Newline newline \end_inset Francesco Rinaldi \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Further details, new functional requirement \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 1.0 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout 14/11/2016 \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Giancarlo Colaci \begin_inset Newline newline \end_inset Giulio De Pasquale \begin_inset Newline newline \end_inset Francesco Rinaldi \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Initial Release \end_layout \end_inset \end_inset \end_layout \begin_layout Subsection Description of the given problem \end_layout \begin_layout Standard We will project and implement PowerEnjoy, which is a new car-sharing service that exclusively employs electric cars. The system that will be developed has to allow the registration of a new user with all his personal information (like name, age, driving license and credit card information), log in credentials and the possibility to find the locations of available cars within a certain distance from his current location or from a specified address. Moreover, according to some policies (specified later) the user can obtain exclusive discounts and offers. \end_layout \begin_layout Subsection Purpose \end_layout \begin_layout Standard The principal purpose of this document, the Requirement Analysis and Specificatio n Document, is to show the functional and non-functional requirements of the system-to-be. They will be based on different aspects: the needs expressed by the stakeholder s, the constraints which it is subject to, the typical scenarios that will happen after its deployment. The targeted audience in this case will be mainly made of software engineers and developers who have to actually develop the service here described. \end_layout \begin_layout Subsection Scope \end_layout \begin_layout Standard The system will be an optimization of a pre-existing system for renting electric cars already in use in some cities. The new system will let users to check reservability and status of available cars, rent or reserve them through a mobile or a web application in a more simple and effective way. In addition to a better user interface, the new system will guarantee a smarter uniform distribution of cars in the city, in order to offer a better service for the citizens, and will also offer some special discount, in order to incentivize the virtuous behaviors of the users. \end_layout \begin_layout Subsection Goals \end_layout \begin_layout Standard PowerEnJoy's users will be able to: \end_layout \begin_layout Itemize register themselves to the system; \end_layout \begin_layout Itemize log into the system; \end_layout \begin_layout Itemize find the location of available cars in a specified area; \end_layout \begin_layout Itemize book a car with the possibility to cancel the reservation; \end_layout \begin_layout Itemize open his / her reserved car; \end_layout \begin_layout Itemize be notified of active reservation status; \end_layout \begin_layout Itemize end the rental; \end_layout \begin_layout Itemize know the total cost at the end of the lease; \end_layout \begin_layout Subsection Stakeholders \end_layout \begin_layout Standard Our primary stakeholder is the professor who gave us this didactical project. Our stakeholder's main need is to review the complete project at the end of the semester. Our objective is to show him/her we have followed the development process in all its parts and that we are able to carry out a challenging task from the beginning to the end fully comprehending all its internal phases. We want to show that we can identify key requirements and specifications, design and test our web/mobile application while providing all documentation backing up the source code. Finally, our typical users will be people that don’t have a car or that prefer to rent a car instead of a public service transportation to go around the city. \end_layout \begin_layout Subsection Glossary \end_layout \begin_layout Standard Below there are definitions of some terms that will be used in the document, in order to avoid any ambiguity in their use and their understanding. \end_layout \begin_layout Description Guest: a person that has never signed up to the system. He can only sign up and view available cars \end_layout \begin_layout Description User: a person already registered in the system who can log in and has a personal profile and can use all the functionalities described. Unless specified, each user is active: therefore can use the service with no restrictions \end_layout \begin_layout Description Deactivated \begin_inset space ~ \end_inset user: a user with revoked privileges. He/she cannot use the service until the issues with his/her account are solved (e.g., expired license) \end_layout \begin_layout Description Login: the action of accessing the system via a username and related password \end_layout \begin_layout Description Notification: a real-time alert that warns a user when there are updates about what he is dealing with \end_layout \begin_layout Description Reservation: the action performed by the registered user when he chooses to drive an available car. It expires as soon as one of these conditions is met: one hour is elapsed from the user's reservation request or the car is unlocked \end_layout \begin_layout Description Rent: the temporary possession and use of one of the PowerEnjoy's cars in return for payment by a user. It starts once a minute is elapsed from the car doors unlock or the engine is ignited and lasts until the doors are re-locked by the system \end_layout \begin_layout Description Available: a fully functional car ready to be used by a registered user \end_layout \begin_layout Description Unavailable: a car which is currently reserved or used by a registered user or is not entirely working (e.g. exhausted battery, mechanical damage) \end_layout \begin_layout Description Reservable: an available car located in a geographical region where a registered user is enabled to reserve it \end_layout \begin_layout Description Parking \begin_inset space ~ \end_inset area: circumscribed public area where cars can be parked (e.g. no parking lots). The set of safe areas for parking cars is pre-defined by the management system. \end_layout \begin_layout Description Recharging \begin_inset space ~ \end_inset area: it is included in the parking area; cars parked here can also be recharged thanks to several charging stations \end_layout \begin_layout Description Special \begin_inset space ~ \end_inset area: specific recharging areas decided by the system to ensure a uniform distribution of cars in the city \end_layout \begin_layout Description RMSS: Request Management Sub-System, it is an already developed part of our system which stores and manages all the information about the PowerEnjoy's cars, users and about their request (reservation or rent). \end_layout \begin_layout Description MES: Maintenance External Service, it is an external service that takes care of ordinary or extraordinary car maintenance. \end_layout \begin_layout Description ADS: Auto Diagnosis System, an always on embedded peripheral which continuously monitors the status of the car (e.g. battery charge, tires pressure, impact detection) \end_layout \begin_layout Description ECS: Emergency Call System, an always on embedded peripheral which can be used to call the consumer service or an emergency number quickly \end_layout \begin_layout Description Verification \begin_inset space ~ \end_inset code: it is a four digits code chosen by the user during the registration procedure that adds another level of security to our service; the user will need it to unlock the car \end_layout \begin_layout Description Countdown: it is the time given to the user to pick-up the reserved car before the reservation expires (during this period the reservation is active) \end_layout \begin_layout Description EULA: End User License Agreement \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Section Overall Description \end_layout \begin_layout Subsection Proposed System \end_layout \begin_layout Standard The server-side implementation will be structured through a net of micro-service s mainly written in Python and managed through Docker. The server will run the business logic, host PowerEnjoy's website, and users' data. Besides, we propose a web/mobile application which allows to registered users to use PowerEnjoy's services. The web client will use Python/Javascript and HTML5/CSS for web pages generatio n and formatting respectively. We will also use open-source libraries such as Flask to speed up the developmen t. The mobile applications will be deployed on the main platforms currently available (iOS, Android, Windows Phone) and will be written accordingly to each devices' programming language. Client-server communication will be platform agnostic since it will happen through an encrypted RESTful API which returns its data through JSON. \end_layout \begin_layout Subsection Domain Properties \end_layout \begin_layout Standard We suppose these conditions will be respected at any given time: \end_layout \begin_layout Itemize the user will request help only if he/she needs it; \end_layout \begin_layout Itemize the user will never try to exploit the system's features (e.g. sleep in the car); \end_layout \begin_layout Itemize the user will never fake his/her position to cause a denial of service; \end_layout \begin_layout Itemize the user will only provide correct and authentic information while signing up; \end_layout \begin_layout Itemize a booked car will always be driven by the user who reserved it; \end_layout \begin_layout Itemize the user will never be robbed of the access credentials and the verification code; \end_layout \begin_layout Itemize the user agrees to be geolocalized; \end_layout \begin_layout Itemize each available car is fully functional; \end_layout \begin_layout Itemize each car has an embedded key to turn on the engine; \end_layout \begin_layout Itemize each car is equipped with a properly working ADS and an ECS; \end_layout \begin_layout Itemize each car is fitted with a properly working notification touchscreen display; \end_layout \begin_layout Itemize an available car will always be found in the supposed position; \end_layout \begin_layout Standard \begin_inset Newpage pagebreak \end_inset \end_layout \begin_layout Subsection Assumptions \end_layout \begin_layout Standard This section explores some of the vague concepts or loosely explained ones: further hypotheses have been added to expand the description of the requirement s and to account better for the interaction between the external environment and the developed application. \end_layout \begin_layout Standard Due to some unclear points in the specification we made some assumptions, which are: \end_layout \begin_layout Itemize the system allows users to locate any car in PowerEnjoy's area of operation; \end_layout \begin_layout Itemize the system's money saving option has to be enabled or disabled in the user profile; \end_layout \begin_layout Itemize the system permits users to reserve an available car only in his/her city; \end_layout \begin_deeper \begin_layout Itemize with "a certain geographical region" we mean that the user can reach the vehicle in a reasonable amount of time; \end_layout \end_deeper \begin_layout Itemize the system can locate its users through Cellular Data or GPS; \end_layout \begin_layout Itemize the system's proximity check is done through one of these: numerical code on each cars' windshield or GPS data from user's phone; \end_layout \begin_layout Itemize the fees are applied as soon as one of these conditions is met: one minute is elapsed from the car's doors opening, or the engine is revved; \end_layout \begin_layout Itemize each seat is equipped with a sensor which is used to detect the number of passengers into each car; \end_layout \begin_layout Itemize each user can't reserve more than one car at the same time; \end_layout \begin_layout Itemize to be eligible for the 10% discount, almost two passengers have to remain seated at the same time for at least one minute; \end_layout \begin_layout Itemize if a car is parked in a special area, the discount equals to 40%; \end_layout \begin_layout Subsection Actors Identifying \end_layout \begin_layout Standard The system provides the interaction of two different types of actors who can use different functionalities of the application system. The types are set out below along with a brief description of their privileges. \end_layout \begin_layout Subsubsection Guest \end_layout \begin_layout Standard A person that is not registered (yet!) so can check for cars' position, register or ask for help/advice. \end_layout \begin_layout Paragraph Privileges: \end_layout \begin_layout Itemize Register to the system by creating a new account; \end_layout \begin_layout Itemize Check available cars' position and status; \end_layout \begin_layout Itemize Contact the customer service; \end_layout \begin_layout Subsubsection User \end_layout \begin_layout Standard A person that is already registered to the system with his personal information; a guest can become a user after the authentication to the system using the login form. \end_layout \begin_layout Paragraph Privileges: \end_layout \begin_layout Itemize Log into the system; \end_layout \begin_layout Itemize Consult reservations' history; \end_layout \begin_layout Itemize Edit account information: \end_layout \begin_deeper \begin_layout Itemize personal and billing data; \end_layout \begin_layout Itemize enable/disable money saving option; \end_layout \end_deeper \begin_layout Itemize Check available cars' position and status; \end_layout \begin_layout Itemize Reserve a reservable car; \end_layout \begin_layout Itemize Rent the reserved car; \end_layout \begin_layout Itemize Check active reservation status: \end_layout \begin_deeper \begin_layout Itemize Remaining time until the reservation expires; \end_layout \begin_layout Itemize Reserved car's position and status; \end_layout \begin_layout Itemize Elapsed rental time; \end_layout \end_deeper \begin_layout Itemize Request help through the ECS; \end_layout \begin_layout Itemize Terminate the rent; \end_layout \begin_layout Itemize Contact the customer service; \end_layout \begin_layout Subsubsection Deactivated User \end_layout \begin_layout Standard A user with revoked privileges. He/she cannot use the service until the issues with his/her account are solved (e.g expired license). \end_layout \begin_layout Paragraph Privileges: \end_layout \begin_layout Itemize Log into the system; \end_layout \begin_layout Itemize Consult reservations' history; \end_layout \begin_layout Itemize Edit account information: \end_layout \begin_deeper \begin_layout Itemize personal and billing data; \end_layout \begin_layout Itemize enable/disable money saving option; \end_layout \end_deeper \begin_layout Itemize Check available cars' position and status; \end_layout \begin_layout Itemize Contact the customer service; \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Section Specific Requirements \end_layout \begin_layout Standard In this section will be analyzed in detail functional and non-functional requirements that the system developed has to satisfy, when the domain properties previously denoted hold and referring to the declared goals. \end_layout \begin_layout Subsection Functional requirements \end_layout \begin_layout Standard The functional requirements include the functionalities that the system must necessarily have and describe the interactions between the system developed and the external environment independently from the implementation. \end_layout \begin_layout Enumerate Registration of a guest to the system: \end_layout \begin_deeper \begin_layout Enumerate The system has to guarantee the registration to a new user by creating a new account. \end_layout \end_deeper \begin_layout Enumerate Login of a user into the system: \end_layout \begin_deeper \begin_layout Enumerate The system has to allow the login to an already registered user when he types the correct username and the password in the login form. \end_layout \end_deeper \begin_layout Enumerate Find the location of available cars in a specified area: \end_layout \begin_deeper \begin_layout Enumerate The system has to allow both guests and users to specify the address where they want to locate an available car or to use their position; \end_layout \begin_layout Enumerate The system has to guarantee that a car is showed on the map if and only if it is available (that means that every available car is showed and that every showed car is available); \end_layout \begin_layout Enumerate The system has to guarantee that the car's position is regularly showed up to date. \end_layout \end_deeper \begin_layout Enumerate Book a car with the possibility to cancel the reservation: \end_layout \begin_deeper \begin_layout Enumerate The system has to guarantee that only a user (i.e. not a guest) can reserve a car; \end_layout \begin_layout Enumerate The system must be able to check the position of the user; \end_layout \begin_layout Enumerate The system has to guarantee that any user can reserve only one car at a time; \end_layout \begin_layout Enumerate The system has to ensure that the same car cannot be reserved at the same time by different users; \end_layout \begin_layout Enumerate The system has to guarantee that any user can have at most an active reservation ; \end_layout \begin_layout Enumerate The system has to guarantee that every reservable car is available; \end_layout \begin_layout Enumerate The system has to ensure that only a reservable car can be reserved; \end_layout \begin_layout Enumerate The system has to guarantee that when a user reserves a car, the latter is no more available; \end_layout \begin_layout Enumerate The system has to ensure that only an active reservation can expire or be canceled; \end_layout \begin_layout Enumerate The system has to make sure that when a reservation expires or is revoked, the car becomes available again; \end_layout \begin_layout Enumerate When a reservation is activated, the system starts a countdown at the end of which the reservation expires if the user did not pick-up the reserved car; \begin_inset Newpage pagebreak \end_inset \end_layout \end_deeper \begin_layout Enumerate Open his/her reserved car; \end_layout \begin_deeper \begin_layout Enumerate The system must be able to check the proximity of the user to the reserved car; \end_layout \begin_layout Enumerate The system must be able to check if the money saving option is enabled for the current reservation; \end_layout \begin_layout Enumerate The system has to allow the user to insert the verification code; \end_layout \begin_layout Enumerate The system has to unlock the reserved car only if the entered verification code is correct; \end_layout \end_deeper \begin_layout Enumerate Be notified of active reservation status: \end_layout \begin_deeper \begin_layout Enumerate The system must be able to retrieve the starting time of the rental; \end_layout \begin_layout Enumerate The system must be able to calculate and notify the elapsed time of the rental periodically; \end_layout \begin_layout Enumerate The system must be able to communicate with every grid power station to check their power plugs' availability; \end_layout \begin_layout Enumerate The system, to ensure a uniform distribution of parked cars, must be able to notify the user the nearest selected station where to leave the car to get a discount only if he/she inputs a destination and the money saving option is active; \end_layout \end_deeper \begin_layout Enumerate End the rental: \end_layout \begin_deeper \begin_layout Enumerate The system has to allow the user to communicate that he/she wants to terminate the rental using the car's display; \end_layout \begin_layout Enumerate The system has to allow the user to end the rental only if he is in a safe parking area; \end_layout \begin_layout Enumerate The system has to guarantee that when a reservation is ended, the car becomes available again; \end_layout \end_deeper \begin_layout Enumerate Know the total cost at the end of the rental: \end_layout \begin_deeper \begin_layout Enumerate The system has to communicate with the ADS to retrieve the car status and rental information; \end_layout \begin_layout Enumerate The system must be able to apply the discounts, if any, handling the previously retrieved information; \end_layout \begin_layout Enumerate The system must communicate to the user the final cost of the rental; \end_layout \end_deeper \begin_layout Enumerate Modify the profile information: \end_layout \begin_deeper \begin_layout Enumerate The system has to allow the user to modify his/her personal information; \end_layout \begin_layout Enumerate The system has to allow the user to enable or disable the money saving option; \end_layout \end_deeper \begin_layout Subsection Non-functional requirements \end_layout \begin_layout Standard The non-functional requirements are those not related to the functionality, but rather consider the quality of the system to be implemented (Quality of Service, QoS), regardless of the application domain. \begin_inset VSpace smallskip \end_inset \end_layout \begin_layout Standard \end_layout \begin_layout Standard Security: \end_layout \begin_layout Itemize Each user will only be able to access functionality that competes to his category, and it is, therefore, necessary to provide an authentication method: it will be used the symmetric username/password one. Furthermore, each credential will not be stored in cleartext, and client/server communications will be protected by asymmetric encryption. \end_layout \begin_layout Standard Portability: \end_layout \begin_layout Itemize The client must be compatible with all hardware and software platforms to reach as many users as possible. This requirement is satisfied by realizing the client as a web application, in this way the only assumptions that must be met by users are the availability of a web browser and a connection to the Internet. \end_layout \begin_layout Standard Stability and reliability: \end_layout \begin_layout Itemize The system must notify the user the result of each his/her transaction request while maintaining an optimal level of reliability. Therefore it will be able to face with the possible loss of connection between clients and the central server by ensuring atomicity of all operations. \end_layout \begin_layout Standard Performance: \end_layout \begin_layout Itemize As for performance, the timing of getting and insertion the information in the database must be acceptable to do not block the whole system. \end_layout \begin_layout Standard Concurrency management: \end_layout \begin_layout Itemize The system must ensure data consistency while dealing with multiple concurrent accesses to the same resource in the database by multiple users authenticated to the system. \end_layout \begin_layout Standard Graphical User Interfaces (GUIs): \end_layout \begin_layout Itemize The system has to include several graphical user interfaces: intuitive, complete and exceptionally easy to use. An interface to contain areas of input, dialog boxes, buttons, links and drop-down menus will be developed. The interfaces will interact with business logic and then be differentiated according to user roles in the system: each interface will provide access to features that compete for the particular user who is logged in. \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Section Scenarios \end_layout \begin_layout Standard This section will present some possible situations that may occur from the interaction between a user and the system developed. \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Subsection Alice is curious about PowerEnjoy \end_layout \begin_layout Standard Lily tells Alice about a new service called PowerEnjoy: Alice, now curious, tries to register to PowerEnjoy. She visits the homepage, browses the site a little and then proceeds to the registration page. Alice then enters all the data needed by the system to complete the process: name and surname, username, email address, password, ID card number and license number. To complete the sign-up she finally enters the billing information. Once everything is done, the system sends her a confirmation mail with a link used to activate her new account. She has now completed the registration, and she can log into the system and power enjoy the service. \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Subsection Grandpa Peter and his expired license \end_layout \begin_layout Standard Grandpa Peter has been registered to PowerEnjoy for a quite long time. He loves the car sharing model, now more than ever since his old Panda broke a long time ago and he could not pick up his nephews, David and Goliath, from the pool. There is a problem, though: Peter is getting old, and his license has to be renewed to drive again. After a long day at the Driver and Vehicle Licensing Agency, Grandpa Peter successfully got his shiny license back! To reactivate his PowerEnjoy account, Peter has to edit his account data and insert the new license card number: after having logged in, he proceeds to his personal area by clicking “Edit Personal Data", he puts the new data in the system, and finally he saves the changes. Grandpa Peter is on the road, again! \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Subsection Grandpa Peter and his nephews \end_layout \begin_layout Standard It's rainy outside, so Grandpa Peter has to pick up his two nephews from the pool: he picks up his smartphone and checks if there are any available cars near him. He is getting old so he cannot walk for a long time, so he reserves the nearest car which, unfortunately, has less than 50% battery charge remaining. Once in the car's reach, Peter taps on “Open Vehicle” and inputs his verificati on code. His memory is aging just like him so the usual “1969” code, which corresponds to the year he married his beloved Franca, turned into “1967” which is not accepted by the system. The system prompts him again, and this time Peter does not fail: the doors unlock, and Grandpa is on the road once more! Peter's driving skills are still amazing: he picks up the kids and gets home in no time, so he ends the rent. Unfortunately, he is not able to use the 20% discount due to the battery charge left, but he will be cut 10% since he took at least two other people in the car. \end_layout \begin_layout Standard \begin_inset Newpage pagebreak \end_inset \end_layout \begin_layout Subsection Pablo and Tata go to the cinema \end_layout \begin_layout Standard Tata and Pablo make a great couple. It's Friday night, and the theaters are flooded by the latest sci-fi movie everyone love. Pablo loves all those lightsabers and starships while Tata just can't get the point out of them. The film will start in more than one hour: Pablo is ready for the night out, Tata has to fix her makeup. “Five minutes and I am ready!" - she said. Unfortunately, Pablo forgot to charge his phone so he can't use his phone's GPS to save precious battery juice and reserves his PowerEnjoy car by entering his address into the app. Time goes by; one hour has passed, and Pablo is still waiting for Tata who seems to have no intentions leaving the bathroom. The film has just begun, the reservation expired, the car is available to be reserved again, and Pablo has to pay 1€ fee: “One minute and we are rolling!” - she said. Pablo, may the force be with you! \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Subsection Gustavo, the discount hunter \end_layout \begin_layout Standard Gustavo is a saver, methodic and old-fashioned man, and he built an economic empire from scratch. He owns a vintage 1968 Ford Torino which is only used on Saturday afternoons with his closest friend to honor the times long gone: on the other days, he mainly uses PowerEnjoy. Gustavo has turned on the money saving option while signing up, and he loves it. Once in the car, he logs in and proceed to set up his seat and insert his destination: the system now calculates the overall cars distribution in the city, verifies the availability of power plugs in the nearest power grid stations to the arrival and suggests to park in a special area just 300 meters away from his destination. Once there, Gustavo, just before ending the rental, takes care of plugging the car into the power grid: now, the smartphone application shows him the total cost which includes the 40% discount. \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Section Models \end_layout \begin_layout Standard In this section we are going to abstract from the previously seen scenarios in order to have a more high-level description. For this purpose we will use UML (Unified Modeling Language) diagrams. \end_layout \begin_layout Subsection Use cases model \end_layout \begin_layout Standard From previously denoted scenarios and from the whole analysis we did in this document, we individuated the use cases of the system to be developed. In these pictures there are some use Cases diagram which represent actors, their use cases and their interactions. Then some of them are better explained using a less formal and more narrative way. \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/Usecase_guest.png width 60text% \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Guest Use Case \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/usecase_user.png width 100text% \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout User Use Case \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/Usecase_disuser.png width 100text% \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Deactivated User Use Case \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Subsubsection Registration \end_layout \begin_layout Standard \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset Guest \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The guest has a working Internet connection and he has not registered an account yet. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The guest reaches the registration page \end_layout \begin_layout Enumerate The system requires the guest to enter all his/her personal information, driving license data and login credentials along with the verification code \end_layout \begin_layout Enumerate The guest types the requested information and presses the ’Next’ button \end_layout \begin_layout Enumerate The system verifies the uniqueness of the email, the equality of the twice typed passwords and that the driving license is not expired yet \end_layout \begin_layout Enumerate The system notifies the guest that he is going to be redirected to an external service web page where he will be required to enter his billing information \end_layout \begin_layout Enumerate The system receives a confirmation from the external payment service about the correctness of the billing information \end_layout \begin_layout Enumerate The system shows to the guest a recap of the information already provided and requires him to confirm them, to read and accept the EULA and complete the registration \end_layout \begin_layout Enumerate The guest ticks the “I read carefully, and I accept the contract” box and presses the “Confirm and Complete Registration” button \end_layout \begin_layout Enumerate The system sends an email to notify the correct registration to the guest \end_layout \begin_layout Enumerate The system reports the registration and redirects the user to the login page \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has signed up. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The email the guest typed has been already used. The second password does not match with the first one. One of the fields is empty. The SSN is not in compliance with the other guest's personal information. The driving license is already expired. The external payment service didn't confirm the billing information. The guest did not accept the EULA. In these cases the system notifies the error and cannot complete the registrati on. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Log in \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset User or Deactivated User \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor has a working Internet connection and he has already registered his account. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The actor reaches the log in page \end_layout \begin_layout Enumerate The system requires the actor to enter his email and password \end_layout \begin_layout Enumerate The actor types the requested information and press the ’Log in’ button \end_layout \begin_layout Enumerate The system verifies the correctness of the email and password \end_layout \begin_layout Enumerate The system redirects the actor to his personal page \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor is logged in. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The email or the password the actor typed are not correct. One of the fields is empty. In these cases the actor can’t complete the log in. The system notifies the error and cannot complete the login. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Edit personal information \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset User or Deactivated User \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor has a working Internet connection and he is already logged into the system. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The actor reaches his personal area \end_layout \begin_layout Enumerate The actor clicks the \begin_inset Quotes eld \end_inset Edit personal information \begin_inset Quotes erd \end_inset button \end_layout \begin_layout Enumerate The system allows the actor to change his address, mobile phone number, password (and to confirm it), driving license number, the expiration date and the authority who released it \end_layout \begin_layout Enumerate The user enters the new information and presses ’Save’ \end_layout \begin_layout Enumerate The system verifies the correctness and the completeness of the information \end_layout \begin_layout Enumerate The system shows the actor his updated information \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has modified his personal information. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset One of the fields is empty. The second password does not match with the first one. The driving license is already expired. In these cases the system notifies the error and cannot complete the request. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Edit billing information \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset User or Deactivated User \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor has a working Internet connection and he is already logged into the system. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The actor reaches his personal area \end_layout \begin_layout Enumerate The actor clicks the \begin_inset Quotes eld \end_inset Edit billing information \begin_inset Quotes erd \end_inset button \end_layout \begin_layout Enumerate The system notifies the actor that he is going to be redirect to an external service web page where he will be required to enter his new billing information \end_layout \begin_layout Enumerate The system receives a confirmation from the external payment service about the correctness of the new billing information \end_layout \begin_layout Enumerate The system shows the actor his updated information \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has modified his billing information. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The external payment service did not confirm the billing information. In this case the system notifies the error and cannot complete the request. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Check available cars' position and status \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset Guest, User or Deactivated User \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor has a working Internet connection. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The actor opens the map \end_layout \begin_layout Enumerate The system requires the actor to enter an address or to use his position to localize cars \end_layout \begin_layout Enumerate The actor types the address where he wants to find an available car or clicks \begin_inset Quotes eld \end_inset Use my position \begin_inset Quotes erd \end_inset button \end_layout \begin_layout Enumerate The system verifies the correctness of the information and send a request to the RMSS \end_layout \begin_layout Enumerate The system receives an answer from the RMSS with the available cars and shows them to the actor on the map \end_layout \begin_layout Enumerate The actor taps the icon that stands for the available car he chooses \end_layout \begin_layout Enumerate The system shows to the actor the status of the selected available car \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor obtains all the information about the position and the status of any available car in a certain area. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The address field is empty. The inserted address is not found or the location service does not work. There is no available cars in the selected area. In these cases the system notifies the error and cannot complete the request. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Reserve a car \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout User \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has a working Internet connection, he has already checked the position and the status of an available car and he is logged into the system for the whole reservation. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The user clicks on “Reserve car” button \end_layout \begin_layout Enumerate The system send to the RMSS the user position and his reservation request \end_layout \begin_layout Enumerate The system receives an affirmative answer from the RMSS \end_layout \begin_layout Enumerate The system creates a new instance of the reservation \end_layout \begin_layout Enumerate The system notifies the user the success of the reservation \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user reserved successfully a car. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The communication with the RMSS failed. The system says to the user that the service is temporarily not available. The localization service does not work. The system receives a negative answer from the RMSS. In these cases the system notifies the error to the user and he cannot complete the reservation. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Open the reserved car \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout User \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has a working Internet connection, has already reserved a car and he is logged into the system. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The user reaches the car he reserved. \end_layout \begin_layout Enumerate The system checks user position or requires him to enter the code on the windshield \end_layout \begin_layout Enumerate If necessary, the user enters the code he can read on the windshield \end_layout \begin_layout Enumerate The system requires the user enter his verification code \end_layout \begin_layout Enumerate The user types his verification code \end_layout \begin_layout Enumerate The system verifies the correctness of the verification code and the status of the reservation \end_layout \begin_layout Enumerate The system unlocks the car doors, terminates the reservation and creates a rent instance on the RMSS \end_layout \begin_layout Enumerate The user opens the car doors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user can get in the car. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user failed to unlock the car in less than one hour: the system notifies the end of the reservation to the user, declares the reserved car as available again and applies 1€ of fee to the user. | The system is not able to check the user position. The user fails to enter the windshield code. The verification code is not correct. In these cases the system doesn’t unlock the doors. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Use the reserved car and terminate the rent \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout User \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user has a working Internet connection, has already opened his reserved car and he is logged into the system. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate If the money saving option is actived, the user can enter his final address on the touchscreen display in the car \end_layout \begin_layout Enumerate If the user did it, the system shows a special parking area near his destination \end_layout \begin_layout Enumerate The user starts the engine and uses the car \end_layout \begin_layout Enumerate As a matter of choice, the user takes care of plugging the car into the power grid \end_layout \begin_layout Enumerate The user clicks \begin_inset Quotes eld \end_inset Terminate rent \begin_inset Quotes erd \end_inset \end_layout \begin_layout Enumerate The system verifies nobody is in the car and that it is in a safe parking area \end_layout \begin_layout Enumerate The system locks the car doors again, verifies the car's status and updates the rent instance \end_layout \begin_layout Enumerate If necessary, the system contacts the MES for an ordinary (or extraordinary) car maintenance. \end_layout \begin_layout Enumerate The system calculates the total cost and notifies the end of the rental to the user along with the total cost \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The user successfully rented a car. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The address is not correct or it is not found. The system notifies the error to the user and requires him to insert it again. | The car is not in a safe parking area. The car is not empty. In these cases the system doesn’t allow to terminate the rent. | The user can't pay the total cost: the system deactivate the user. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Subsubsection Contact customer service \end_layout \begin_layout Standard \paragraph_spacing onehalf \begin_inset Tabular \begin_inset Text \begin_layout Plain Layout Actors \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Guest, User or Deactivated User \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Preconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor has a working Internet connection. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Events \end_layout \end_inset \begin_inset Text \begin_layout Enumerate The actor reaches the “Contact the Customer Service” page \end_layout \begin_layout Enumerate The system requires the actor to enter his own name, surname, mobile phone number, email address and to explain his problem in less than 1000 words \end_layout \begin_layout Enumerate The user types the requested information and press the ‘Contact the Customer Service” button \end_layout \begin_layout Enumerate The system redirects the request of the user to the customer service. \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Postconditions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor successfully contacted the customer service. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout Exceptions \end_layout \end_inset \begin_inset Text \begin_layout Plain Layout \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset The actor uses more than 1000 words to explain his request. There is at least one empty field. In these cases the system notifies the error and cannot complete the request. \begin_inset ERT status open \begin_layout Plain Layout \backslash vspace{0.15cm} \end_layout \end_inset \end_layout \end_inset \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Subsection Sequence Diagram \end_layout \begin_layout Standard This section presents the sequence diagram of the most important interaction, in order to have a dynamic sight of the main entities too. \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_reg.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Registration Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_login.png width 70text% height 70theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Login Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_checkavailability.png width 100text% height 90theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Check Cars' Availability Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_editinfo.png width 100text% height 70theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Modify Personal Information Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_editbilling.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Modify Billing Information Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_reservation.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Car Reservation Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_opencar.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Car Unlock Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_rent.png width 100text% height 100theight% \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Car Rental Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status collapsed \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/seqdia_contact.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Contact Customer Service Sequence Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Subsection Class Diagram \end_layout \begin_layout Standard Here it is shown a class diagram in order to give a static sight of the main involved entities and of their relations. The diagram, whose aim is just to better specificy requirements, is shown in this picture. \end_layout \begin_layout Standard This diagram is intended as a starting draft to be expanded further in the design phase: moreover, it doesn't represent the final class infrastructure which will be used in our system. Finally, this diagram doesn't include the classes that will be used in the Mobile/Web applications. \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/ClassD.png width 100text% height 100theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Caption Standard \begin_layout Plain Layout Class Diagram \end_layout \end_inset \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Section Alloy \end_layout \begin_layout Standard In this section we tried to verify the consistency of our class diagram. To this goal, we realized a formal model of the system based both on the class diagram and in the previously done assumptions and considerations about constraints. We realized this model using Alloy syntax, thanks to which we get on formally describing the domain of our application and its properties. Then we verified the consistency of our model using Alloy Analyzer. Here there is the code of the model of the system. \end_layout \begin_layout Standard \begin_inset space \quad{} \end_inset \end_layout \begin_layout Standard \begin_inset ERT status open \begin_layout Plain Layout \backslash lstdefinelanguage{alloy} \end_layout \begin_layout Plain Layout {keywords={% \end_layout \begin_layout Plain Layout assert, pred, all, no, lone, one, some, check, run, \end_layout \begin_layout Plain Layout but, let, implies, not, iff, in, and, or, set, sig, Int, int, \end_layout \begin_layout Plain Layout if, then, else, exactly, disj, fact, fun, module, abstract, \end_layout \begin_layout Plain Layout extends, open, none, univ, iden, seq, \end_layout \begin_layout Plain Layout }, \end_layout \begin_layout Plain Layout literate=% \end_layout \begin_layout Plain Layout {:}{$ \backslash colon \backslash $}1 \end_layout \begin_layout Plain Layout %{|}{$ \backslash bullet$}1 \end_layout \begin_layout Plain Layout {==}{$=$}1 \end_layout \begin_layout Plain Layout {=}{$= \backslash $}1 \end_layout \begin_layout Plain Layout {!=}{$ \backslash neq \backslash $}1 \end_layout \begin_layout Plain Layout {&&}{$ \backslash land$}1 \end_layout \begin_layout Plain Layout {||}{$ \backslash lor \backslash $}1 \end_layout \begin_layout Plain Layout {<=}{$ \backslash le \backslash $}1 \end_layout \begin_layout Plain Layout {>=}{$ \backslash ge \backslash $}1 \end_layout \begin_layout Plain Layout %{all}{$ \backslash forall \backslash $}1 \end_layout \begin_layout Plain Layout {exists}{$ \backslash exists \backslash $}1 \end_layout \begin_layout Plain Layout {!in}{$ \backslash not \backslash in \backslash $}1 \end_layout \begin_layout Plain Layout { \backslash \backslash in}{$ \backslash in$}1 \end_layout \begin_layout Plain Layout {=>}{$ \backslash implies \backslash $}2 \end_layout \begin_layout Plain Layout % the following isn't actually Alloy, but it gives the option to produce nicer latex \end_layout \begin_layout Plain Layout {|=>}{$ \backslash Rightarrow$}2 \end_layout \begin_layout Plain Layout {<=set}{$ \backslash subseteq$}1 \end_layout \begin_layout Plain Layout {+set}{$ \backslash cup$}1 \end_layout \begin_layout Plain Layout {*set}{$ \backslash cap$}1 \end_layout \begin_layout Plain Layout {==>}{$ \backslash Longrightarrow$}3 \end_layout \begin_layout Plain Layout {<==>}{$ \backslash Longleftrightarrow$}4 \end_layout \begin_layout Plain Layout {...}{$ \backslash ldots$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash hl}{$ \backslash hline$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash alpha}{$ \backslash alpha$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash beta}{$ \backslash beta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash gamma}{$ \backslash gamma$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash delta}{$ \backslash delta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash epsilon}{$ \backslash epsilon$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash zeta}{$ \backslash zeta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash eta}{$ \backslash eta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash theta}{$ \backslash theta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash iota}{$ \backslash iota$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash kappa}{$ \backslash kappa$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash lambda}{$ \backslash lambda$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash mu}{$ \backslash mu$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash nu}{$ \backslash nu$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash xi}{$ \backslash xi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash pi}{$ \backslash pi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash rho}{$ \backslash rho$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash sigma}{$ \backslash sigma$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash tau}{$ \backslash tau$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash upsilon}{$ \backslash upsilon$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash phi}{$ \backslash phi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash chi}{$ \backslash chi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash psi}{$ \backslash psi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash omega}{$ \backslash omega$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Gamma}{$ \backslash Gamma$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Delta}{$ \backslash Delta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Theta}{$ \backslash Theta$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Lambda}{$ \backslash Lambda$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Xi}{$ \backslash Xi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Pi}{$ \backslash Pi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Sigma}{$ \backslash Sigma$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Upsilon}{$ \backslash Upsilon$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Phi}{$ \backslash Phi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Psi}{$ \backslash Psi$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash Omega}{$ \backslash Omega$}1 \end_layout \begin_layout Plain Layout { \backslash \backslash EOF}{ \backslash ;}1 \end_layout \begin_layout Plain Layout , \end_layout \begin_layout Plain Layout sensitive=true, % case sensitive \end_layout \begin_layout Plain Layout morecomment=[l]//,% \end_layout \begin_layout Plain Layout morecomment=[l]{--},% \end_layout \begin_layout Plain Layout morecomment=[s]{/*}{*/},% \end_layout \begin_layout Plain Layout morestring=[b]", \end_layout \begin_layout Plain Layout numbers=none, \end_layout \begin_layout Plain Layout firstnumber=1, \end_layout \begin_layout Plain Layout numberstyle= \backslash tiny, \end_layout \begin_layout Plain Layout stepnumber=2, \end_layout \begin_layout Plain Layout basicstyle= \backslash scriptsize \backslash ttfamily \backslash large, \end_layout \begin_layout Plain Layout commentstyle= \backslash bfseries \backslash color{blue!20!black!50!green}, \end_layout \begin_layout Plain Layout keywordstyle= \backslash bfseries \backslash color{blue}, \end_layout \begin_layout Plain Layout numberstyle= \backslash bfseries \backslash color{red}, \end_layout \begin_layout Plain Layout ndkeywordstyle= \backslash bfseries \backslash color{red}, \end_layout \begin_layout Plain Layout tabsize=2, \end_layout \begin_layout Plain Layout columns=fullflexible, \end_layout \begin_layout Plain Layout } \end_layout \begin_layout Plain Layout % inline \end_layout \begin_layout Plain Layout \backslash def \backslash A{% \end_layout \begin_layout Plain Layout \backslash lstinline[language=alloy,basicstyle= \backslash ttfamily,columns=fixed]} \end_layout \begin_layout Plain Layout \end_layout \begin_layout Plain Layout % paragraph \end_layout \begin_layout Plain Layout \backslash lstnewenvironment{alloy}[1][]{% \end_layout \begin_layout Plain Layout \backslash lstset{language=alloy, \end_layout \begin_layout Plain Layout floatplacement={tbp},captionpos=b, \end_layout \begin_layout Plain Layout xleftmargin=8pt,xrightmargin=8pt,basicstyle= \backslash ttfamily,#1}}{} \end_layout \begin_layout Plain Layout \end_layout \begin_layout Plain Layout % paragraph from file \end_layout \begin_layout Plain Layout \backslash newcommand{ \backslash alloyfile}[1]{ \end_layout \begin_layout Plain Layout \backslash lstinputlisting[language=alloy,% \end_layout \begin_layout Plain Layout frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle= \backslash ttfamily,columns=fixed]{#1} \end_layout \begin_layout Plain Layout \end_layout \begin_layout Plain Layout } \end_layout \begin_layout Plain Layout \backslash lstinputlisting[language=alloy]{res/alloy/AlloyPowerEnjoy.als} \end_layout \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Subsection Generated Worlds \end_layout \begin_layout Standard Here are presented three generated worlds, according to the model specified in Alloy. \end_layout \begin_layout Standard \align center \begin_inset Graphics filename res/img/world1.png height 100theight% rotateAngle 90 \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \align center \begin_inset Graphics filename res/img/world2.png height 100theight% rotateAngle 90 \end_inset \end_layout \begin_layout Standard \begin_inset Newpage newpage \end_inset \end_layout \begin_layout Standard \align center \begin_inset Graphics filename res/img/world3.png height 100theight% rotateAngle 90 \end_inset \end_layout \begin_layout Section Appendix \end_layout \begin_layout Subsection Tools used \end_layout \begin_layout Standard We used the following tools to produce this document: \end_layout \begin_layout Itemize \series bold LaTex \series default as typesetting system to write this document \end_layout \begin_layout Itemize \series bold LyX \series default as editor \end_layout \begin_layout Itemize \series bold Visio Professional \series default to draw all the diagrams \end_layout \begin_layout Itemize \series bold Alloy Analyzer 4.2 \series default to write and verify alloy models \end_layout \begin_layout Subsection Hours spent \end_layout \begin_layout Standard \begin_inset Float figure wide false sideways false status open \begin_layout Plain Layout \align center \begin_inset Graphics filename res/img/hours.png width 50text% height 50theight% keepAspectRatio \end_inset \end_layout \begin_layout Plain Layout \begin_inset Newpage pagebreak \end_inset \end_layout \end_inset \end_layout \end_body \end_document