The original purpose for developing the SPY framework
was to give NASA's IV\&V 
(independent verification and validation)
facility a new method to check model
properties.
Since, as discussed in \tion{SPY}, SPY allows any
data type in the models being analyzed,
it can be used to verify properties in models
that would defeat techniques with completeness 
guarantees, like model checking.

Recall from \tion{SPY} that SPY does not perform any
symbolic analysis of the model's source code.
Some other tools, like our baseline tool Reactis,
use heuristic analysis of the model's source code,
such as trying to achieve full path coverage, when picking input points. 
SPY's selection of input points is completely random, but it
uses partial descriptions to restrict the region
of the search space that these points are chosen from.

This section
describes the models analyzed (\tion{theModels}),
the experimental goals of this analysis (\tion{modelGoals}),
and the results of these experiments (\tion{modelResults}).


\subsection{Models Under Consideration}\label{sect:theModels}
The models used in this section were originally developed in 
Simulink\footnote{Available from The MathWorks Inc, at \url{www.mathworks.com}.}.
The models were translated to the SPY language
by a LUSTRE-based translator \cite{halbwachs91synchronous}
developed as part of the SPY framework development,
at the University of Minnesota.

To gauge the effectiveness of SPY in verifying properties and 
uncovering defects, we analyzed three different models
\begin{itemize} \itemsep -14pt
\item Sensor Voting
\item Dual FGS
\item Altitude Switch 
\end{itemize}
This section will describe some of the particulars of the
models.

\subsubsection{Sensor Voting}
The Sensor Voting model\footnote{Developed at Honeywell Laboratories.}
is a generic triplex voter. 
The voter takes inputs from three redundant sensors and 
synthesizes a single reliable sensor output. 
Each of the redundant sensors produces both a measured data value 
and self-check bit (validity flag) indicating whether or not 
the sensor considers itself to be operational. 
The output of a sensor is amplitude limited in hardware 
by the A/D conversion. 

The functionality of the triplex voter is as follows: \\
\bi
{Sample digitized signals of each sensor measurement at 
a fixed rate appropriate 
for the control loop, \eg 20 Hz. A valid flag supplied by sensor hardware 
indicating its status is also sampled at the same rate.}
{Use the valid flag and comparison of redundant sensor measurements 
to detect and isolate failed sensors.}
\item Output at a specified sample rate a signal value 
computed as a composite average 
of the signals of non-faulty sensors. Also output, at the same specified rate, the status of the composite output by setting an ``outputValid'' flag. 
\item Tolerate ``false alarms'' due to noise, transients, 
and small differences in sensor 
measurements. Sensors are not marked failed if they are operating within 
acceptable tolerances and noise levels. 
\item Maximize the availability of valid output by providing an output whenever 
possible, even with two failed sensors. 
\item The algorithm is not required to deal with 
simultaneous sensor failures since this 
is a very low probability event. 
\ei

The operation of the sensor voter algorithm is as follows. 
All valid sensor signals are 
combined to produce the voter output. 
If three sensors are available, a weighted average 
is used in which the outlying sensor value is 
given less weight than those that are in closer agreement. 
If only two sensors are available a simple average is used. 
If only one sensor is available, it becomes the output. 
There are two mechanisms whereby a faulty sensor 
may be detected and no longer considered valid;
either by comparison of the redundant sensor signals or
by the validity flags produced by the sensors themselves.




\subsubsection{Dual FGS}
A Flight Guidance System is a component of the overall 
Flight Control System (FCS) in 
a commercial aircraft. 
The FGS compares the measured state of the aircraft (position, 
speed, and attitude) 
to the desired state and generates pitch and roll guidance commands 
to minimize the difference between the measured and desired state. 
The FGS subsystem 
accepts input about the aircraft's 
state from the Air Data System (ADS) and Flight 
Management System (FMS). 
Using this information, it computes pitch and roll guidance 
commands that are provided to the autopilot (AP). 
When engaged, the autopilot translates 
these commands into movement of the aircraft's 
control surfaces necessary to achieve the 
desired changes about the lateral and vertical axes. 

The flight crew interacts with the FGS primarily through 
the Flight Control Panel (FCP). 
The FGS has two physical sides corresponding to 
the left and right sides of the aircraft. 
These provide redundant implementations that communicate 
with each other over a 
cross-channel bus. 
Normally, only one FGS (the pilot flying side) is active, with the other 
FGS operating as a silent, hot spare. 
In this dependent mode of operation, the active FGS 
provides guidance values to the AP and the Flight Director (FD).
The pilot and copilot can switch which side is the 
pilot flying side by pressing the Transfer Switch on the FCP. 
This is frequently done 
when switching to a different navigation source. 
However, in some critical modes, such 
as Approach and Go Around, both sides are active and 
independently generate guidance 
values for their own FD. 
In this independent mode of operation, both sets of guidance 
values are provided to the AP, 
which first verifies that they agree within a predefined 
tolerance value. 
If in agreement, the values are averaged and executed. If not in 
agreement, the situation is annunciated to the pilot and the AP disconnects. 


