
\section{Related Work}

%%%%% added...
This section provides a brief overview of the research behind the tools used
in the experiments described later:  symbolic and explicit-state model
checking tools, increasingly powerful testing tools influenced by ideas
from model checking research, and random search as a way to efficiently
detect faults in formal software models.

\subsection{Model Checking}
\label{model-checking}
%%%%% added... (since I deleted the "model checking as testing" section heading below)
\label{mctest}

\textit{Model checking} is probably the most widely used automated
verification technique. Model checking tools carry out an exhaustive
exploration of the behavior represented by an abstract program model
to check for consistency with a specification of desired properties
\cite{huth00}. Model checking has been effective in many domains
including computer hardware design, networking, security and
telecommunications protocols, and automated control systems
\cite{holzmann97,clarke99,cimatti00}. Model checking has been used
in safety critical NASA projects \cite{havelund00,gluck02,holzmann04}.
Microsoft research has developed
a proprietary model checking framework for use on critical
components of Windows \cite{ball01}.

The input to a model checking tool is the specification of a
finite-state concurrent system.  In order to verify that the
properties hold, the model checker must construct a single composite
finite-state machine to represent all possible behaviors of the
individual concurrent machines in the model as they interact with
each other.  In practice this composite finite-state machine may be
very large.  This is the \textit{state-space explosion} referred to
in the literature: if there are many concurrent machines in the
input model, making many transitions in parallel, the number of
global states in the composite machine may grow exponentially,
compared to the number of concurrent machines in the original model
\cite{clarke99}.

Model checking techniques originated in the 1980's.
%At that time the maximum number of states in tractable models was between $10^4$
%and $10^{5}$.
In the early 1990's Clarke and colleagues began using
binary-decision diagrams, or BDDs, to succinctly represent the
global system \cite{clarke99}.
%%%%% deleted...
% This new \textit{symbolic model
% checking} technique made it possible to verify much larger input
% models.
% The best implemention is the Symbolic Model Verifier (SMV),
% available in several versions including Cadence SMV
% \cite{mcmillan00} and NuSMV \cite{cimatti00}, which we use in the
% experiments.
%%%%% added...
This new \textit{symbolic model checking} technique, implemented
in a tool called SMV (the Symbolic Model Verifier), made it possible to
verify much larger input models.  In the experiments described below we
use two popular versions of SMV: Cadence SMV \cite{mcmillan00} and
NuSMV \cite{cimatti00}.

Symbolic model checking works well with models representing
synchronous systems, including integrated circuit designs, which
tend to have many small, symmetrical components. But software
systems are often asynchronous. In an asynchronous system several
things may be going on in parallel with no synchronization point and
different interleavings are possible.  If all possible interleavings
must be checked, the state space required tends to grow very large.

Unlike SMV, the SPIN model checker is designed specifically for
asynchronous software models~\cite{holzmann97}.  To handle models
with many possible interleavings of parallel behaviors, SPIN uses
\textit{partial order reduction}: only interleavings relevant to the
property specification are checked.  That is, if the specified
properties are unaffected by the order of some set of events, only
one possible ordering of those events will be checked
\cite{clarke99,holzmann97}. SPIN has been used to verify a wide range of
algorithms, protocols, and system implementations
\cite{holzmann90,holzmann97,holzmann03}.

%%%%% Patrial -> Partial here
Partial order reduction decreases the number of states that must be
explored to verify the input model. To decrease the amount of memory
required for each state, SPIN offers options for lossless or lossy
compression.  The lossless methods save memory, but tend to require
a lot of time \cite{holzmann03}. For example, in the experiments
presented in Section \ref{utpb23}, without compression SPIN would
have required 6.8 Gb of memory for the verification run (this
statistic is provided by SPIN when used with the compression
option). With compression, the run required only about 270 Mb, but
took 30 minutes on a computer with a 2.5GHz processor.


SPIN's lossy compression options run quickly and scale to large
systems, but sacrifice completeness; that is, there is the
possibility of missing property violations present in the system. In
the current version of SPIN these are the hash compaction and
bitstate hashing options \cite{holzmann03}.  In the past, ``scatter
search,'' an incomplete random search technique that limited which
states were explored rather than limiting the amount of information
stored with each state, was added to SPIN \cite{holzmann87}.
Although this idea was eventually given up, results from that work
suggest that if there is a fault in the model, it is likely to
affect a large portion of the state space. This idea is an important
assumption in our work on random search as a scalable alternative to
model checking \cite{owen02a}.

