5383 lines
95 KiB
Plaintext
5383 lines
95 KiB
Plaintext
|
#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
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="middle" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Log in
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Edit personal information
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Edit billing information
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Check available cars' position and status
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Reserve a car
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
User
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Open the reserved car
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
User
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\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
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="top" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
User
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
|
|||
|
|
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Subsubsection
|
|||
|
|
Contact customer service
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\begin_layout Standard
|
|||
|
|
\paragraph_spacing onehalf
|
|||
|
|
\begin_inset Tabular
|
|||
|
|
<lyxtabular version="3" rows="5" columns="2">
|
|||
|
|
<features tabularvalignment="middle">
|
|||
|
|
<column alignment="center" valignment="middle" width="20text%">
|
|||
|
|
<column alignment="block" valignment="middle" width="75text%">
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Actors
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" topline="true" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Guest, User or Deactivated User
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Preconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Events
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Postconditions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
<row>
|
|||
|
|
<cell alignment="center" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\begin_inset Text
|
|||
|
|
|
|||
|
|
\begin_layout Plain Layout
|
|||
|
|
Exceptions
|
|||
|
|
\end_layout
|
|||
|
|
|
|||
|
|
\end_inset
|
|||
|
|
</cell>
|
|||
|
|
<cell alignment="block" valignment="top" bottomline="true" usebox="none">
|
|||
|
|
\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
|
|||
|
|
</cell>
|
|||
|
|
</row>
|
|||
|
|
</lyxtabular>
|
|||
|
|
|
|||
|
|
\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
|