\section{Modeling and Verification Framework}
\label{framework}

This section describes the modeling and verification tools that
together make up the framework for the experiments described in the
next section.  We briefly describe the tools we used: the SCR Toolset, the
Cadence SMV and NuSMV symbolic model checkers, the SPIN
explicit-state model checker, the Salsa invariant checker and Lurch,
our random search debugging tool for formal models.

\subsection{The SCR Toolset}

The SCR requirements specification language, a tabular notation
for concise, unambiguous description of functional requirements,
was developed by Heitmeyer and others over the last twenty years and
has been used in a variety of research and industrial
applications \cite{heitmeyer05}.  An SCR specification includes
both \textit{monitored} variables, which represent environmental
quantities monitored by the system, and \textit{controlled}
variables, which represent quantities controlled by the system.
Monitored variables may change nondeterministically, but behavior
within the system, causing changes to controlled variables,
must be deterministic.
In general, changes in controlled variables
are triggered by \textit{conditioned events} of the form:

\vspace{5pt}
$\mathrm{@T(}c\mathrm{)}\hspace{.4em}\mathrm{WHEN}\hspace{.4em}d
  \hspace{1em}^{\mathrm{def}}_{\textstyle \hspace{.1em}=}
  \hspace{.6em}\neg c \wedge c' \wedge d$
\vspace{5pt}

This event could be read: ``\textit{c} changes from false to true
when \textit{d} is true.''
The @T(\textit{c}) portion of the event
is a two-state predicate and is true if the condition \textit{c} is
false in the current state but true in the next state.  For the
entire event to be true (including WHEN \textit{d}) the condition
\textit{d} must be true in the current state.

During the last 15 years automated tools have been developed to
enable more effective and less costly analysis of SCR
specifications. The current version of the SCR Toolset includes the
following modeling and verification tools:

\begin{enumerate}
\item Specification Editor: Enables user-friendly viewing, editing,
  and search of specifications; also provides access to the other
  tools through a single interface.
\item Simulator: Allows the user to observe and control execution of
  the specification, to follow a path to an error discovered by one
  of the model checking tools, for example.
\item Dependency Graph Browser: Constructs and displays a graph showing
  relationships between variables in the specification.
\item Consistency Checker: Detects various kinds of errors including
  syntax errors, invalid values, circular definitions, and violations
  of disjointness or coverage properties.
%%%%% added...
  (Disjointness is explained
  in the discussion of the second motivating example above; coverage
  violations occur when, from a certain state of the system, for a
  given input, no next state is specified.)
%%%%%
\item Model Checker(s): Automatic translation from SCR to the SMV
  and SPIN model checkers.
\item Theorem Prover: Automatic translation to TAME \cite{archer02},
  a simplified theorem proving tool.
\item Invariant Checker: Automatic translation from SCR to the Salsa
  invariant checker.
\item Invariant Generator: Automatically generates state invariants
  for the specification.
\end{enumerate}

In addition to these tools, we wrote scripts to automatically
translate from an SCR specification to the input language for our
Lurch random search tool.
Through these scripts and the tools
listed above, it is thus possible to automatically
translate from an SCR specification into the input languages of all
five of the testing and verification tools described below.

\subsection{The Cadence SMV and NuSMV Symbolic Model Checkers}

