Select Git revision
Forked from
Anders Blomdell / LabComm
Source project has a limited visibility.
-
Tommy Olofsson authoredTommy Olofsson authored
03-model.tex 19.40 KiB
This section introduces the receiver model used in the rest of the
paper. Specifically, Section~\ref{sec:gps:phy} describes the physics
behind the model and Section~\ref{sec:gps:mod} discusses our modelling
choices.
\subsection{GPS physics}
\label{sec:gps:phy}
GPS sensors locate themselves through a process called
\emph{trilateration}~\cite{bib:gps-book}. This process consists in
measuring the distance from 4 or more points in space (satellites),
whose position is known. Given the distance measurements, the GPS
sensor then performs a least square estimation to determine its
current position. Figure~\ref{fig:globe} shows an example with five
satellites. To correctly estimate the current position, the GPS
receiver must measure the distance from $s_1, s_2, s_3$ and $s_4$.
Additionally, measuring the distance from $s_5$ is not necessary, but
improves the position accuracy.
The GPS framework includes (circa) 30 satellites. These satellites
orbit around the Earth following known trajectories. While orbiting,
they broadcast periodic signals that encode a set of parameters,
called \emph{ephemeris data}. The emphemeris data describe the
satellites' orbits (see for example the trajectory of satelite $s_3$
in Figure~\ref{fig:globe}), and therefore allow the GPS receiver to
accurately determine their position in time. The satellite
trajectories are not constant in time, due to uncertainties and
disturbances, like corrections for collision avoidance.
\begin{figure}
\centering
\scalebox{0.6}{%
\begin{pspicture}(-5,-4)(6,6)
\psset{RotX=-23, RotZ=30, PHI=46.5833, THETA=0.3333,
visibility=false, Decran=15,
path=/usr/share/texlive/texmf-dist/tex/generic/pst-geo/data}
% map
\WorldMapThreeD[circles=false, blueEarth=false]
\WorldMapThreeD[circles=false, visibility=true, opacity=0.8]
% s1
\pscircle[linecolor=red, fillcolor=red, fillstyle=solid](-3,5){0.1}
\psline[linecolor=red, linewidth=0.1](0.8,0.8)(-3,5)
\rput[tl](-2.75,5.2){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$s_1$}}
% s2
\pscircle[linecolor=red, fillcolor=red, fillstyle=solid](5.5,5.5){0.1}
\psline[linecolor=red, linewidth=0.1](0.78,0.83)(5.5,5.5)
\rput[tl](5.5,5.3){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$s_2$}}
% s3
\pscircle[linecolor=red, fillcolor=red, fillstyle=solid](5,3){0.1}
\psline[linecolor=red, linewidth=0.1](0.75,0.82)(5,3)
\rput[tl](4.8,2.8){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$s_3$}}
% s4
\pscircle[linecolor=red, fillcolor=red, fillstyle=solid](1.25,5){0.1}
\psline[linecolor=red, linewidth=0.1](0.78,0.82)(1.25,5)
\rput[tl](1.45,5.15){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$s_4$}}
% s5
\pscircle[linecolor=red, fillcolor=red, fillstyle=solid](0.5,4.5){0.1}
\psline[linecolor=red, linestyle=dashed, linewidth=0.1](0.8,0.82)(0.5,4.5)
\rput[tl](-0.1,4.5){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$s_5$}}
% curve for satelite s3
\pscurve[linecolor=red, linestyle=dotted]{->}(5,3)(5.75,3.2)(4,1.5)
% delay and distance for s1
\rput[tl](-4.4,4.3){\fontsize{16pt}{16pt}\selectfont\textcolor{red}{$\{\Delta_1, d_1\}$}}
\end{pspicture}}
\caption{Trilateration: GPS receiver and satellites.}
\label{fig:globe}
\end{figure}
The ephemeris data expire after 30 minutes, i.e., after 30 minutes
they are not considered valid anymore. To correctly estimate thecurrent position, the receiver should ensure that the ephemeris data
are frequently updated. The transmission of the ephemeris data has a
duration of 30 seconds, and the satellites continuously broadcast new
data. In order to ensure the correct aquisition of one data point, the
receiver then has to fetch and decode the signal for a time that is in
the interval $[30,60)$ seconds (in the worst case, the receiver is
turned on right after the start of a new message transmission).
All the satellites transmit on the same frequency and then the
different signals are multiplexed using the Code Division Multiple
Access (CDMA) technique. Using CDMA, the signal has three components:
(i) the carrier wave, (ii) the data waveform, and (iii) a spreding
waveform. The spreading waveform is a deterministic signal, different
for each satellite\footnote{Each satellite's spreding waveform is
unique and has been chosen to be a \emph{golden code}, i.e., it
looks like white noise and it does not correlate with any other
satellite sequence.}, transmitted at much higher frequency with
respect the data waveform. The spreading waveform is then used to
recognize the satellite the received message belongs to.
The spreading waveform is also used for determining the distance
between the satellite and the receiver. Assuming the satellite and the
receiver share a time reference, the receiver can measure the delay it
takes to receive the signal from the satellite. In
Figure~\ref{fig:globe} the delay to receive the message from satellite
$s_1$ is denoted by $\Delta_1$. Multiplying this quantitiy by the
speed of light $C$, the receiver can determine how far the signal has
been travelling, i.e., the distance from the satellite, indicated in
Figure~\ref{fig:globe} with $d_1$. For a generic satellite $x$, this
can be written as $d_{x} = \Delta_{x} \cdot C$. The set of the
distances the receiver measures from the visible satellites is called
\emph{ranging data}.
The hypothesis that the clocks of the receiver and the satellites are
synchronized is not valid, so one extra satellite must be tracked and
used for the trilateration procedure. The fourth satellite allows the
receiver to compensate its time reference offset.
Due to the satellites' and the receiver's movements, the doppler
effect will distort the signal reception. The effect is a shift in the
frequency spectrum of the signal. To fetch the signal, the receiver
must then perform a two-dimensional search in phase and frequency
shift. As a consequence, the process of fetching the signal directly
includes the measurement of the ranging data\footnote{Additionally,
the receiver can estimate its own speed from the measured doppler
effect and compensate for the satellite speed retrieved with the
ephemeris data.}. This process takes some milleseconds (usually in
the range from $2ms$ to $10ms$), depending mainly on signal stength.
% --------------------------------------------------------------------
\begin{table*}[t]
\caption{Combinations of Ephemeris Data, Ranging Data and Antenna Status.}
\label{fig:states}
\centering
\begin{tabular}{lcccc}
\hline\hline
\textbf{State Name} & \textbf{Ephemeris Data} & \textbf{Ranging Data} & \textbf{Antenna} & \textbf{State Number} \\ \hline\hline
Position Available & Available & Available & On & \textcircled{\scriptsize 4} \\ \hline
--- & \st{Available} & \st{Available} & \st{Off} & \\ \hline
Warm Start & Available & Not Available & On & \textcircled{\scriptsize 5} \\ \hline
Warm Start Available & Available & Not Available & Off & \textcircled{\scriptsize 6} \\ \hline
Read Ephemeris Data & Not Available & Available & On & \textcircled{\scriptsize 3} \\ \hline
--- & \st{Not Available} & \st{Available} & \st{Off} & \\ \hline
Cold Start & Not Available & Not Available & On & \textcircled{\scriptsize 2} \\ \hline
Not Available Info & Not Available & Not Available & Off & \textcircled{\scriptsize 1} \\ \hline\hline
\end{tabular}
\end{table*}
% --------------------------------------------------------------------
\begin{table*}
\caption{Transitions, summary table with name, conditions and eventual updates.}\label{fig:transitions}
\centering
\begin{tabular}{lcc}
\hline\hline
\textbf{Transition} & \textbf{Triggering Condition} & \textbf{Effects (Updates)} \\ \hline\hline
\texttt{turn\_on} & User Controlled & --- \\ \hline
\texttt{turn\_off} & User Controlled & --- \\ \hline
\texttt{fetch\_freq\&phase} & Time Delay, usually in the interval [2ms, 10ms] & \texttt{sat\_tracked\_freq\&phase := visible\_satellites} \\ \hline
\texttt{get\_ephemeris} & Time Delay, in the interval [30s, 60s) & \texttt{sat\_tracked\_ephemeris := visible\_satellites} \\
& & \texttt{expiry\_time\_ephemeris := time + 30minutes} \\ \hline
\texttt{lose\_visibility} & \texttt{sat\_tracked\_freq\&phase < required\_satellites} & --- \\ \hline
\texttt{ephemeris\_expire} & \texttt{time > expiry\_time\_ephemeris or} & --- \\
& \texttt{sat\_tracked\_ephemeris < required\_satellites} & --- \\ \hline\hline
\end{tabular}
\end{table*}
% --------------------------------------------------------------------
\begin{figure*}[t]
\centering
\begin{tikzpicture}[%
p_off/.style = {circle, draw=black, inner sep=3mm},
p_on/.style = {circle, draw=black, fill=black!40!green, inner sep=3mm},
arr/.style = {->, solid, black!60},
>=triangle 60,
font=\footnotesize]
\node[thick] (ni) at ( 0, 0) [p_off, label={No Info}] {1};
\node[thick] (cs) at ( 4, 0) [p_on, label={Cold Start}] {2};
\node[thick] (re) at ( 8, 0) [p_on, label={Read Ephemeris}] {3};
\node[thick] (pa) at (12, 0) [p_on, label={Position Available}] {4};
\node[thick] (ws) at (10, -3) [p_on, label={Warm Start}] {5};
\node[thick] (wsa) at ( 6, -3) [p_off, label={Warm Start Available}] {6};
\node[thick] (zero) at (-1.5, 1) [circle, draw=black!60, fill=black!60, inner sep=0.75mm] {};
\begin{pgfonlayer}{background}
% yellow: ephemeris data available
\draw[draw={rgb:red,205;green,205;blue,15;black,5}, dashed, fill=yellow!10, rounded corners]
(4.25,-4.15) -- (13.5,-4.15) -- (13.5,1.35) -- (10.5,1.35) -- (10.5,-1.95) -- (4.25,-1.95) -- (4.25,-4.15);
\draw[draw=yellow!10,-] (10.5,-1.95) -- (13.5,-1.95);
\node (eda) at (6.35, -3.9) {\textcolor{rgb:red,205;green,205;blue,15;black,5}{\textbf{Ephemeris Data Available}}};
% pink: ranging data available
\draw[draw=none, fill=red, opacity=0.1, rounded corners] (6.65,-1.15) rectangle (13.35,1.15); % fill
\draw[draw={rgb:red,155;green,10;blue,10;black,5}, dashed, rounded corners] (6.65,-1.15) rectangle (13.35,1.15); % border
\node (eda) at (8.55, -0.9) {\textcolor{rgb:red,155;green,10;blue,10;black,5}{\textbf{Ranging Data Available}}};
\end{pgfonlayer}
% arrows from beginning node
\draw [arr, bend right] (zero) to (ni);
% arrows from 1
\draw [arr] (ni) to node [above] {\texttt{turn\_on}} (cs);
% arrows from 2
\draw [arr] (cs) to node [above] {\texttt{fetch\_freq\&phase}} (re);
\draw [arr, in=60, out=120] (cs) to node [above, xshift=1mm] {\texttt{turn\_off}} (ni);
%\draw [arr, in=210, out=240] (cs) edge[loop] node [below, xshift=-6mm] {\texttt{lose\_visibility}} (cs);
% arrows from 3
\draw [arr] (re) to node [above] {\texttt{get\_ephemeris}} (pa);
\draw [arr, in=60, out=120] (re) to node [above] {\texttt{turn\_off}} (ni);
\draw [arr, in=60, out=120] (re) to node [above] {\texttt{lose\_visibility}} (cs);
% arrows from 4 - position available
\draw [arr, in=60, out=120] (pa) to node [above]
{\texttt{ephemeris\_expire}} (re);
\draw [arr, in=45, out=210] (pa) to node
[left, at start, yshift=-3mm, xshift=-6mm] {\texttt{turn\_off}} (wsa);
\draw [arr] (pa) edge[loop right] node {\texttt{get\_ephemeris}} (pa);
\draw [arr, in=45, out=-90] (pa) to node [right, above, xshift=-11mm]
{\texttt{lose\_visibility}} (ws);
% arrows from 5 - warm start
\draw [arr, in=-45, out=0] (ws) to node [right, near start, xshift=1mm] {\texttt{fetch\_freq\&phase}} (pa);
\draw [arr, in=285, out=135] (ws) to node [near end, above, xshift=13mm, yshift=-2mm] {\texttt{ephemeris\_expire}} (cs);
\draw [arr, in=-10, out=190] (ws) to node [above] {\texttt{turn\_off}} (wsa);
%\draw [arr, in=-60, out=-30] (ws) edge[loop] node [below] {\texttt{lose\_visibility}} (ws);
% arrows from 6 - warm start available
\draw [arr, in=170, out=10] (wsa) to node [above] {\texttt{turn\_on}} (ws);
\draw [arr, in=-90, out=180] (wsa) to node [left, xshift=-1mm] {\texttt{ephemeris\_expire}} (ni);
\end{tikzpicture}
\caption{State machine representing the \emph{cyber} dynamics.}
\label{fig:cyberDynamics}
\end{figure*}
% --------------------------------------------------------------------
\subsection{GPS modeling}
\label{sec:gps:mod}
We plan to use a model of the GPS receiver behavior to optimize
battery consumption subject to position data availability. Our
receiver model needs to capture two relevant \emph{phenomena}: GPS
position availability and power consumption.
The GPS receiver provides a position estimate when it has collected
both the ephemeris and the ranging data for at least 4 satellites.
Detecing data from more than 4 satellites improves the positioning
accuracy. As for power consumption, the receiver always consumes a
(negligible) idle power. On top of that, the sensor consumes
additional power when its radio is turned on, which is precisely the
cause of battery draining. This power has been experimentally shown to
be constant in time~\cite{bib:enloc-smartphones, bib:microsoft-leap}
and usually around 400mW. Our model needs to capture whether:
\begin{enumerate}
\item \emph{ephemeris data} are available or not;
\item \emph{ranging data} are available or not;
\item the radio \emph{antenna} is turned on or off.
\end{enumerate}
The discrete nature of these phenomena can be well captured using a
finite state machine. For our purposes, a \emph{timed automaton} is
sufficient. In the following, we describe the states and transitions
of the resulting timed automaton. We use the variable
\texttt{visible\_satellites} to represent the number of (different)
satellites' signals that reach the receiver.
\textbf{States:} The model \emph{states} are the combination of the
three above configurations. Table~\ref{fig:states} reports all of
them. However, the availability of the ranging data is incompatible
with the radio being turned off, so we remove the two corresponding
states from the list. The discrete states are also augmented with
variables representing the number of satellites being tracked. These
are: (i) the number of satellites for which the ephemeris data are
available (\texttt{sat\_tracked\_ephemeris}), (ii) the number of
satellites for which the ranging data are available
(\texttt{sat\_tracked\_freq\&phase}), and (iii) the expiration time of
the ephemeris data (\texttt{expiry\_time\_ephemeris}).
\textbf{Transitions:} Analogously, the model \emph{transitions}
represent the events that alter the information availability or the
antenna state changes. As described in Section~\ref{sec:gps:phy}, the
ephemeris data become available when the receiver listens
consecutively to the satellites' signal for long enough (transition
\texttt{get\_ephemeris}). The loss of availability happens either at
the expiration of the ephemeris data, or when the tracked satellites
disappear from the visible sky. In theory, the second event does not
necessarly force an update of the ephemeris data. For instance, a
satellite may disapper for a limited time interval and appear again
before its ephemeris data's expiration. For simplicity (and without
loss of information with respect to our model usage) we do not include
the specific tracking of different satellites in the model and,consequently, we do not distinguish between these two cases. The
transition \texttt{ephemeris\_expire} implements both. The ranging
data become available as soon as the satellites' signals are
fetched. We refer to this transition as
\texttt{fetch\_freq\&phase}. The loss of ranging data can have two
causes: (i) the antenna is turned off (transition \texttt{turn\_off}),
(ii) the number of visible satellites is less than the required
one\footnote{Generally 4. Different applications may require a higher
number of satellites to improve positioning accuracy
(\url{https://www.developerfusion.com/article/4652/writing-your-own-gps-applications-part-2/2/}).}
(transition \texttt{lose\_visibility}). Lastly the antenna's state is
controlled by the user with the events \texttt{turn\_on} and
\texttt{turn\_off}.
The transitions can be divided in three categories: \emph{inputs},
\emph{delays}, and \emph{disturbances}. The two transitions
\texttt{turn\_on} and \texttt{turn\_off} are arbitrarily controlled by
the user, and can be seen as inputs of the system. The second
category, delays, includes transitions that represent the end of data
aquisition procedures and can be seen as delays in the system's
dynamics: \texttt{fetch\_freq\&phase} and
\texttt{get\_ephemeris}. When fired, these transitions cause the
update of the state variables \texttt{sat\_tracked\_ephemeris} and
\texttt{sat\_tracked\_freq\&phase}, that are set to the number of
\texttt{visible\_satellites}. In addition, when the
\texttt{get\_ephemeris} transition is fired, the expiration time of
the ephemeris data is also updated, according to
\texttt{expiry\_time\_ephemeris = time + 30minutes}. The
\emph{disturbance} class of transitions includes
\texttt{ephemeris\_expire} and \texttt{lose\_visibility}. Both the
transitions are triggered when the number of visible satellites is
less than the required number. Moreover, the
\texttt{ephemeris\_expire} transition is triggered also when the
current time exceeds \texttt{expiry\_time\_ephemeris}.
The different transitions, their triggering conditions, and their
effects (updates) are summarized in Table~\ref{fig:transitions}.
\textbf{Dynamics:} After defining states and transitions, we need to
specify which transitions can fire in each state and the resulting
system state. The resulting \emph{automaton} is shown in
Figure~\ref{fig:cyberDynamics}. In each of the states, the three
properties shown in Table~\ref{fig:states} can change, e.g., the
ephemeris data can become unavailable if they were available. The
states drawn in green are states in which the antenna is on. The pink
rectangle encloses the states in which the ranging data are available.
The yellow polygon shows the states in which the ephemeris data are
available.
In general, each state accepts only the transitions that alterate the
properties that define it. For instance, if the antenna is off (states
No Info \textcircled{\scriptsize 1} and Warm Start Available
\textcircled{\scriptsize 6}), the automaton can accept the transition
\texttt{turn\_on} and move to a different state, but cannot accept the
transition \texttt{turn\_off}. There is one exception, corresponding
to the self-loop in Figure~\ref{fig:cyberDynamics}. In state Position
Available \textcircled{\scriptsize 4} the transition
\texttt{get\_ephemeris} can be fired to indicate an update of the
ephemeris data before their expiration.
Finally, two (discrete) equations complement the model dynamics. They
saturate the number of tracked satellites (both in terms of ephemeris
and ranging data) to the number of visible satellites, implementing
the fact that the receiver can only track visible satellites. These
are, repsectively, \texttt{sat\_tracked\_ephemeris :=
min\{sat\_tracked\_ephemeris, visible\_satellites\}} and
\texttt{sat\_tracked\_freq\&phase := min\{sat\_tracked\_freq\&phase,
visible\_satellites\}}.