\section{Introduction}

%%%%% deleted...
% There are a variety of strategies, implemented in various tools, to
% improve the scalability of automated verification tools.
% Some strategies retain the ability to fully verify the input model, while
% other strategies limit the scope of verification to improve
% scalability.  Scope may be limited in various ways.  For example,
% the types of input models or properties that can be verified may be
% restricted; properties proved or errors detected may have to be
% validated manually or with another tool.
%%%%% added...
There are a variety of ways to improve the scalability of automated
verification tools.  Some verification strategies limit the scope of
verification to improve scalability.  For example, the scope may be
limited by restricting the types of input models or properties that
can be verified.  Or the results of verification---properties proved
or errors detected---may have to be validated manually or with another tool.

%%%%% deleted...
% Diverse strategies for improving scalability, implemented
% aggressively in different model checking tools, so that time and
% memory use is decreased as much as possible, tend to make the tools
% complementary to each other.  That is, for a given input model and
% property specification, one verification strategy may be much more
% effective than another, but for a different input model and property
% specification the effectiveness may reverse.
% Also, different strategies emphasize different goals.  One may emphasize speed but
% require much more memory, while another requires less memory but is
% slower; one strategy may provide simpler and more useful information
% for correcting detected errors but may require much more time and
% memory to produce such information.
%%%%% added...
Diverse verification strategies, each attempting to improve scalability
in different ways, tend to be complementary.  In the experiments below,
for example, verification of a given input model may require require
much more or much less time and memory, depending on the model translation
and verification tools used.  In addition, because different translation
tools implelement different scalability-improving assumptions, property
violations present in a model may be missed by one verification strategy
but caught by another.  And even when two different strategies catch the
same property violation, one strategy may be much faster, require much
less memory, or produce simpler and more useful information for correcting
the input model.

Cobleigh et.al.~recognize complementary relationships between
modeling languages, translation and verification tools and recommend the use of a
verification framework in which a variety of strategies are
available, so that, as software models and users' needs change, the
right strategy is available \cite{cobleigh01}.
%%%%% deleted...
% In this article we
% consider the basic verification challenge, to determine whether a
% software model is consistent with a formal specification of
% correctness properties, and argue that the best verification
% strategy is to use \textit{all} or most of the tools, \textit{all}
% of the time.
%%%%% added...
In this article we consider the basic verification challenge, to determine
whether a software model is consistent with a formal specification of
correctness properties, and argue for the use of several verification
strategies---each with its own automatic translation and verification tools---together.

%%%%% deleted...
% Using multiple complementary verification tools on the same input
% model yields two types of advantages.
%%%%% added...
Using multiple complementary translation and verification tools together
on the same input model yields two types of advantages.
%%%%%
First, hidden assumptions and
idiosyncrasies of the tools are brought to light, so that individual
tools may be used more effectively and the user has reason for
increased confidence in the results.  This is especially important
%%%%% deleted...
% when verification tools are used in a framework including elements
%%%%% added...
when tools are used in a verification framework that includes elements
not developed by the user, e.g., automatic translators or modeling
tools, as in the experiments we present below. If automated
verification tools are to be practical and cost-effective, expert
knowledge of the inner workings of a tool must not be a prerequisite
for use.
%%%%% deleted...
% If multiple tools, implementing diverse verification
% algorithms, run on the same input and yield consistent results, the
% user can be more confident in correctness, without knowing a great
% deal about the particular tools.
%%%%% added...
If multiple tools, representing
diverse modeling languages, translation
assumptions, and verification algorithms, can be run on the same input
to produce consistent results, the user can be much more confident in
the results' correctness. 

A second advantage of multiple-tool verification strategies is
improved scalability. Tools may be cascaded in such a way that input
models difficult for one tool are passed on to another.
%%%%% deleted...
% Complementary performance implies that most input models will be
% easy for at least one tool even if difficult for others.
% In addition, cascading multiple tools may result in an overall
% verification strategy much less sensitive, in terms of time and
% memory requirements, to minor changes in the input model.
%%%%% added...
If tools' performance is sufficiently complementary, most imput models
will be easy for at least one tool even if they are difficult for one
or more other tools.  Cascading multiple tools may result in an overall
verification strategy much less sensitive, in terms of time and memory
requirements, to minor changes in the input model \cite{owen07}.