\subsubsection{Altitude Switch}
The Altitude Switch (ASW) is a re-usable component 
that turns power on to a Device 
Of Interest (DOI) when the aircraft 
descends below a threshold altitude above ground level. 
If the altitude cannot be determined for more than two seconds, the ASW 
indicates a fault. 
The detection of a fault turns on an indicator lamp within the cockpit. 
The DOI is turned back off again if the aircraft ascends
above the threshold altitude plus 
some hysteresis value. 
The ASW receives a status indication from the DOI indicating 
whether the DOI is powered on. 
If the DOI does not indicate that it is powered on within 
two seconds after power is applied, a fault is indicated. 
The ASW does not apply power 
to the DOI if the DOI is already powered on. 
The ASW is not in complete control of the DOI, 
since the DOI may be turned on and off by other systems or the pilot. 
If the DOI is 
turned off after the aircraft descends below the threshold altitude, 
the ASW does not 
reapply power to the DOI unless the aircraft again 
descends below the threshold altitude. 
The ASW also accepts an inhibit signal that prevents 
it from turning on power to the DOI 
or indicating a fault. 
All other ASW functions are unaffected by the inhibit signal. 
The 
ASW also accepts a reset signal that returns it to its initial state. 



\subsection{Experimental Goals}\label{sect:modelGoals}
This section will describe the properties
we want to verify in each of the models described in \tion{theModels}.



\subsubsection{Sensor Voting}
The Sensor Voting model combines the output from 
three sensors to produce a high 
quality output.  
It operates in such a fashion as to tolerate transient errors 
or multiple failures in the sensors, 
to detect significant differences in the signals, and to 
isolate that difference (if possible) to a single faulty sensor.  
The full details of this model 
are given in \tion{theModels}.
  
For the Sensor Voting model we checked the following properties \\
\begin{enumerate} \setstretch{0.9} 
\item If sensor valid flag goes bad 3 time steps in a row, 
then the sensor output shall be flagged as bad.  
This sensor will stayed flagged as bad even if the sensor valid 
flag becomes good at a later time.
\itemsep +4pt
\item If a persistent threshold violation is detected by the model, 
the sensor output shall be flagged as bad.  
This sensor will stayed flagged as bad even if the 
persistent threshold violation disappears at a later time.
\end{enumerate}
Both these properties were applied separately for each of the three sensors.

The first property was implemented in SPY using a trio of simple
accumulators that tracked the number of consecutive time steps that
a sensor valid flag was bad.  If any of the accumulators exceeded
the 3 time steps allowed, that sensor was recorded as bad by SPY,
and if the model ever reported that sensor as good a property
violation was reported.

The second property, which measures disagreement between the
values reported by the different sensors, was a bit
more complicated to implement.
Two sensors had to disagree by an amount above a certain threshold
(Sensor Magnitude Threshold)
for a time exceeding another threshold
(Sensor Persistence Threshold).
In addition, since with only two valid sensors it would be impossible
to determine which sensor was faulty, 
all three sensors had to be considered valid by the
model for it to isolate which sensor was producing the disagreeing value.
If the objective function detected a persistent threshold violation
that was not reported by the model,
a property violation was reported by SPY.

Together these two properties were also checked in the other direction.
That is, if the objective function decided
a sensor was valid according to both criteria,
but the model reported the sensor as invalid,
a property violation was reported by SPY.

\subsubsection{Dual FGS}
The FGS compares the measured state of the aircraft 
(position, speed, and attitude) to the 
desired state and generates pitch and 
roll guidance commands to minimize the difference 
between the measured and desired state.  
\tion{theModels} gives a more detailed description of 
the Dual FGS. 

For the Dual FGS model, we checked the following properties \\
\be
{At least one FGS side shall always be active}
{Exactly one side shall be the pilot flying side. 
  This property was stated in two forms 
  \begin{enumerate} \itemsep +4pt
  \item It is always the case that property 2 holds \label{item:2wrong}
  \item It is always the case that when property 2 is false then in the next step property 2 is true \label{item:2right}
  \end{enumerate}}
\item If the system is in independent mode (defined in \tion{theModels}), both sides shall be active.  
  This property was stated in two forms: 
  \begin{enumerate} \itemsep +4pt
  \item It is always the case that property 3 holds \label{item:3wrong}
  \item It is always the case that when property 3 is false then in the next step property 3 is true \label{item:3right}
  \end{enumerate}