The Cadence SMV \cite{mcmillan00} and NuSMV \cite{cimatti02}
symbolic model checkers are two freely available
versions of SMV, the ``symbolic model verifier''.  The input
languages for Cadence SMV and NuSMV are basically the same.  As
described earlier, however, there are slight differences.
%%%%% deleted...
% Further,
% differences between the SCR modeling language and the SMV language
% are the reason the SCR Toolset's translator to SMV restricts the
% type of assertions to those involving only the current state of the
% system.
%%%%% added...
Further, the SCR Toolset's translator to SMV simplifies the input model
(and improves scalability as a result) by restricting the type of
assertions allowed to only those involving the current state of the
system.
%%%%%
For example, any assertion using the SCR \textit{Next}
(\texttt{'}) operator is removed from the model before translating
to SMV.

\subsection{The SPIN Explicit-State Model Checker}

The SPIN explicit-state model checker is a widely used and freely
available automated verification tool \cite{holzmann03}.
%Unlike
%Cadence SMV and NuSMV, which represent sets of states symbolically
%with BDDs, SPIN represents each global state explicitly in the
%global finite-state machine representing the behavior of the overall
%system.
%As mentioned previously, SPIN uses other techniques to
%control the size of the global finite-state machine and to decrease
%the amount of memory required for each state stored.
Unlike the SCR modeling language, in which state transitions may be
triggered by change events based on the current state and previous
state of the system, in Promela, the SPIN input language, state
transitions are based only on the current state of the system.
Rather than removing such behavior from the SCR model before
translation to Promela (as is done before translation to SMV), the
SCR Toolset's Promela translator makes two copies of every variable
in the specification, one for the previous state and one for the
current state of the system.  Change events (and assertions
involving both the previous and current state) can thus be included
in the Promela version of the specification.
%%%%% deleted...
% This makes
%%%%% added...
The different approach taken by the SCR-to-SPIN translator (compared
to the SCR-to-SMV translator) makes
%%%%%
SPIN's verification result more comprehensive, since the input model is
closer to the original SCR model.  But this also makes the
verification run require much more time and memory, compared to
verification with Cadence SMV or NuSMV.  \footnote{Some performance
differences may also be due to the fact that SCR is a synchronous
modeling language, and SPIN has been designed for asynchronous
models, unlike Cadence SMV and NuSMV, which are designed for
synchronous models.}

\subsection{The Salsa Invariant Checker}

The Salsa invariant checker uses a combination of ideas from theorem
proving and symbolic model checking to prove disjointness and
coverage properties, as well as user-specified assertions, for input
models written in a modified form of the SCR specification language
\cite{bharadwaj00,sims01}.
Like an automated theorem proving tool,
Salsa attempts to carry out an inductive proof using decision procedures.
Like a symbolic model checker, Salsa uses BDDs to represent the
global system in a very compact way.

Salsa either determines that a property is true or outputs a
two-state counterexample.  (This is different from the
counterexample produced by a model checker, which would include all
states along a path from initial conditions to the property
violation.)  In some cases Salsa is unable to prove properties that
are actually true, so the user must determine whether
the two-state
counterexamples produced by Salsa are valid;  that is, whether the
first state in the counter example is reachable from the system's
initial state.

\subsection{The Lurch Random Search Tool}

%%%%% Note:  this paragraph was deleted in the draft we submitted,
%%%%% but I think it's more important than the following paragraph.
%%%%% So I kept this one and deleted the next.
%%%%% added...
Lurch, our random search tool for detecting property violations in
formal models, explores a sample of paths through the global
finite-state machine, choosing randomly when more than one branch
is possible \cite{owen03a}.  Lurch runs until it reaches a property
violation, the end of a path, or a user-specified depth limit.  This
is repeated until a user-specified number of paths has been explored,
or until \textit{saturation} is achieved; that is, if the percentage
of unique global states explored, compared to the total number of
global states explored, drops below a user-specified threshold, the
search is stopped early \cite{menzies02}.

%%%%% deleted...
% Lurch was originally designed to run on asynchronous models.  The
% experiments below use functionality added later to support synchronous,
% hierarchical finite-state models, in which
% the individual machines may each execute a transition at each
% execution step, but within each step machines are ranked in a
% dependency order. This is necessary to support models translated
% from SCR, which is a synchronous, hierarchical modeling language.

Lurch's input language is similar to Promela, the input language for
SPIN, allowing state transitions and assertions to be based only on
the current state of the system.  Because of this our
scripts to translate from SCR to Lurch actually translate from
the SCR Toolset's Promela model, generated for SPIN, to Lurch,
rather than directly from SCR to Lurch \cite{owen06}.  This makes
the Lurch version of an SCR specification larger (like the SPIN
version), but does not have much impact of Lurch's performance,
since Lurch does a limited number of random explorations through the
model.  For a more detailed description of Lurch, the additional
features and the process of translating from SCR to Promela to
Lurch, see \cite{owen07}.
