

\section{Conclusion}


Automatic verification tools offer great benefits to developers of
complex and critical software systems.  These tools can be used to
detect subtle, non-repeatable errors that would be extremely
difficult to find through conventional testing or manual inspection
of source code. Still, developers remain skeptical because of the
costs, in user effort and expertise, and in computing resources, of
using these tools. These costs may be divided into two general
categories, along the lines of the traditional distinction between
validation and verification in software assurance.  There is the
cost of building an abstract model and property specification that
together accurately represent the essential behavior of the system
to be verified (validation), and there is the cost, in computational
resources and user expertise in the chosen verification method, of
verifying that the model and properties are consistent with each
other.

These two categories of costs, validation cost and verification
cost, are not at all independent from each other:  action to
decrease one may increase the other in unexpected ways.  For
example, validation cost is decreased if it is possible to
automatically translate the software model into the language
required by a verification tool.  But automatically generated models
tend to be less efficient, compared to carefully handwritten models,
and require much more time and memory for verification.  On the
other hand, verification cost may be greatly decreased by
restricting the input language of the verification tool, but this
makes it much more difficult to create accurate input models,
because the models likely represent systems that could be much more
more elegantly expressed in a less restrictive language.

In this article we considered a specific modeling and verification
framework, the SCR Toolset, including the consistency checker and
its command-line version, \textit{testtool}, and several integrated
back-end verification tools.  For the case study experiments, we
used the Salsa invariant checker for SCR specifications, the Cadence
SMV and NuSMV symbolic model checkers, the SPIN explicit-state model
checker, and our Lurch random search tool for debugging formal
models.
%%%%% deleted...
% Lurch works in some ways like an explicit-state model
% checker, but instead of carrying out a systematic, complete
% exploration of the behavior represented in the model, it explores a
% series of random paths through the model.

In attempting to use this wide range of tools, we initially expected
the primary validation challenge would be to make sure that automatic
translation, from the original SCR specification to input models for Salsa,
Cadence SMV, NuSMV, SPIN and Lurch, was done correctly.
Over time, however, with more experience using
the automatic translators and verification tools, our view of the validation
challenge shifted:  the challenge is not to make sure that all translators
produce \textit{correct} output, where \textit{correct} is understood
to mean perfectly equivalent models for each verification tool.
Instead, the primary validation challenge is to clearly understand the differences
between the models produced by each translator.  It is actually beneficial to have different,
non-equivalent versions of the model, at different levels of abstraction and with different
features present.  Verification results are validated when results from different verification
tools, running on different (i.e., non-equivalent in behavior) models of the system, can
be synthesized into a coherent whole.

Likewise with verification strategies, the goal should not be to
simply make sure they all produce equivalent results and then pick
the one with the best performance.  Instead, it is desirable that
they be complementary, in terms of what kinds of defects they can
detect and the kinds of properties they can prove. Further, it is
 likely that their performance will be complementary too.
%, so that it
%is not possible to simply pick the \textit{one} with the best
%performance.
Rather than a single best strategy for efficient, scalable
verification, we confirm the reports that different strategies have
different strengths and weaknesses.  Not only will a particular
strategy be preferable for certain classes of input models, but, for
a single input model, changes to the model that seem insignificant
can make a large difference in the effectiveness of a particular
verification strategy.

By combining diverse strategies for verification, we can increase the scope
of the overall strategy, so that a wider range of properties can be checked,
and we can increase confidence in the validity of the results of the verification,
as different tools confirm or disconfirm each other's results.  In addition,
combining strategies with complementary performance makes it possible to integrate
incomplete but efficient strategies, such as random search, without sacrificing
the completeness of the overall strategy, so that much more time (or memory)
consuming methods are used only when absolutely necessary.


\begin{figure}
\begin{center}
\includegraphics[width=3in]{bojan-diagram.pdf}
\caption{A conceptual model of the challenges involved in using automatic
verification tools.}
\label{f:bojan-diagram}
\end{center}
\end{figure}

Figure \ref{f:bojan-diagram} is meant to illustrate some of the
challenges described previously in this section and, along with
that, how these challenges may be addressed by a combination of
diverse modeling and verification strategies. At the center of
Figure \ref{f:bojan-diagram} is the \textit{specification}, or more
generally, the software artifact, which may be anything from prose
requirements to source code, along with properties to be verified in
whatever form available.  The specification and properties must be
translated into a formal description suitable for verification and
then verified. Thus the information from the specification moves
through a \textit{validation space}, in which the goal is to
generate accurate models capturing necessary and sufficient
information, to a \textit{verification space}, in which the goal is
to efficiently determine whether the part of the specification
representing behavior is consistent with the part of the
specification representing desired properties.

We offer two general contributions. First, we proposed that
complementary translation (and modeling) strategies should be
combined to address accuracy issues in the validation space. Second,
we demonstrated that complementary verification strategies can be
combined to address performance issues in the verification space.
Through the experiments presented above, we have attempted to show
how multiple translation and verification techniques, available
within the framework of the SCR Toolset and integrated back-end
tools, can be combined to achieve higher confidence and decreased
user effort and computational cost.
% for software specifications written in SCR.