\item If the system is in dependent mode, it shall not be the case that both sides are active.  
  This property was stated in two forms: 
  \begin{enumerate} \itemsep +4pt
  \item It is always the case that property 4 holds \label{item:4wrong}
  \item Property 4 cannot be false for more than two consecutive time steps \label{item:4right}
  \end{enumerate}
\item Pressing the transfer switch shall cause the system to change PF sides.
 This property is expressed in two parts: 
 \begin{enumerate} \itemsep +4pt
 \item It is always the case that if the Left FGS is not the pilot flying side and the transfer switch is not pressed, then in the next step if the transfer switch is pressed, Left FGS shall become the pilot flying side.
 \item It is always the case that if the Right FGS is not the pilot flying side and the transfer switch is not pressed, then in the next step if the transfer switch is pressed, Right FGS shall become the pilot flying side.
  \end{enumerate}
\ee

Properties \ref{item:2right}, \ref{item:3right}, and \ref{item:4right}
capture the properties the developers intended the models
to have.
We checked properties \ref{item:2wrong}, \ref{item:3wrong}, 
and \ref{item:4wrong} to ensure that SPY checked for some
properties that did not hold in the model.


The first property was easy to implement by checking the two boolean 
variables used to record the status of each side of the FGS.
One side had to be active at every time step.

The second property checked the two boolean variables that recorded
which side of the FGS was giving input to the AP, 
\ie the ``flying'' side.
An accumulator was used to count the number of time steps
that both sides of the FGS were flying.
When checking property \ref{item:2wrong}, if this accumulator
was ever greater than 0, a violation was reported.
When checking property \ref{item:2right}, if this accumulator
was ever greater than 1, a violation was reported.

The third property checked that if the system
was in independent mode (defined in \tion{theModels})
both boolean variables that recorded
if a FGS side is active were set to true.
An accumulator was used to count the number of time steps
this was false.
When checking property \ref{item:3wrong}, if this accumulator
was ever greater than 0, a violation was reported.
When checking property \ref{item:3right}, if this accumulator
was ever greater than 1, a violation was reported.

The fourth property was implemented in a way similar to 
property 3.  
The accumulator was incremented if the FGS was in dependent mode 
and both FGS sides were active.
When checking property \ref{item:4wrong}, if this accumulator
was ever greater than 0, a violation was reported.
When checking property \ref{item:4right}, if this accumulator
was ever greater than 2, a violation was reported.

The final property was checked for both sides of the FGS.
If the side being checked was the flying side and the
transfer switch wasn't pressed during the current time step,
but was pressed during the previous step and the side was
the flying side in the last step, a violation was reported.


\subsubsection{Altitude Switch}

The Altitude Switch(ASW) is a re-usable component 
that turns power on to a Device of 
Interest (DOI) when the aircraft descends below a 
threshold altitude above ground level.  
Refer to \tion{theModels} for a more detailed description of the 
Altitude Switch. 

For the Altitude Switch, we checked the following properties: \\
\be{The ASW shall command the DOI to be turned on if and only if the following 
conditions are satisfied
\be{The aircraft descends below the threshold altitude (nominally 2000 ft)} 
{The DOI is not already on}
\item The ASW is not inhibited 
\item The ASW is not reset
\ee}
{The ASW shall command the DOI to be turned off if and only 
if all of the following conditions are satisfied
\be{The aircraft has attained an altitude greater than the threshold  plus hysteresis. (Hysteresis is assumed to be 0.1 * Threshold)}
{The DOI is not already OFF}
\item The ASW is not inhibited 
\item The ASW is not reset 
\ee}
\item The ASW shall indicate a fault, if any of the following conditions are satisfied: 
\be {ASW is not able to determine the altitude for more than 2 seconds \label{aswProp:31} }
{DOI does not indicate that it is powered ON within 2 seconds after ASW 
applies power to it \label{aswProp:32}}
\item Altimeter indicates that the Altitude Quality is bad \label{aswProp:33}
\item ASW is not inhibited   \label{aswProp:34}
\ee
\ee

The first two properties were very similar and checked in the same
way.  They list four conditions that must exist for the
DOI to be turned on or off.  Both simply check that all
four conditions hold when ever the DOI is turned on or off.

The third property checks that the ASW has not been inhibited
or reset and then checks that if any of the three alarm
modes (properties \ref{aswProp:31} - \ref{aswProp:33})
are true indicating that the alarm signal should be activated.

\subsection{Experimental Results}\label{sect:modelResults}
In this section we present the results of the experiments
in which we tried to verify the properties described in
\tion{modelGoals}.
Each of the models was run for 10 iterations,
with each iteration having a 100 instances batch size,
and each instance running the model for 40 discrete time steps.


