The essential question the SPY framework tries to answer is: 
what input range restrictions are most likely to 
constrain the state of the model to states that are considered 
more desirable?
SPY does not use formal methods to investigate the models 
under question.
%and hence does not suffer that 
%theoretical restriction on the type of input values
Instead the SPY framework includes an execution engine for driving the models 
under examination.  
SPY executes the model a prescribed number of times generating a 
set of input-output pairs.  
The desirability of these pairs is evaluated by 
an objective function.
SPY then finds correlations between 
input-output pairs and their desirability by using tar4 
(see \tion{tar3Details} for a description of tar4).
This cycle of executing the model, objective function 
evaluation, and data mining is called an iteration.  
The SPY framework runs for several iterations, 
with the learner finding treatments in between each iteration.  
Notice this is the same work flow as ITL's work flow,
discussed in \chap{itl}, in particular in 
\fig{modelControl}. 

During each iteration the SPY framework randomly 
chooses inputs for the models 
according to range restrictions on the input variables.  
These restrictions are initially 
described by the analyst, 
but after the first iteration are modified by SPY's learning process.  
The restrictions take the form of upper and 
lower bounds for each input value.  
SPY reduces the space it searches by 
increasing the lower bound and/or decreasing the 
upper bound according to the treatments returned 
at the end of each iteration.
Hence the points that are randomly sampled during 
one iteration are always from a space smaller 
than the space sampled from during the previous iteration.  
However, rather than just using the treatments themselves
as the upper and lower bounds (as the ITL method used in
\chap{casestudies} did),
the bounds are adjusted in the {\it direction} suggested
by the treatments, but not necessarily in the {\it amount}
suggested by the treatments. 

The selection of input points from the search space is 
completely random; SPY attempts 
no symbolic analysis of the model's source code.  
This is different from other random tools, such as Reactis, 
which use heuristic analysis of the model's source code (such as 
path coverage) when picking input points. 
Refer to \cite{clark06} for a complete 
description of the SPY framework.


In addition to introducing SPY, \cite{clark06} also
applies the framework to a ``magic'' bus that tries to transport
passengers the farthest it can before running out of fuel.
While this artificial model was useful in demonstrating
the capability of SPY to learn model input constraints,
the next section returns to the original motivation for developing
SPY: verifying temporal properties in models with real valued
inputs.
To do so we will investigate three NASA flight models
and ten properties the the original model developers describe
in the requirements documentation available to us.


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