\documentclass[../dissertation.tex]{subfiles}

\begin{document}

%%%%% HYPOTHESIS %%%%%
\section{Hypothesis}
\begin{itemize}
    \item Checklists can be tested in a simulated environment 
      to find flaws in checklist for things like
      \begin{itemize}
        \item Can be done in an amount of time that will not endanger aircraft
        \item Provides reproducible results
        \item Procedures will not endanger aircraft or crew further (Crew referring to Checklist Manifesto with the cargo door blowout)
      \end{itemize}
    \item Results in being able to see where to improve checklists
\end{itemize}


%%%%% SAFETY %%%%%
\section{Safety in Aviation}
\subsection{History}
% TODO write about:
% - Safety became more of a concern when more passengers and more planes in the sky
% - Safety procedures being added
% - Rates of accidents
\begin{itemize}
  \item 70-80\% of aviation accidents are attributed to human factors~\cite{faa-reasons}
\end{itemize}

\subsection{Checklists}
\begin{itemize}
  \item Checklists have been shown to aid in minimising human errors~\cite{manifesto}
  \item However, checklists can be misleading and compromise the safety of the aircraft
    due to them being either too confusing or taking too long to complete~\cite{nasa-design}
  \item That is why testing checklists are important to avoid these situations
\end{itemize}


%%%%% FORMAL METHODS %%%%%
\section{Formal Methods}
% TODO add quick overview of what Formal Methods are
% Potential resource: https://shemesh.larc.nasa.gov/fm/fm-what.html

\subsection{History}


\subsection{Application}


%%%%% SOLUTION STACK %%%%%
\section{Solution Stack}
\begin{itemize}
  \item There would be around 3 main components to this tester
    \begin{itemize}
      \item Formal Model
      \item Flight Simulator plugin
      \item Checklist Tester (to connect the formal model and flight simulator)
    \end{itemize}
  \item As VDM-SL is being used, it uses VDMJ to parse the model~\cite{vdmj}. This was a starting
    point for the tech stack, as VDMJ is also open source.
  \item VDMJ is written in Java~\cite{vdmj}, therefore to simplify implementing VDMJ into the
    Checklist Tester, it would be logical to use a Java virtual machine (JVM) language.
\end{itemize}

\subsection{Formal Model}
\begin{itemize}
  \item There were a few ways of implementing the formal model into another application
  \item Some of these methods were provided by Overture~\cite{overture-remote}
    \begin{itemize}
      \item RemoteControl interface
      \item VDMTools API~\cite{vdmtoolbox-api}
    \end{itemize}
  \item However, both of these methods did not suit what was required as most of the
    documentation for RemoteControl was designed for the Overture Tool IDE. VDMTools
    may have handled the formal model differently
  \item The choice was to create a VDMJ wrapper, as the modules are available on Maven
\end{itemize}

\subsection{Checklist Tester}
\subsubsection{JVM Language}
\begin{itemize}
  \item There are multiple languages that are made for or support JVMs~\cite{jvm-alt-lang}
  \item Requirements for language
    \begin{itemize}
      \item Be able to interact with Java code because of VDMJ
      \item Have Graphical User Interface (GUI) libraries
      \item Have good support (the more popular, the more resources available)
    \end{itemize}
  \item The main contenders were Java and Kotlin~\cite{kotlin}
  \item Kotlin~\cite{kotlin} was the choice in the end as Google has been putting Kotlin first
    instead of Java. Kotlin also requires less boilerplate code (e.g. getters and setters)~\cite{android-kotlin}

\end{itemize}

\subsubsection{Graphical User Interface}
\begin{itemize}
  \item As the tester is going to include a UI, the language choice was still important
    \item There are a variety of GUI libraries to consider using
    \begin{itemize}
      \item JavaFX~\cite{javafx}
      \item Swing~\cite{flatlaf}
      \item Compose Multiplatform~\cite{compose}
    \end{itemize}
  \item The decision was to use Compose Multiplatform in the end, due to time limitations and
    having prior experience in using Flutter~\cite{flutter}
  \item Compose Multiplatform has the ability to create a desktop application and a server,
    which would allow for leeway if a server would be needed
\end{itemize}

\subsection{Flight Simulator Plugin}
\begin{itemize}
  \item There are two main choices for flight simulators that can be used
    for professional simulation
    \begin{itemize}
      \item X-Plane~\cite{x-plane}
      \item Prepar3D~\cite{p3d}
    \end{itemize}
  \item X-Plane was the choice due to having better documentation for the SDK, and a variety
    of development libraries for the simulator itself
  \item For the plugin itself, there was already a solution developed by NASA, X-Plane Connect~\cite{xpc}
    that is more appropriate due to the time limitations and would be more likely to be reliable
    as it has been developed since 2015
\end{itemize}


\end{document}