\subsubsection{Sensor Voting model}
Both properties formulated for the Sensor Voting model
were not expected to be violated, and SPY
did not detect a violation of either property.
Recall from \tion{modelGoals} that property 1 said
that the sensor valid flag had to be bad 3 time 
steps in a row for the model to invalidate that sensor.
Internally in the SPY code this threshold was stored in {\tt numBadFlags}.
Additional experiments were run with the Sensor Voting
model, with {\tt numBadFlags} set to have different values.
Whenever this number differed from the 3 
(the formulation desired by the original model developers)
SPY reported a property violation,
showing that it could detect differences between 
the property formulations and the implementation
of the models.
These results are summarized in \ble{VoterResults}.

\begin{table}
\centering
\begin{tabular}{ccc}
Property & SPY Result & Expected Result \\
Property 1 & Not Violated & Not Violated \\
Property 2 & Not Violated & Not Violated \\
{\tt numBadFlags} = 2 & Violated & Violated \\
{\tt numBadFlags} = 4 & Violated & Violated \\
\end{tabular}
\caption{Sensor Voting property check results}
\label{table:VoterResults}
\end{table}

There was one subtle bug that SPY missed which was discovered by 
manual inspection .
The Sensor Voting model detects a persistent threshold violation 
(property 2 in \tion{modelGoals}) by 
accumulating the time that any sensor differs 
(above a set threshold) from any of the other sensors 
(provided that the sensors are still considered valid by the model).  
This accumulator value was stored in a floating-point variable.  
At each time step this accumulator is checked against 
the allowed time for a sensor to miscompare with the other sensors.  
However, when accumulating .05 seconds (since the model runs at 20 Hz) 
ten times, the sum was actually just below .5 seconds.  
But since both the model and the code used to check the 
model suffered from this form of numeric creep, 
SPY did not recorded a failure.  
Hence a property violation escaped SPY's notice.
Our collaborators at the University of Minnesota 
(who developed the translation system discussed in \tion{theModels})
independently checked this violation using our commercial
tool Reactis.
That tool also failed to detected this numeric creep.
Since both tools failed to detected this violation,
this example demonstrates the danger in using floating-point
variables for some applications.
After manual inspection detected this error, 
the property checking code in SPY was re-written to use
an integer accumulator to count the number of time steps
that two sensors miscompared.
Using this integer accumulator, SPY detected the property violation,
demonstrating that the original failure of SPY was due
to the numeric creep issue.
This means that SPY, when the objective function was
properly implemented, found a subtle bug that 
apparently had not been previously discovered.

\subsubsection{Dual FGS}
\ble{FGSResults} shows the different properties
and their expected results for the Dual FGS model.
The results we obtained from SPY differ from the 
expected results for only one of the nine properties
checked, property 4.b.
The FGS system was also independently check by our UMN collaborators.
Reactis also reported that property 4.b was violated.
Since this model has been in production use for some time,
it is likely that the property is formulated incorrectly
in the requirements documentation we had access to.
Even if the property formulation is incorrect and there
are no faults in the model, having consistent requirements
is obviously valuable.
Discovering inconsistent requirements, 
while not the stated goal of the SPY framework,
is always possible when testing requirements
against a development artifact.

\begin{table}
\centering
\begin{tabular}{ccc}
Property & SPY Result & Expected Result \\
Property 1 & Not Violated & Not Violated  \\
Property 2.a & Violated & Violated  \\
Property 2.b & Not Violated &  Not Violated  \\
Property 3.a & Violated & Violated  \\
Property 3.b & Not Violated & Not Violated  \\
Property 4.a & Violated & Violated  \\
Property 4.b & Violated & Not Violated  \\
Property 5.a & Not Violated & Not Violated  \\
Property 5.b & Not Violated &  Not Violated  \\
\end{tabular}
\caption{FGS property check results}
\label{table:FGSResults}
\end{table}



\subsubsection{Altitude switch model}
\ble{ASWResults} shows the results of our experiments with
the altitude switch model.
When these experiments were started it was thought that 
properties 1 and 2 should not be violated,
but when Reactis was used as an
independent check, it also reported properties 1 and 2
violated by the model.
This led to a closer examination of the requirements documentation.
It became apparent that the model's behavior was not fully
encapsulated in the properties, 
as the properties were recorded.
Since the original developers were not available to us,
this was as far as our investigation could go.


\begin{table}
\centering
\begin{tabular}{ccc}
Property & SPY Result & Expected Result \\
Property 1 & Violated & Violated  \\
Property 2 & Violated & Violated  \\
Property 3 & Not Violated &  Not Violated  \\
\end{tabular}
\caption{ASW property check results}
\label{table:ASWResults}
\end{table}



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