\jection{Experiments}
\subsection{Requirements Engineering}

\begin{frame}
\frametitle{Requirements Engineering}
Early life cycle work 
\end{frame}

\begin{frame}
\frametitle{DDP}
\frametitle{Defect Detection and Prevention}
DDP models have
\begin{itemize}
\item weighted objectives
\item risks to objectives
\item mitigations to reduce risks, but cost money
\end{itemize}
to find what ``design'' maximizes the objectives achieved, 
while costing the least.

DDP was developed at JPL and has proven its effectiveness
over the last seven years on dozens of JPL projects.

DDP has a built-in simulated annealer to find a near-optimal design.
\end{frame}

\begin{frame}
\frametitle{The Models}
Studied three DDP models, {\it aero, cob}, and {\it holo}.

Previously only {\it aero} had been studied previously,
using diagonal striping.
\end{frame}

\begin{frame}
\frametitle{Question 1: Extreme sampling tuning}
Extreme sampling has two parameters that must be set
by the user.
\begin{itemize}
\item $M$, batch size
\item $N$, how are instances assigned to the good and bad class
\end{itemize}
And which of the three versions (\borens, \borepns, \wobns) is preferred
\end{frame}

\begin{frame}
\frametitle{Answer 1}
\centering
%\includegraphics[width=3.4in]{../Greenwald06/Figures/ddpStudy/setting_iter_mean_2nd_alone.png} \\
\includegraphics[width=1.85in]{../Greenwald06/Figures/ddpStudy/M_iter_mean_2nd_alone.png}
\includegraphics[width=1.85in]{../Greenwald06/Figures/ddpStudy/N_iter_mean_2nd_alone.png}

\end{frame}

\begin{frame}
\frametitle{Answer 1}
\centering
\includegraphics[width=3.1in]{../Greenwald06/Figures/ddpStudy/selector_iter_mean_2nd_alone.png}
\end{frame}

\begin{frame}
\frametitle{Question 2: \bore vs.\ diagonal}
Now that we have picked the highest performing version
of extreme sampling that we investigated,
is our new discretizer better than our old
one?
\end{frame}

\begin{frame}
\frametitle{Answer 2}
\begin{columns}[T]

\begin{column}{2.1in}
\includegraphics[width=1.95in]{../Greenwald06/Figures/aeroDiagComparsion} 
\includegraphics[width=1.95in]{../Greenwald06/Figures/holoDiagComparsion} 
\end{column}
\begin{column}{1.9in}
\bore outperforms diagonal by 61\% while using only 25\% 
of the number of data points.
\end{column}

\end{columns}

\end{frame}

\begin{frame}
\frametitle{Question 3: \bore vs.\ SA}
Our new discretizer increases the performance of ITL,
but how does ITL (with \borens) compare to other metaheuristic
search techniques?

Let's compare ITL to the built-in simulated annealer in DDP.
\end{frame}

\begin{frame}
\frametitle{Answer 3}
\begin{columns}[T]

\begin{column}{2.0in}
\includegraphics[width=1.95in]{../Greenwald06/Figures/aeroComparsion.png} \\
\includegraphics[width=1.95in]{../Greenwald06/Figures/holoComparsion.png} \\
\end{column}

\begin{column}{2.0in}
\includegraphics[width=1.95in]{../Greenwald06/Figures/cobComparsion.png} \\
SA outperforms ITL by only 1.4\%, while searching six times as many points.
\end{column}

\end{columns}

\end{frame}


\begin{frame}
\frametitle{Conclusions from DDP}
The experiments with DDP and ITL show
\begin{itemize}
\item how $M/N$ effect performance of extreme sampling, \borens-500/75 the
      best investigated \pause

\item \bore better than diagonal 
      \begin{itemize}
      \item faster
      \item higher quality solutions
      \end{itemize}
\pause

\item ITL faster than simulated annealer
      \begin{itemize}
      \item faster
      \item same quality solutions
      \end{itemize}
\end{itemize}

\end{frame}


\subsection{Property Verification}

\begin{frame}
\frametitle{Property Verification}
Late life cycle work
\end{frame}

\begin{frame}
\frametitle{SPY}
Motivation for SPY development was to create an environment
to validate temporal properties in models with real-valued inputs.

The presence of real-valued inputs makes validating these types of
models difficult with complete model checking techniques.
Two common ways to use model checkers with real-valued models
\begin{itemize}
\item bounded checking
\item abstraction
\end{itemize}
\pause
A complement to, not a replacement of, model checkers.

\end{frame}

\begin{frame}
\frametitle{SPY}
The SPY framework checks these types of models by conducting
an ITL search.  
Hence, like all metaheuristic methods, it has
no completeness guarantee,
but has no restrictions on model input types.

%SPY framework works by executing the model and
%finding input range restrictions that restrict
%the model to desired behavior.

Desired behavior is determined by the development
what is called the {\it worth} function.
\end{frame}

\begin{frame}
\frametitle{NASA flight models}
We investigated three NASA flight models
developed by NASA contractors that were
translated from Simulink by a translation framework
developed by our UMN collaborators
\begin{itemize}
\item Dual FGS
\item Altitude Switch
\item Voting Sensor
\end{itemize}
There were a total of ten properties we checked in these models.
\pause

In addition, we baselined SPY against Reactis, a popular
commercial product we the same capabilities and a similar
methodology.
\end{frame}


