
\section{Discussion}

%%%%% deleted...
% \subsection{Performance Variations Between Tools}
%%%%% added...
\subsection{Performance Variations Between Verification Strategies}
\label{variations}

\begin{figure}
\begin{center}
\includegraphics[width=3in]{min-max-time.pdf}
\caption{Specifications plotted to show maximum and minimum time
  requirements for any tool.}
\label{f:min-max-time}
\end{center}
\end{figure}

Figure \ref{f:min-max-time} shows each fault-seeded specification,
excluding equivalent mutants, plotted as a point whose x-coordinate
is the maximum time required for any tool to detect a property
violation and y-coordinate is the minimum time required for any tool
to detect a property violation.  For example, the point in the lower
right corner of the largest dotted box represents a specification
for which the fastest tool to detect a property violation required
about 0.020 seconds, while the slowest tool to detect a property
violation required about 20 seconds. Points plotted with an
x-coordinate of infinity represent specifications for which one or
more tools were never able to detect a property violation,
regardless of time allotted.  Nearly half of fault-seeded
specifications for which a fault was detected are in this category.
%(equivalent mutants are not shown in figure \ref{f:min-max-time}).
Two reasons why there were such a large number of specifications for
which one or more tools could not detect a violation are 1) Cadence
SMV and NuSMV could not check 6 of the 15 properties, since
two-state assertions are not compatible with the SCR Toolset's SMV
translator; and 2) although Lurch was able to check for violations
of all 15 properties, it is incomplete.

\begin{figure}
\begin{center}
\includegraphics[width=3in]{min-max-memory.pdf}
\caption{Specifications plotted to show maximum and minimum memory
  requirements for any tool.}
\label{f:min-max-memory}
\end{center}
\end{figure}

Figure \ref{f:min-max-memory} is similar to Figure
\ref{f:min-max-time}, except that points represent the maximum and
minimum \textit{memory} required by the tools.  Again, points
plotted with an x-coordinate of infinity represent specifications
for which one or more tools were unable to detect any property
violation.

These figures are meant to illustrate the complementary
relationships between tools used in our experiments.  If tools were
not complementary, we would expect to see points plotted along a
45-degree line from the origin to the upper right corner of the
graph, indicating that specifications easy for a given tool are easy
for all tools and that specifications difficult for one tool are
difficult for all tools.  We do see a large set of specifications
(122) easy for all tools.  For these specifications, no tool
requires much more than 10 seconds or 100 megabytes. But nearly all
specifications that represent significant challenges for some tools
require less than 100 seconds (107 specifications) or less than 50
megabytes (103 specifications) for at least one other tool.  That
is, regarding performance, the tools are complementary:  nearly all
specifications are relatively easy to check for at least one of the
verification tools, including specifications difficult or impossible
for one or more other tools.


\subsection{Tool-Specific Lessons Learned}

For each verification tool used in our experiments---Salsa, SMV,
NuSMV, Lurch and SPIN---we list here characteristics of the tool
brought out by comparison of that tool's results with results from
other tools.
%%%%% added... (disclaimer)
Note that comparisons below are based on input models using SCR-specific
translation tools available to us.  We do not intend to suggest general
conclusions about the relative performance of the verification tools.
%The SCR Toolset not included, since our focus here is
%on developing a verification strategy effective on models that have
%already passed all of the checks implemented in the SCR Toolset GUI.
%The assumption is that back-end verification tools would only be
%used after a specification has already passed the SCR Toolset's
%generic checks.
%

Salsa is generally slower than Cadence SMV but faster than NuSMV, Lurch and SPIN, and requires
very little memory.  Assertions and generic properties can be proved automatically using
Salsa, but any assertions that Salsa fails to prove must be checked manually or with some
other tool.
%Salsa's ability to prove a particular assertion is, at least in our experiments,
%independent of the presence or absence of other assertions in the specification.  So, for
%example, if a copy of the specification is made for each assertion, so that only one
%assertion is present in each copy, and Salsa is run on each copy, we do not find that
%Salsa is able to prove any more assertions than if it were run on a single copy that
%includes all of the assertions.

Although some interesting variations were observed in the performance of other tools
running on sets of specifications categorized according to classes of Salsa results,
none of these variations can be readily exploited in a multiple-tool verification strategy.
However, as shown in the next section, if assertions proved by Salsa are removed from
a specification it may greatly improve SPIN's performance.  Also, \texttt{NATURE}
constraints in an SCR specification are compatible with Salsa but not with SPIN or
Lurch (assuming models are generated from the automatic SPIN translator included with
the SCR tools).  So Salsa can be used to automatically validate assertion violations reported
by SPIN or Lurch, which may be just the result of ignoring \texttt{NATURE} constraints.
Since Salsa is not complete, however, some violations may still need to be validated
manually using the SCR Simulator.
%\footnote{% \ssp One additional minor
%point about the use of Salsa within the framework of the SCR tools:  the filename
%of the SCR specification must not include a hyphen (-), or else the
%automatically translated Salsa version of the specification will not
%work with Salsa.}


As stated in section \ref{motivation}, the SMV version of a specification generated
by the SCR Toolset requires minor modifications to be compatible with NuSMV.
With these changes, results from Cadence SMV and NuSMV were consistent, in terms of accuracy,
in all our experiments.  We found also that Cadence SMV was consistently faster and required
less memory, although NuSMV resource requirements were still small compared to SPIN.
Since Cadence SMV was faster we use it in the combined strategy described in the next section.
Depending on the application it may be preferable to use NuSMV, however, because it is
an open-source tool with a less restrictive license.

