diff --git a/1.RASD/RASD.lyx b/1.RASD/RASD.lyx index cbabab1..10585e5 100644 --- a/1.RASD/RASD.lyx +++ b/1.RASD/RASD.lyx @@ -1,5382 +1,5382 @@ -#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 -Correction to the RASD -\end_layout - -\begin_layout Subsection -Rasd Version 1.1 -\end_layout - -\begin_layout Standard -While writing the Design Document, we found necessary to make some modifications - to the RASD. - This is why we wrote the second version of the document. - Here there are the updates we did: -\end_layout - -\begin_layout Itemize -In the previous RASD we didn't specify that the Customer Service is an outsource -d service, and so in this document and in the following documents we won't - implement it; -\end_layout - -\begin_layout Itemize -We introduced a new functional requirement: modify the profile information. - -\end_layout - -\begin_layout Section -Introduction -\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 -\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 -\begin_inset External - template PDFPages - filename res/img/alloy_mondo_1.pdf - rotateAngle 90 - -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset Newpage newpage -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset External - template PDFPages - filename res/img/alloy_mondo_3.pdf - rotateAngle 90 - -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset Newpage newpage -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset External - template PDFPages - filename res/img/alloy_mondo_2.pdf - 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 +#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 +Correction to the RASD +\end_layout + +\begin_layout Subsection +Rasd Version 1.1 +\end_layout + +\begin_layout Standard +While writing the Design Document, we found necessary to make some modifications + to the RASD. + This is why we wrote the second version of the document. + Here there are the updates we did: +\end_layout + +\begin_layout Itemize +In the previous RASD we didn't specify that the Customer Service is an outsource +d service, and so in this document and in the following documents we won't + implement it; +\end_layout + +\begin_layout Itemize +We introduced a new functional requirement: modify the profile information. + +\end_layout + +\begin_layout Section +Introduction +\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 +\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 +\begin_inset External + template PDFPages + filename res/img/alloy_mondo_1.pdf + rotateAngle 90 + +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset Newpage newpage +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset External + template PDFPages + filename res/img/alloy_mondo_3.pdf + rotateAngle 90 + +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset Newpage newpage +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset External + template PDFPages + filename res/img/alloy_mondo_2.pdf + 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 diff --git a/3.Integration Test Plan Document/ITPD.lyx b/3.Integration Test Plan Document/ITPD.lyx index c7fd98f..8028ce3 100644 --- a/3.Integration Test Plan Document/ITPD.lyx +++ b/3.Integration Test Plan Document/ITPD.lyx @@ -1391,7 +1391,7 @@ Car Manager \end_layout \begin_layout Subsubsection* -Reservation Management +RMSS \end_layout \begin_layout Standard @@ -5011,7 +5011,7 @@ Returns a list of cars around the Location. \end_layout \begin_layout Subsection -Reservation Management +RMSS \end_layout \begin_layout Standard