\begin{frame}[allowframebreaks]{gethomesafe}

    Get Home Safe is a mobile application that tries to help people be safer out on the streets.

\begin{enumerate}

    \item \textbf{Use Spin to Model Communication Protocol} \\
        The communication protocol between our server and client is of a highly temporal nature. Spin can be used to simulate the protocol to verify that it is always correct.

    
    \item \textbf{Use Alloy to Verify Our Heat-Map Algorithm} \\
        The crime heat-map if affected by various variables such as crime type, density, and time, and it also varies depending on how zoomed in our out you are viewing the map. Thus, alloy can be used to evaluate the correctness of our proposed heat-map algorithm for crimes.

    \item \textbf{User Study for User Interfaces} \\
        Due to the nature of our application, it is very important that the user interface is easy to use and not error-prone. Therefore, a user study could be conducted in which we design a set of different user interfaces for each scenario that we wish to study and measure user feedback such as completion time and acccuracy to determine what the best user interface for each scenario is.

\end{enumerate}

\end{frame}