The SCR tools' translators used
in our experiments are complementary, for example, in the sense that the output
for SMV is a smaller model than the output for SPIN, and so can be verified more
efficiently; yet the output for SPIN is a more complete representation of the
specification, including both single-state and two-state assertions, so verification
using SPIN is more comprehensive.  Also, the
Salsa and SMV models generated by the SCR tools respect \texttt{NATURE} constraints,
which is relatively easy to do in the input languages for these tools.  But the
output for SPIN does not---to do so would require much additional complexity in
the portion of the model representing the environment.

Verification tools used in our experiments were complementary as
well.  SPIN was slowest, and required the most memory, but is the
only tool capable of fully verifying SCR
specifications,
%%%%% added...
because of the translators used in our experimental framework.
%%%%%
Salsa, Cadence SMV and NuSMV sometimes proved
particular properties much more quickly than SPIN, and running SPIN
on specifications with these already proven properties removed was
much less time consuming than running SPIN with these properties
still present in the model. Cadence SMV, NuSMV and Lurch detected
property violations in certain specifications more quickly than
SPIN, and for these specifications a more time-consuming SPIN run
was not necessary.  In addition, SPIN showed significant performance
variations from one fault-seeded specification to another.  Some
specifications contained property violations almost as difficult for
SPIN to detect as it was for SPIN to verify the correct model.
%%%%% Reviewer 3 would like more explanation here.  But we don't really
%%%%% have any good conclusions about *why* certain specifications'
%%%%% violations were so much harder for SPIN.
But
for many of these same specifications, property violations could be
detected very quickly using Cadence SMV, NuSMV or Lurch.

What would the ideal set of tools for verification look like?  We
suggest that it should look like the one in Figure
\ref{f:bojan-diagram}. Multiple strategies for improving the
scalability of automatic verification would be integrated, through
multiple tools, or possibly through multiple scalability strategies
available in the same tool.  These strategies would be
complementary, some emphasizing quick proof of a subset of the
properties (as Salsa and SMV were used in our experiments) and some
emphasizing quick detection of errors (as SMV, Lurch, and SPIN in
the first two modes, were used in our experiments).  For each
strategy, translation methods would be available at different levels
of abstraction, some emphasizing similarity to the behavior of the
source model and property specification (to address validation
challenges) and some emphasizing structural simplicity (to address
verification challenges).  If these kinds of translation and
verification tools are available, combination strategies like the
one we proposed for SCR will provide better performance and higher
confidence in the verification result.

%\section{Open Research Questions}
%%
%
%The experiments presented above were done on a software specification
%with relatively simple structure, carefully written by experts in the modeling language
%and related tools, as an example of how to write a clean, high quality software specification.
%After a significant amount of effort we developed a strategy combining several tools in a way
%that allowed us to more effectively verify fault-seeded versions of the specification.
%Though the effort was significant, in our case there was less work to do, because
%we started with a software artifact very carefully written in a formal modeling language,
%and much of the work was already done---other than the translator from the SCR Toolset's
%SPIN version of the model to Lurch, which we developed, all verification tools and automatic
%translators were already integrated within the SCR Toolset.  Readers might reasonably
%wonder whether our results, however interesting, could be applied in a situation where
%the model, properties, and integrated verification framework are not already available.
%Our results are probably more applicable to researchers working on modeling and verification
%tools than to software developers, unless they are working within the framework of the SCR
%Toolset.  We suggest further work on integrated frameworks, along the lines of
%figure \ref{f:bojan-diagram}.
%
%Our results indicate complementary relationships between verification strategies, in terms of
%time and memory required to detect property violations in fault-seeded software models.
%Based on these results, we advocate using a combination of tools.  But we have not
%attempted to understand \textit{why}, for each of these strategies, some input models
%are much easier to check than others.  Is there something measurable about the structure
%of a formal model that could be used to predict the performance of a particular verification
%strategy?  For example, for deterministic, complete search methods, we have offered above
%the idea that a minor change in the input model might place a property violation in a
%different location in the space of behaviors represented by the model, thereby greatly
%affecting the performance of the verification tool.  Would it be useful to offer a
%\textit{reverse search} option in a model checker, so that property violations on
%the opposite side (conceptually) of the state space would be found quickly?  That is,
%just as apparently minor changes in the input model may greatly affect the performance
%of a particular verification strategy, might apparently minor changes in the search algorithm
%have just as great an affect on performance?

%Our work on random search as an efficient method of detecting errors in formal models,
%implemented in Lurch, raises its own version of some of these general questions about
%verification strategies.  For Lurch runs in which no property violation is detected,
%is there any way to measure coverage, to estimate the size of the space of behaviors
%left unexplored, or to characterize the structure of the state space?  Monitoring a
%random search run for saturation is helpful in knowing when to stop trying to use
%random search to find new behavior in the model, but we have not done experiments
%to try to use saturation-related metrics to estimate the size of the remaining unexplored
%behavior or to predict the performance of other tools.  Because of the unbiased nature
%of a random search, compared to a systematic, deterministic search through a space of
%behaviors, it may be possible to use it to quickly gain approximate information about
%the structure or size of the state space.  With a better understanding of the relationship
%between model structure and alternative verification strategies, information from random
%search might helpful in guiding the use of other tools.