As far as the differences between Cadence SMV and Salsa, Lurch or SPIN, Cadence SMV is 1) very fast,
and requires very little memory, 2) respects \texttt{NATURE} constraints (like Salsa),
and 3) can only verify single-state assertions.  Thus it makes sense to run Cadence SMV first.
If an assertion violation is detected, it should not need to be validated by another tool, since
\texttt{NATURE} constraints are respected (of course it can be validated by another
tool if desired).  If no error is detected, all single-state assertions can be removed
from the model before running other tools to check two-state assertions.


Lurch is usually slower than Salsa, Cadence SMV and NuSMV, but often faster than SPIN, at
detecting assertion violations.  Lurch is able to check both single state and two-state
assertions, but assertion violations reported by Lurch must be validated, because the
input model for Lurch is generated from the SCR Toolset's SPIN version of the specification,
which ignores \texttt{NATURE} constraints.  Lurch is incomplete, so if no assertion
violations are detected by Lurch a complete tool (i.e., SPIN) must be used to fully
verify the specification.

%In the simple performance-based multiple tool verification strategies described
%in chapter \ref{motivation}, Lurch was run until
%an arbitrary time cutoff, set at 7 seconds.
%This was approximately optimal, but a cutoff value anywhere between
%1 and 30 seconds produced similar results.  Still, it would be preferable to have a
%generally applicable cutoff value not related to running time.  For this reason we
%propose below to use Lurch's \textit{saturation} statistic, a measure of the ratio of
%new states to repeat states explored by the search.  A saturation-based cutoff value
%of 25\%, which roughly corresponds to the 7 second time cutoff used in the PACS
%experiments, is used in the final set of experimental results presented below.
%

Within our experimental framework, comprised of the SCR Toolset, our script for generating
Lurch input models, and minor modifications necessary for NuSMV and SPIN described
in section \ref{motivation}, the only tool capable of fully verifying all types of assertions
present in an SCR specification is SPIN.  So, although SPIN in some cases requires far
more time and memory than other tools, it is a necessary component of any complete
verification strategy.  We should point out also that SPIN's completeness is related
to its resource requirements.  If, for example, a translator was written to produce
SMV input models so that two-state assertions could be checked
by SMV, this might increase Cadence SMV's time and memory requirements significantly.

The input model generated by the SCR tools for SPIN encloses code representing transition
tables in a \texttt{d\_step} block, which saves time and memory but is valid only if
all tables are disjoint.  In general, the final \texttt{d\_step} marker must be removed
to fully verify the specification.  In practice, it may also be necessary to use
memory compression options and increase the depth limit for the verification run
to terminate, as we have in the PACS specification experiments.  We found that only
SPIN's \textit{minimized automaton} compression option, the slowest but most memory-efficient
lossless compression available in SPIN, was sufficient to enable full verification
of the PACS specification.  We also had to increase the depth limit from the default
value of 10,000 to 3.2 million.

\subsection{A General Multiple-Tool Verification Strategy}

\begin{figure*}
\begin{center}
\includegraphics[width=6.5in]{combo2.pdf}
\caption{Combined strategy exploiting complementary variations in
  performance and accuracy. % (Baseline complete and single-tool
  %complete strategies enclosed in dotted boxes.)
  }
\label{f:combo2-flow-chart}
\end{center}
\end{figure*}

Figure \ref{f:combo2-flow-chart} shows a flowchart representing a
multiple-tool verification strategy inferred from both performance
variations and characteristics of tools, in the context of the SCR
Toolset, relevant to the accuracy of verification results.
First, we run Cadence SMV to either detect a fault or prove all
single-state assertions. If no fault is detected, single-state
assertions are removed from the model and we run Salsa, to attempt
to prove some or all of the two-state assertions.  Any two-state
assertions proved by Salsa are then removed from the model.  If all
assertions have been proved at this point, the model is correct.

If there are still assertions to be checked in the model, Lurch is run next
to detect violations of these remaining two-state assertions.  Rather than an arbitrary
time cutoff, Lurch is run to 25\% saturation.  If Lurch detects a fault, we stop.  It
is possible at this point that the fault detected by Lurch is not actually present in the
model, due to Lurch's ignoring \texttt{NATURE} constraints, so it needs to be validated.
%%%%% added... (in response to reviewer 3's question)
(In our experiments just 2 of 323 mutant specifications contained spurious property violations
when \texttt{NATURE} constraints were ignored.)
%%%%%
Although we mentioned above that assertion violations detected by Lurch or SPIN can
sometimes be confirmed or disconfirmed automatically using Salsa or Cadence SMV, if a violation
is detected at this point in the flowchart by Lurch it must be validated manually using
the SCR Simulator, because
Salsa and Cadence SMV have already been run, and any violation that would have been disconfirmed
by Salsa or Cadence SMV has already been removed from the model.

If Lurch does not detect a fault, SPIN is run next with default
options.  This is the fastest and the most memory-expensive mode in
which to run SPIN.  It is incomplete, because of the depth limit of
10,000 states, but often detects assertion violations very quickly.
If SPIN with default options detects no assertion violation, SPIN is
next run with options set to allow the run to terminate normally. In
our experiments this required using the minimized automaton
compression option described in the previous section (set to 28) and
increasing the depth limit to 2 million.  Finally, if no violation
is detected with these options SPIN is run again, with options set
to allow a full verification run, on a modified version of the input
model with the final \texttt{d\_step} marker removed.  In our
experiments, in order to get a full verification run on input models
modified in this way we again used the minimized automaton
compression and increased the depth limit to 3.2 million.


The dotted rectangles in figure \ref{f:combo2-flow-chart} show two alternative complete
verification strategies using only SPIN.  The outer rectangle shows how SPIN might be used
interactively, modifying settings as needed to minimize resource requirements on models
for which violations can be detected quickly, but to enable full verification eventually.
The inner rectangle shows how SPIN would be used if it were to be run once on each
input model with options preset to enable full verification.
