\chapter{Model Property Checking}\label{chap:properties}
In the last chapter we saw how ITL with a new discretizer 
was able to perform at the same level as a 
well respected metaheuristic technique.
An important feature of that work was the continuous nature
of the objective function used by ITL (the normalized
benefit/cost ratio).
In this chapter and the next we will present results
from experiments using the SPY framework
(described in \tion{SPY}), which will demonstrate
how important this feature is.

The first case study with SPY uses NASA flight models.
We attempt to verify temporal model properties
in production flight models used by NASA contractors.
Property validation was the original motivation 
for developing the SPY framework.
Although there have been several breakthroughs in 
static verification and validation (V \& V) 
techniques such as model checking, 
the usefulness in verifying properties of software systems has been 
limited because important classes of 
software systems involve large input domains 
(\eg unbounded integer variables and real valued variables) 
as well as interrelated numeric 
constraints over the variables in the input domain.
These characteristics severely limit the 
usefulness of verification techniques like model checking.
There are several modifications to model checking
that can be used to allow model checkers to
work with models that have unbounded numeric inputs.
Bounded model checking \cite{biere99,clarke01}
can be used to check a model with discrete
inputs, by exhaustively checking the model
using a narrow range of values for the model inputs.
Models can also be abstracted to remove or isolate
the effect of numeric inputs.
The drawback of this technique is that the model checker
correctness and completeness depend on the abstraction technique.
It may not be possible to develop an abstraction
that preserves the essential semantics of the model being checked.
The SPY framework was designed to give analysts a
tool that didn't suffer that limitation.
The price an analyst has to pay to get around these
limitations is the incomplete nature of SPY's search.
Many model checkers have a completeness guarantee,
so if the checker reports no violations, the model
is guaranteed to never violate the properties checked.
With SPY if a property violation is not found, 
the random nature of its search means that a violation
may still occur, if different inputs are feed to the model.

Throughout \tion{nasa} we will mention a commercial
tool, Reactis, that was used by our collaborators
at the University of Minnesota (UMN)
as a baseline in a comparison with SPY.
Reactis was used because because it is a common commercial
tool that was available in-house to our collaborators
at UMN.
The advantage of Reactis is that it performs
a random and heuristic search through a model,
without any restriction on the type of the model inputs.
This means that this technique can be used to check 
models with real valued inputs without
any preprocessing of the model, just like SPY.
The random nature of Reactis's search means that it
does not have a completeness guarantee, as discussed in
the previous paragraph.

\section{SPY}\label{sect:SPY}
\input{OtherCases/SPY}


\section{Using SPY on NASA Flight Models}\label{sect:nasa}
\input{NASA/production}
 
\section{Conclusions from NASA Flight Models}\label{sect:nasaConclusions}
This chapter has shown, through comparative analysis,
that our current methodology for verifying temporal
properties in real valued models has much potential.
We showed that 
\begin{itemize} \itemsep -14pt
\item the translation framework preserves the semantics of our models
\item SPY agrees with Reactis on which properties are violated in our models %a commerical tool used by V \& V community,
\item SPY was able to find defects in the models that were either
  \begin{itemize} \itemsep +2pt \setstretch{.75}
  \item already present in the models
  \item injected into the formulation of the properties.
  \end{itemize}
\end{itemize}

A difficulty we encountered in this chapter that
was not seen in \chap{casestudies} was the interface between
the learner and the model input variables.
In \chap{casestudies} ITL could learn directly on the 
input variables because the requirement models
were non-temporal.
With the temporal models studied in this chapter,
SPY could not learn directly on the model input variables,
because they changed during the execution of the model.
In two of our flight models, ASW and Dual FGS,
the model inputs represented the states of control
inputs that were expected to change during the course of a simulation.
In our third flight model, Sensor Voting, we had some real value
inputs that changed during the simulation, namely the values reported
by the individual sensors, as well as discrete control
inputs, namely the validity flags reported by each sensor.
In fact, the properties explicitly detailed how the model
was supposed to react when the control states changed.
Presenting SPY with the exact value that each input
took during each discrete time step was not desirable
for two reasons.
First, presenting the learner with that many input variables,
the number of model inputs times the number of discrete time steps,
would overwhelm the learner's ability to find correlations
between the inputs and the objective function evaluation.
Second, if the learner were presented with the value
of each input at each time step, the learner would
return treatments suggesting value assignments to
particular inputs {\it at particular time steps}.
For our purposes these would not be useful suggestions.
For these reasons we parameterized the model's control inputs
as probabilities.
These probabilities were constant during a simulation
and were the values that the SPY framework learned on.
This meant when a defect was discovered by SPY, its
advice would be to decrease or increase the probability of
some of the control inputs being in one state or the other.
In the models studied in this chapter,
the learner would reduce some of these probabilities to zero, 
effectively saying not to use that control input.
This advice might not be particularly useful to the model developers.

Since we would like to investigate SPY's ability to find
useful range restrictions, we decided to investigate
another class of temporal models whose inputs 
were all real valued, but whose values did not
change during the execution of the model.
The next chapter investigates SPY's ability
to find useful range restrictions with
biomathematical models.
These models have the above-mentioned advantage
of having all real valued inputs that do not change
during the execution of the model.
In addition, the models we chose have had previous
analysis work, so we can compare the results
of using SPY with previous results.



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../thesis"
%%% End: 
