diff --git a/paper/sections/03-model.tex b/paper/sections/03-model.tex index 50e4ce4983c6b3dbd29e93984c9c1ee92ddbf339..5b18e01a25d9723e1a378078bb53ca8b846dd8a5 100644 --- a/paper/sections/03-model.tex +++ b/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