Merge branch 'master' of gitlab.control.lth.se:mmaggio/gps-modeling

paper/sections/03-model.tex

@@ -117,33 +117,6 @@ includes the measurement of the ranging data\footnote{Additionally,
   ephemeris data.}. This process takes some milleseconds (usually in
 the range from $2ms$ to $10ms$), depending mainly on signal stength.
 
-\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. 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.
-
 % --------------------------------------------------------------------
 \begin{table*}[t]
 \caption{Combinations of Ephemeris Data, Ranging Data and Antenna Status.}
@@ -181,68 +154,6 @@ Not Available Info   & Not Available           & Not Available         & Off
 \end{tabular}
 \end{table*}
 % --------------------------------------------------------------------
-
-\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.} (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}.
-
 \begin{figure*}[t]
 \centering
 \begin{tikzpicture}[%
@@ -311,6 +222,95 @@ font=\footnotesize]
 \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. 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.} (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