%%%%% there's a shift in content here... (new section needed?)

In previous work we experimented with a simple random search to
detect errors in software models \cite{owen02a}. Our strategy was as
follows: start at the initial state of the model; choose the next
state at random from those possible; quit when no next state is
possible or a user-specified depth limit is reached. Search results
followed a pattern: at first, many unique states were explored, but
soon the number of unique states explored reached a peak and stopped
increasing; from then on the same states were explored over and
over. When allowed to run to this \textit{saturation} point, at
which the proportion of unique states drops off, the random search
produces surprisingly consistent results.  We concluded that random
search, in spite of its general (worst-case) unreliability, was
sufficiently consistent to pursue as an efficient strategy for
detecting errors in software models
\cite{menzies02,owen02c,owen02b}.

Further work on random search led to the development of Lurch, a
tool for detecting violations of generic and user-defined logical
properties in finite-state machine models \cite{owen03a}. We
compared Lurch's performance to the model checkers SPIN
\cite{holzmann03} and Cadence SMV \cite{mcmillan00} and found that
with random search it is often possible to detect property
violations far more quickly and with orders of magnitude less
memory. We also showed how Lurch could be used together with a
conventional verification tool to greatly improve average
verification performance: use Lurch first for a relatively short
time and only run the verification tool on input models for which
Lurch finds no property violations \cite{owen03b}.

%%%%% deleted...
% In addition, random search can be used  to confirm the results of
% model checking.  This might not be expected, since a model checker
% carries out a complete exploration of all the behavior represented
% by the input model---how could a random sample include any
% additional behavior?  However, in real-world applications of model
% checking, assumptions are often made about the structure of the
% input model in order to improve performance.  Random search of an
% input model with fewer or different assumptions can thus be used as
% a \textit{sanity check} on the verification results produced by a
% model checker \cite{owen06}.
%%%%% added...
In addition, random search can be used as a \textit{sanity check} on
verification results produced by a model checker:  to improve
performance in real-world applications of model checking, the input
model may be simplified, based on assumptions about its structure.
If the model checker detects no faults in this simplified model,
random search can be run
on an un-simplified version of the model.  Assuming the random
search also detects no faults, we can be more confident in the
simplifying assumptions used to make the input model small enough
for verification with the model checker \cite{owen06}.

%%%% deleted...
% In this article, we consider complementary  relationships between
% diverse verification strategies, including random search, different
% types of model checking, and a specialized tool for proving
% invariant properties.
% Our primary contribution is to show how a
% variety of verification tools may be used together in a single,
% generally applicable verification strategy based on complementary
% relationships between tools.
%%%%% added...
In the experiments below we consider complementary relationships between
diverse verification strategies including random search, different
types of model checking, and a specialized tool for proving
invariant properties.
We found complementary relationships between these different
strategies, especially between the translation tools used to generate
the different input models needed for each strategy.
Our primary contribution is to show how complementary strategies like
those we considered can be used together in a single robust verification
strategy.
%%%%%
Complementary relationships considered
include both complementary scope---tools performing different
types of analysis---and complementary performance---execution
time and memory consumption.


%%%%% deleted...
% In this paper, we propose and evaluate a multiple-tool verification
% strategy of software specifications written in the Software Cost
% Reduction (SCR) modeling language \cite{heitmeyer05}. In addition we
% argue that, in general, diverse strategies for improving scalability
% of model checking may be integrated to produce a single strategy
% that is both more scalable and more reliable. Improved reliability
% is the result of insight into the use of each tool gained by
% comparing the results from different tools.
%%%%% added...
In this article, we propose and evaluate a multiple-tool verification
strategy for software system and property specifications written in the
Software Cost Reduction (SCR) modeling language \cite{heitmeyer05}.  In
addition, we suggest the following more general claim:
diverse verification strategies, each attempting
to improve scalability in different ways, may be integrated to produce a
single strategy that is both more scalable and more reliable.  Improved
reliability is the result of insight into the use of each tool gained by
comparing results from different tools.