\begin{frame}
\frametitle{Question 1: temporal properties}
Can SPY find temporal property violations
in models with real-valued inputs.
\end{frame}

\begin{frame}
\frametitle{Answer 1}
SPY found the same property violations as our
baseline tool.  
Some violations were injected
into the property formulations to ensure that 
every model had at least one violated property.
\end{frame}

\begin{frame}
\frametitle{Problems with Flight Models}
The flight models checked by SPY were temporal models,
which raised issues not seen with the non-temporal benefit/cost models.

First attempt to learn on the values of each discrete time step
for every input variable usually defeated the learners ability
to find useful treatments.

When it did find treatments, it was realized their form
was not useful.
\end{frame}

\begin{frame}
\frametitle{Problems with Flight Models}
We ended up parameterizing the input variables as probability
and step functions, and the presented the learner with
the function parameters.
\vspace{.15in}

This led to less than useful range restrictions.
\end{frame}

\begin{frame}
\frametitle{Solution}
Investigate less complex models,
that have more controllable inputs.
\vspace{.15in}

We choose two different biomathematical models which were
temporal, but whose input variables remained fixed
throughout the simulation.
\end{frame}

\begin{frame}
\frametitle{Competitive Exclusion}
A system of two interacting species
\begin{align}
\frac{du_1}{d\tau} &= u_1(1 - u_1 - a_{12}u_2) \notag \\
\frac{du_2}{d\tau} &= \rho u_2(1 - u_2 - a_{21}u_1) \notag
\end{align}
Five independent variables, $\rho \text{, } u_1^0 \text{, }u_2^0\text{, }
a_{12} \text{, and }  a_{21}$.

\end{frame}

\begin{frame}
\frametitle{Competitive Exclusion}
Symbolic analysis shows that system always approaches
an equilibrium state and that if
$0 \leq a_{12} \leq 1 \text{ and }0 \leq a_{21} \leq 1$ \\
both species have a non-zero population at the equilibrium state.
\end{frame}

\begin{frame}
\frametitle{Question 2: Can SPY find the correct ranges}
We want SPY to find ranges on the relevant 
independent variables ($a_{12} \text{ and } a_{21}$)
that lead to the desired model output behavior.

We also want SPY to ignore irrelevant 
independent variables ($\rho \text{, } u_1^0 \text{, and }u_2^0$).

\end{frame}

\begin{frame}
\frametitle{Answer 2}
\small
Relevant variables \\ \vspace{.1in}
\begin{tabular}{c|c|c|c|}
\hline
name & lower bounds & upper bounds & speed \\
$a_{12}$ & 0.0(10) & 0.2(5), 0.6(2), 0.8(2) & 1.8 \\
$a_{21}$ & 0.0(10) & 0.2(3), 0.3, 0.4(4), 0.8(2) & 1.2 \\
\hline
\end{tabular}
\vspace{.25in}

Irrelevant variables \\ \vspace{.1in}
\begin{tabular}{c|c|c|c|}
\hline
name & lower bounds & upper bounds & speed \\
$\rho$ & 0.0(10) & 15.0(10) & 1.0 \\
$u_1^0$ & 0.04(10) & 2.04(10) & 1.0 \\
$u_2^0$ & 0.04(10) & 2.04(10) & 1.0 \\
\hline
\end{tabular}

\end{frame}

\begin{frame}
\frametitle{Animal Neurons}
A computationally model that can simulate the behavior of real neurons
\begin{align}
\frac{dv}{dt} &= 0.04v^2 + 5v + 140 - u + I \notag \\
\frac{du}{dt} &= a(bv - u) \notag \\
&\text{if} ~v \geq 30 mV, \text{then} ~v \leftarrow c~\text{and}~u \leftarrow u + d \notag
\end{align}
Four independent variables, $a \text{, } b \text{, } c \text{, and } d$.

\end{frame}

\begin{frame}
\frametitle{Animal Neurons}
Three example behaviors \\
\vspace{.12in}
\includegraphics[width=1.6in]{../Greenwald06/Figures/phasic-spiking.png}
\includegraphics[width=1.6in]{../Greenwald06/Figures/tonic-bursting.png} \\
\includegraphics[width=1.6in]{../Greenwald06/Figures/phasic-bursting.png}
\end{frame}

\begin{frame}
\frametitle{Question 3: Can SPY find these selected behaviors}
After developing three worth functions,
one each for the three different example behaviors,
can SPY find restrictions to the independent variables
that confine the model output behavior.
\end{frame}

\begin{frame}
\frametitle{Answer 3}
Tonic bursting \\
\includegraphics[width=3.9in]{../Greenwald06/Figures/spy/neuronTB2.png} \\
\vspace{.15in}
8 of 10 trials were successful, most successful objective function.
\end{frame}

\begin{frame}
\frametitle{Conclusions from SPY}
SPY experiments with flight and biomathematical models show
\begin{itemize} \itemsep -1pt
\item SPY execution model is effective
\item translation preserved model semantics
\item SPY found property violations that were
\begin{itemize} \itemsep -2pt
    \item presented in the model
    \item injected in the property formulations
\end{itemize}

\item potentially useful range restrictions found in the biomathematical models
\pause
\item time-dependent independent variables have to be parameterized functions
\item difficult to optimize discrete/non-continuous functions
\end{itemize}
\end{frame}


