
\section{Motivating Examples}
\label{examples}

%%%%% deleted...
% This section presents three examples in which multiple verification
% tools were run on the same SCR input model and produced inconsistent
% results.
% In each case the inconsistency was eventually resolved,
% and we gained a better understanding of the tools in the process.
% Also, in each case a single tool would have offered an invalid
% verification result, even though the tool had been used correctly.
%%%%% added...
This section presents three examples in which different verification
strategies produced inconsistent results when run on the same SCR input
model.  In each case the inconsistency was eventually resolved, and we
gained a better understanding of the translation and verification tools
in the process.  Also, in each case it would have been possible to use
a single verification strategy to get an invalid result, with no indication
that translation and verification tools had been used incorrectly.
%%%%%
The first two examples illustrate a key limitation in the use of
model checking tools: although a fault detected by the tool can be
%%%%% One reviewer wants "discarded" instead of "disconfirmed" in the
%%%%% sentence below but that doesn't make sense to me.
%%%%% (It's a word:  http://mw1.m-w.com/dictionary/disconfirm)
manually confirmed or disconfirmed by inspecting the counter example
trace provided by the model checker, if the model checker reports
that the model is correct no proof is generated to certify this
result.
%%%%% added... (for reviewer 3)
(Others have developed ways to determine whether a the ``all clear'' result
from a single model checker is valid \cite{chockler06}; in this work we
show how multiple tools can be used to validate each other without detailed
knowledge of any particular tool.)
%%%%% deleted...
% Still, this result can be examined by another model checking
% tool.
% In the third example, the inconsistency brought to light is
% not as critical as the inconsistencies found in the first two
% examples.  In the third example, rather than preventing a violation
% from being missed, we showing that a violation reported by one tool
% is actually not present in the original input model.
%%%%% added...
In the third example, the inconsistency brought to light is less
critical:  the use of multiple strategies, rather than preventing a violation
from being missed, has the practical benefit of showing that a violation
detected by one strategy is not actually present in the original input model.


\subsection{Inconsistent Results from Two Symbolic Model Checkers}
\label{utpb527}

\begin{figure*}
\begin{center}
\begin{tabular}{l}
\begin{minipage}{5in}
\scriptsize \tt
\begin{verbatim}
Copyright 1996 Cadence Berkeley Labs. Cadence Design Systems...

Model checking results
======================
(AG (((~(cGuardAlarm=On))|(cUserDisplay=SeeOfficer))&((~(cUserDisplay=.....false
\end{verbatim}
\end{minipage} \\ \\ \hline \\
\begin{minipage}{5in}
\scriptsize \tt
\begin{verbatim}
*** This is NuSMV 2.4.1 zchaff (compiled on Tue Jan 30 19:33:47 UTC 2007)...

-- specification AG ((!(cGuardAlarm = On) | cUserDisplay = SeeOfficer)
  & (!(cUserDisplay = SeeOfficer) | cGuardAlarm = On)) is true

\end{verbatim}
\end{minipage}
\end{tabular}
\caption{Inconsistent outputs from Cadence SMV (top) and NuSMV (bottom) running
on the same fault-seeded specification.}
\label{f:smv_output}
\end{center}
\end{figure*}

Figure \ref{f:smv_output} shows the outputs from two versions of the
SMV symbolic model checker, Cadence SMV \cite{mcmillan00} and NuSMV
\cite{cimatti00}, running on the same input model.\footnote{For
clarity many lines of output have been deleted in this figure and
similar figures below.}  The model was generated automatically from
the specification of a security system, written in the SCR modeling
language and described in more detail in section \ref{case-study}.
As shown in Figure \ref{f:smv_output} Cadence SMV and NuSMV disagree
about whether one of the assertions included in the input model is
true or false---the assertion \texttt{(cGuardAlarm = On) <=>
(cUserDisplay = SeeOfficer)}.

The input model in this example was generated from a fault-seeded
version of the specification known to be correct in the original
version.  The fault-seeded version contained two mutations,
so our first step in attempting to resolve the inconsistency between
Cadence SMV and NuSMV was to look at the results from running these
tools on input models generated from specifications that each had
just one of the mutations.  Results on these single-mutation
versions were consistent:  for an input model with just the first
mutation, both Cadence SMV and NuSMV reported that all assertions
included in the input model were true; for an input model with just
the second mutation, both Cadence SMV and NuSMV reported that the
assertion \texttt{(cGuardAlarm = On) <=> (cUserDisplay =
SeeOfficer)} was false.  This suggests that the assertion violation
reported by Cadence SMV is present in the input model, but somehow
masked by the first mutation for NuSMV.

\begin{figure*}
\begin{center}
\begin{tabular}{l}
\begin{minipage}{5in}
\scriptsize \tt \begin{verbatim}
Depth= 500129 States= 1e+06 Transitions= 1.02631e+06 Memory= 72.780...

pan: assertion violated (( !((cGuardAlarm_NEW==0))||(cUserDisplay_NEW==9))
  &&( !((cUserDisplay_NEW==9))||(cGuardAlarm_NEW==0))) (at depth 859760)...

(Spin Version 4.2.4 -- 14 February 2005)...

State-vector 32 byte, depth reached 859769, errors: 1

\end{verbatim}
\end{minipage}
\end{tabular}
\caption{Output from SPIN running on a model generated from the same fault-seeded
specification used to generate the models for which Cadence SMV and NuSMV outputs
are shown in figure \ref{f:smv_output}.}
\label{f:spin_output}
\end{center}
\end{figure*}

To confirm the Cadence SMV result, we ran SPIN on an input model
generated from the same fault-seeded specification.  Figure
\ref{f:spin_output} shows the result from SPIN, consistent with the
result from Cadence SMV.
%%%%% deleted...
% Based on this, we contacted the developers
% of NuSMV and via several emails determined the reason for NuSMV's
% incorrect verification result for the example input model.  Although
% the input model was syntactically valid for NuSMV, the keyword
% \texttt{SPEC} used to mark assertions is not interpreted the same
% way by NuSMV as by Cadence SMV.
%%%%% added...
Based on this, we contacted the devlopers of NuSMV and via several emails
determined that the SCR-to-SMV translator we were using produced a syntatically
correct but outdated input model.  Specifically, the keyword \texttt{SPEC}
used to mark assertions was not being interpreted the same way by NuSMV as
by the older Cadence SMV.
%%%%%
As a result, NuSMV was checking
assertions in the input model only for a limited set of possible
execution paths.
%%%%% deleted...
% To force NuSMV to check assertions for all valid
% execution paths, it was necessary to replace \texttt{SPEC} with a
% NuSMV-specific key word, \texttt{INVARSPEC}.
% After doing this and
% running NuSMV on the modified input model, the output was consistent
% with Cadence SMV, reporting a violation of the assertion.
%%%%% added...
By replacing \texttt{SPEC} with \texttt{INVARSPEC} in the input model
before running NuSMV, we were able to get the desired behavior.
After making this change the output from NuSMV was consistent with
Cadence SMV, reporting a violation of the assertion.

%%%%% deleted...
% This example might be dismissed as not relevant to the question of
% whether a particular verification tool is more accurate than
% another.  The cause of the inconsistency between NuSMV and Cadence
% SMV was not a bug in either tool, but an incompatibility between the
% automatic translation tool used to generate the input model (which
% used \texttt{SPEC} rather than \texttt{INVARSPEC} to mark
% assertions) and the NuSMV input language.  From the point of view of
% the user, however, the cause of inconsistency is irrelevant.  A
% model checker, after a full verification run, reported that an
% incorrect input model was correct. It is only because this output
% was compared to that of other verification tools that was it shown
% to be incorrect and eventually corrected.
%%%%% added...
The inconsistency between NuSMV and Cadence SMV in this
example was not due to a bug in either tool, but to an outdated translator.
A more experienced user of NuSMV may have seen right away that the input model
produced by the translator wasn't right.  For us, however, it is only
because the output produced by NuSMV was compared to that of other
verification tools that we discovered and corrected the translation problem.

\subsection{Inconsistent Results from Model Checking and Random Search}
\label{utpb23}

\begin{figure*}
\begin{center}
\begin{tabular}{l}
\begin{minipage}{5in}
\scriptsize \tt
\begin{verbatim}
Depth= 500129 States= 1e+06 Transitions= 1.02631e+06 Nodes= 19616 Memory= 144.710...

(Spin Version 4.2.4 -- 14 February 2005)...

State-vector 32 byte, depth reached 1714629, errors: 0
\end{verbatim}
\end{minipage} \\ \\ \hline \\
\begin{minipage}{5in}
\scriptsize \tt
\begin{verbatim}
time  memory   states  sts/sec  % new   col  depth    name...

9.08   7.55   1.2e+05  1.3e+04   49.0     0    155    _assert6_violated

\end{verbatim}
\end{minipage}
\end{tabular}
%%%%% deleted...
% \caption{Inconsistent outputs from SPIN (top) and Lurch (bottom) running
% on the same fault-seeded specification.}
%%%%% added...
\caption{Inconsistent outputs from SPIN (top) and Lurch (bottom) running
on input models generated from the same fault-seeded specification.}
%%%%%
\label{f:splu_output}
\end{center}
\end{figure*}

Figure \ref{f:splu_output} shows outputs from the explicit-state
model checker SPIN \cite{holzmann03} and our tool Lurch running on
input models generated from a second fault-seeded version of the
security system specification mentioned above.\footnote{For a more
detailed explanation of the example described here see
\cite{owen06}.}  SPIN reports that the input model is correct but
Lurch reports an assertion violation.  Because Lurch is an
incomplete tool, which can detect property violations but not verify
correctness, we would expect to sometimes see violations missed by
Lurch but detected by SPIN.  We would not expect the result shown 
here:  Lurch, an incomplete tool, reports a
violation, while SPIN reports no violation.

Unlike the example in the previous section, in which NuSMV and
Cadence SMV were run on the same input model, in this case SPIN and
Lurch ran on two different input models, generated from the
fault-seeded specification using two different translation tools. We
initially assumed that the inconsistent outputs shown in Figure
\ref{f:splu_output} were due to an error in the translator to
generate the Lurch input model, since it was newly developed as
part of the research presented here. So, to determine whether the
property violation detected by Lurch was present in the original
fault-seeded specification and not due to an error in the
translator, we used an SCR simulation tool to step through the
fault-seeded specification according to the execution trace output
by Lurch.

\begin{figure*}
\begin{center}
\begin{tabular}{l}
\begin{minipage}{5in}
\scriptsize \tt
\begin{verbatim}
--- Initial State --------------------------------------
mDigit4 = Blank                         tNumCReads = 0...

--- State 36 -------------------------------------------
DISJOINTNESS ERROR: Function cGuardDisplay can be assigned both Blank and
SeeOfficer.  The first comes from the discriminant at row 1 column 1.  The
second comes from the discriminant at row 1 column 2.  Using first assign.

\end{verbatim}
\end{minipage}
\end{tabular}
\caption{Simulator log produced by stepping through execution trace output
by Lurch.}
\label{f:sim_output}
\end{center}
\end{figure*}

Figure \ref{f:sim_output} shows part of the log produced by stepping through
the fault-seeded specification.  The log indicates that one of the functions in the specification is
not \textit{disjoint}; that is, the function is nondeterministic as a result of overlap between
two conditions that should be mutually exclusive.  This general disjointness
error does not necessarily mean that a specific assertion in the specification
will be violated.
We observed, however, that the translation tool used to
generate the input model for SPIN uses a feature of the SPIN input language
in a way that would not be compatible with the nondeterminism indicated by
the disjointness error shown in Figure \ref{f:sim_output}.  % is this confusing?

The SPIN input language allows blocks to be marked as deterministic
steps with the key word \texttt{d\_step}.  SPIN assumes such blocks
are deterministic and therefore checks only one path through
the block.  For blocks that are not deterministic, this results in
some of the behavior of the input model being ignored.  For the
fault-seeded specification in this example, that ignored behavior
happened to include a violation of one of the assertions, the violation
detected by Lurch.  After removing the relevant \texttt{d\_step}
marker from the input model and running SPIN again, it quickly
detected the assertion violation previously detected only by Lurch.

In this experiment, if only the SPIN had been used, there would have
been no way of knowing that this particular specification had a
disjointness error and a related assertion violation.  And this is
not because of any bug in SPIN, but because of an assumption made in
the translation---an assumption which makes sense most of the time
and greatly improves SPIN's performance on automatically translated
models, but an assumption that was not valid in this case.  Using
Lurch as well, we were able to uncover this assumption and better
understand how to use SPIN to get accurate verification results.

\subsection{Inconsistent Results from an Invariant Checker and a Model Checker}
\label{sasp}

\begin{figure*}
\begin{center}
\begin{tabular}{l}
\begin{minipage}{5.7in}
\scriptsize \tt
\begin{verbatim}
Analyzing SAL specification in file: utpb28.ssl.sal.
Checking disjointness of all modules...

Checking coverage of all modules...

Checking guarantees in all modules...

Checking PINEntry ... (1,0,1):0 - (1,1,0):0 pass...
\end{verbatim}
\end{minipage} \\ \\ \hline \\
\begin{minipage}{5.7in}
\scriptsize \tt
\begin{verbatim}
Depth=  499462 States=   1e+06 Transitions= 1.02634e+06 Nodes=   17543 Memory= 60.608
pan: assertion violated ((mPINInput_OLD==mPINInput_NEW)||((mcStatus_OLD==10)||(mcStatus_OLD==5)))
  (at depth 833676)...

(Spin Version 4.2.4 -- 14 February 2005)...

State-vector 32 byte, depth reached 833689, errors: 1

\end{verbatim}
\end{minipage}
\end{tabular}
\caption{Inconsistent outputs from Salsa (top) and SPIN (bottom) running
on input models generated from the same fault-seeded specification.}
\label{f:sasp-output}
\end{center}
\end{figure*}

Figure \ref{f:sasp-output} shows inconsistent results from the
invariant checker Salsa \cite{bharadwaj00} and the model checker
SPIN running on input models generated from a third fault-seeded
version of the security system
specification used in the previous two examples. Salsa, a
specialized tool implementing ideas from model checking and theorem
proving to prove assertions in SCR models, is described in more
detail in section \ref{framework}. Salsa reports that the property
\texttt{PINEntry} is true (top of Figure \ref{f:sasp-output}) but
SPIN reports a violation of the assertion corresponding to the
property. As discussed in section \ref{framework}, Salsa is capable
of proving properties true; however, if a property cannot be proved
true by Salsa it is not necessary false.  In this way Salsa is
different from a model checker like SPIN, which is designed to
detect only genuine property violations.  Strangely, in this example
SPIN reports a violation of a property proved true by Salsa.

Eventually, we determined the reason for this inconsistency: again,
it was due to the translation tool, which ignores a feature of the
SCR modeling language when translating to SPIN.  SCR
allows the use of \texttt{NATURE} constraints to limit the behavior
of variables representing inputs from the environment.
%%%%% added...
Using
\texttt{NATURE} constraints, environment
variables and variable change events may be directly linked in ways
that would be very difficult to represent in Promela, SPIN's input
language.  And ignoring \texttt{NATURE} constraints does not cause
SPIN to miss property violations, since they can only be used to limit
modeled behavior.  So it makes sense that the translator would ignore them.

In this case
one of the \texttt{NATURE} constraints is necessary in the model for
the property \texttt{PINEntry} to be true.  Thus Salsa, running on
an input model including the relevant \texttt{NATURE} constraint,
found that the property \texttt{PINEntry} was true.  But SPIN,
running on a model without the constraint, found a violation of the
property.  This explanation of the discrepancy between Salsa and
SPIN was confirmed by removing the constraint from the Salsa input
model.  Rerunning Salsa on an input model without the constraint, we
found that Salsa could no longer prove the property true.

This inconsistency is less critical than the two in the previous examples,
because there was no possibility of missing a genuine property violation.  But it does show
a practical benefit of combining complementary strategies.
If only SPIN
%%%%% added...
(and hence only the \texttt{NATURE}-ignoring translator)
%%%%%
were used,
much manual effort might be expended attempting to find and correct the input
model so that the property \texttt{PINEntry} would not be violated.  Using Salsa
makes it unnecessary to track down the cause of the violation found by SPIN.
In addition, this example underscores the need to validate faults detected by
SPIN or any model checker.  The fault may be related to a mistake in the portion
of the input model representing the environment rather than the critical system
to be verified.