SMV also implements incomplete but scalable search options. Success
in the development of algorithms for solving satisfiability (SAT)
queries has enabled the development of a symbolic search technique
known as bounded model checking \cite{biere99}. To perform bounded
model checking, a SAT query is used to represent the state space up
to a user-specified depth, and a SAT solving algorithm determines
whether the query is satisfiable, which corresponds to determining
whether the input model is consistent with the property
specification.
%%%%% Reviewers didn't mention this but this criticism of bounded MC was
%%%%% criticized in past rejected papers... (should we do anything about it?)
Bounded model checkers are very effective; nevertheless,
bounded model checking is incomplete and can miss faults because of
the search depth restriction. If no property violation is found, we
only know that there is no violation within the user-specified
search depth.

The use of incomplete techniques is controversial, since the primary
goal of model checking is verification, not debugging. But in
practice, even when complete verification is not possible model
checkers have proven useful.  For example, they can automatically
detect complex errors in systems too large for complete verification
\cite{cobleigh01,groce02}, find counter examples to aid in fixing
known errors \cite{dong03}, and be used to automatically generate
test cases \cite{gargantini99,heimdahl03}.

%%%%% deleted...
% \subsection{Model Checking as Testing}
% \label{mctest}

%%%%% deleted...
% Efficient but incomplete model checking  can serve for the
% development of testing methods.
%%%%% added...
Incomplete strategies that nevertheless provide some of the benefits
of model checking can be thought of as part of a growing set of testing
tools with capability inspired by model checking.
%%%%%
Much work is being done on testing
strategies that are increasingly automated and capable of detecting
more complex types of faults. For example, tools running directly on
source code and large production models can detect classes of faults
previously in the realm of formal verification
\cite{savage97,godefroid97,sims01,groce02}.

%%%%% deleted... (this paragraph doesn't fit here)
% Besides scalability, an important criterion for comparing various
% testing and verification strategies is \textit{scope}: the types of
% faults that can be detected or, for complete verification
% techniques, the types of properties that can be verified.  For
% example, many incomplete techniques scale to large systems but
% cannot detect liveness property violations, which require cycle
% detection \cite{godefroid97,savage97,groce02}.  Even complete
% techniques may use optimizations limiting the scope of properties
% that can be verified; these optimizations must be turned off,
% sacrificing scalability, in order to verify the full range of
% temporal logic properties.

It is difficult to compare techniques' scalability and scope,
because different approaches work well with different types of
models, and some researchers advocate a framework in which several
complementary approaches are available
\cite{corbett96,cobleigh01,groce02}.
%As pointed out by Cobleigh
%et.al. \cite{cobleigh01}, the expectations of users vary through
%different phases of software development, while the scalability of a
%particular tool may depend on what it is being used for.
For example, an explicit-state model checker (SPIN) might quickly
find many long counter examples, while a symbolic model checker
(SMV) might require more time and memory but find much shorter
counter examples \cite{bharadwaj99,cobleigh01}.  So it may depend on
whether a verification practitioner requires, e.g., fault detection
alone versus short counter examples to facilitate debugging. Related
to this is the sensitivity of a testing strategy to minor changes in
a model. 
%%%%% deleted...
% A small change in the input model can make a significant
% difference in the time and memory required to detect faults.
%%%%% added...
For a given testing strategy, a small change in the input can make a
significant difference in the time and memory required to detect a fault.

\subsection{Random Search Applied to Formal Models}
\label{west-random}

Almost twenty years ago West explored the idea of using a simple
incomplete technique, random search, to detect faults in
finite-state models of software systems \cite{west89}. Random
search, although incomplete, was shown to be surprisingly quick and
effective. West's explanation of the success of random search is
helpful in understanding the success of various heuristics and
incomplete verification strategies available today. He noted that
faults detected in concurrent systems are often much less complex
than the overall system \cite{west89}. That is, a fault involving a
small subset of processes is present in many global system
states---processes not relevant to the fault may be in any local
state as long as the relevant processes are in the local states that
together constitute the error.

Faults may also be less complex than the overall system in another
way:  even if the fault is present in a very small number of global
system states, there may be many paths that lead to those states.
This kind of structure is exploited by SPIN's partial order reduction
strategy, which avoids
exploring interleavings of behaviors irrelevant to the properties
being verified.  In models for which partial order reduction is effective we
expect incomplete techniques to perform well also:
where any one of a large number of interleaved paths is sufficient to represent all
relevant behavior, the search only needs to explore one, so an incomplete
search may be sufficient.
