

\section{Case Study}

%%%%% This paragraph was included in the dissertation but deleted in the draft
%%%%% we submitted.  I'm bringing part of it back since the replacement
%%%%% paragraph below generated complaints from the reviewers.
Section \ref{case-study} outlines the experimental procedure and summarizes general
results from the main case study example presented in this article.
We describe the input model used,
an SCR specification for a personnel access control system (PACS) written
as an example to show how to develop a high quality software
requirements specification.
We then describe our process for automatically generating
a set of fault-seeded versions of the original SCR specification.
Section \ref{experiments} first describes the experimental process carried out
for each fault-seeded specification---the order in which verification tools
were run, the settings and precise way in which each tool was used, and the
data collected.  Finally, we summarize experimental results:  fault-seeded
specifications are divided into subsets based on which tools were able to
detect faults in each specification, and average time and memory requirements
reported for each tool running on each of these subsets.

%%%%% This paragraph caused 3/4 reviewers to complain about missing references,
%%%%% so I'm deleting it for now and using some of the original paragraph
%%%%% above (from my dissertation) to introduce the section.
% When examining the effectiveness of testing techniques, standard
% experimental practice calls for the mutation of the software
% artefact followed by the accounting of mutants captured by the
% technique being evaluated. To the best of our knowledge, such an
% experiment has never been performed in the realm of formal
% verification.  The insights from this experiment will enable us to
% analyze the strengths and weaknesses of different verification
% techniques and develop the most beneficial combined verification
% strategy.

\subsection{PACS SCR Specification}
\label{pacs}

In the three motivating examples and in the experiments below,
we used an SCR specification for a Personnel Access Control System
(PACS) described in a prose requirements document from the National
Security Agency \cite{nsa03}.  These requirements have been used by
others to compare the effectiveness of process-based and
formal-methods-based strategies for developing reliable software
\cite{widmaier00}. The SCR specification was derived from that
document as an example to demonstrate how to write a high quality
formal requirements specification and to evaluate compositional
verification methods \cite{desovski06}.

The PACS checks information on magnetic cards and PIN numbers to limit
physical access to a restricted area to authorized users.  To gain
access, the user swipes an ID card containing their name and
social security number (SSN) through a card reader.  After confirming that the user has the
required access privileges, the system instructs the user to enter a
four-digit personal identification number (PIN).  If the entered PIN
matches a stored PIN in the system database, the PACS allows the user
to enter the restricted area through a gate.  To guide the user
through this process, the PACS includes a single-line display
screen.   A security officer monitors and controls the PACS using a
console with a second single-line display screen, an alarm, a reset
button, and a gate override button.

To initiate the process, the PACS displays the message
\textit{Insert Card} on the user display and, upon detecting a card
swipe, validates the user's name and SSN.  If the card is
valid, the PACS displays \textit{Enter PIN}.  If the card is
unreadable or the information on the card fails to match information
in the database, the PACS displays \textit{Retry} for a maximum of
three tries.  If the user's card is still invalid or there is no
match, the system displays \textit{See Officer} on both the user
display and the officer display and turns on an alarm on the
officer's console. Before system operation can resume, the officer
must push the reset button. The user, who has three tries to enter a
PIN, has a maximum of five seconds to enter each of the four digits
before the PACS displays the \textit{Invalid PIN} message. If three
times either an invalid PIN is entered or the time limit is
exceeded, the system displays \textit{See Officer} on both the user
and the officer display. After receiving a valid PIN, the PACS
unlocks the gate and instructs the user to \textit{Please Proceed}.
After 10 seconds, the system automatically closes the gate and
resets itself for the next user.

\begin{figure*}
\begin{center}
\includegraphics[angle=90,width=6in]{pacs2.pdf}
\caption{PACS mode finite-state machine.}
\label{f:pacs2}
\end{center}
\end{figure*}

Figure \ref{f:pacs2} shows a finite-state machine representing the
core mode logic of the SCR model of the PACS requirements.
%%%%% deleted... (mentioned in added paragraph below)
% The full
% SCR model is available in \cite{owen07}.
Initially, the mode is
\textit{EnterCard}; when a card is entered the mode changes to
\textit{CheckCard}.  If the card is not valid, a limited number of
retries are allowed, during which time the mode alternates between
\textit{CheckCard} and \textit{ReEnterCard}.  If the card is valid,
the mode changes to \textit{EnterPIN}; when a PIN is entered the
mode changes to \textit{CheckPIN}. Similar to \textit{CheckCard},
from \textit{CheckPIN} the user has a limited number of retries if
an invalid PIN is entered, during which time the mode alternates
between \textit{CheckPIN} and \textit{ReEnterPIN}.  If a valid PIN
is entered the mode changes to \textit{Proceed}.  In mode
\textit{Proceed}, the user is able to enter through the gate.  Once
the gate closes the system is reset to \textit{EnterCard}.

In modes \textit{CheckCard} and \textit{CheckPIN}, if the maximum
number of retries is reached after repeated invalid card or PIN
entries, the mode changes to \textit{Error}.  From \textit{Error}
the officer may override the PACS, the mode of which then changes to
\textit{Override}.  The user may then enter through the gate.  When
the gate is closed, the mode changes to \textit{EnterCard}.  Also,
if the system is reset by the officer in any mode (except
\textit{EnterCard}) the mode is reset to \textit{EnterCard}.
%%%%% deleted
% \footnote{Note the dotted line transition in the upper right part of
% figure \ref{f:pacs2}.}

%%%%% added... (there's no explanation of the assertions below)
The SCR specification of the PACS is approximately 200 lines and includes
15 assertions.  To give an idea of the type of properties checked in the
experiments below, one of the assertions is:  the user display shows "Retry"
if and only if the ID card has been read at least
once but fewer than three times.  For the full SCR model, see \cite{owen07}. 

\subsection{Generating Fault-Seeded Versions of the PACS SCR Specification}
\label{seeding}




\begin{figure*}
\begin{center}
\footnotesize
\begin{tabular}{l|l|rll}
Label & Description & \multicolumn{3}{l}{Example} \\ \hline
AOR & Arithmetic Operator Replacement & \texttt{+} & $\rightarrow$ & \texttt{-} \\
CRP & Constant Replacement & \texttt{1} & $\rightarrow$ & \texttt{2} \\
EVR & Enumerated Type Value Replacement & \texttt{a} & $\rightarrow$ & \texttt{b} \\
 & & \multicolumn{3}{l}{\parbox{2.5in}{(where \texttt{a} and \texttt{b} are possible
  values for the enumerated type)}} \\
IOR & Implication Operator Replacement & \texttt{=>} & $\rightarrow$ & \texttt{<=>} \\
LCR & Logical Connector Replacement & \texttt{AND} & $\rightarrow$ & \texttt{OR} \\
ROR & Relational Operator Replacement & \texttt{<} & $\rightarrow$ & \texttt{<=} \\
SND & SCR \textit{Next} Operator Deletion & \texttt{'} & $\rightarrow$ \\
SOR & SCR Event Operator Replacement & \texttt{@T} & $\rightarrow$ & \texttt{@F} \\
UOD & Unary Operator Deletion & \texttt{NOT} & $\rightarrow$ \\
VRP & Variable (same type) Replacement & \texttt{x} & $\rightarrow$ & \texttt{y} \\
 & & \multicolumn{3}{l}{\parbox{2.5in}{(where \texttt{x} and \texttt{y} are variables
  of the same type)}}

\end{tabular}
\normalsize
\caption{Mutation operators used to generate fault-seeded versions of the PACS SCR
  specification.}
\label{t:operators}
\end{center}
\end{figure*}

Figure \ref{t:operators} shows mutation operators used to generate fault-seeded
versions of the PACS SCR specification.  This set of operators is adapted from a
set of five determined to be sufficient by Offutt et.al.~for Fortran programs \cite{offutt96}.
Operators AOR, LCR and ROR are taken directly from that set.  UOD is similar to
the unary operator insertion (UOI) mutation operator included in the set from
Offutt et.al.~but is easier to implement without a full parse of the input
specification.

The set of five sufficient mutation operators from Offutt
et.al.~also includes an absolute value insertion (ABS) operator,
which replaces an entire arithmetic expression with zero, a positive
value, or a negative value.  To avoid fully parsing the input
specification, and because SCR does not assign a logical value to
arithmetic expressions (i.e., SCR does not define \texttt{1} to be
true and \texttt{0} to be false), ABS was not used. Instead we used
CRP (from \cite{offutt96} ~but not one of the five selected) and
EVR, which replace individual integers or, for variables of
enumerated type, other legal values.  IOR and SND are similar to LCR
and UOD, but deal with SCR-specific features.  We developed a
mutation tool which automatically generated 323 mutant SCR
specification models. Due to space limitations we omit details of
the mutant generation algorithm, which are available in \cite{owen07}.

In Andrews et.al.~\cite{andrews06} a similar set of mutation operators,
adapted from Offutt et.al.~to use with C programs, is used to accurately
evaluate test suites; that is, these mutation operators produce fault-seeded
programs realistic enough that a given set of tests will achieve approximately
the same level of program coverage, in terms of widely used coverage criteria,
that the given set of tests would achieve for programs with real faults.
Also, automatic fault seeding with these mutation operators is compared
to manual fault seeding and found to yield results that are actually
\textit{more} realistic.




\subsection{Experiments}
\label{experiments}

%%%%% added (condensed version of paragraph from disseration that we'd deleted)
For each fault-seeded specification, the SCR Toolset was used to run basic
generic checks and generate Salsa, SMV and SPIN versions of the specification.
We then ran Salsa, SMV and SPIN on the appropriate generated input models;
Lurch was run on an input model generated from the SPIN version of the specification.
%Salsa was run on the SCR Toolset's Salsa version of the specification.  SMV
%was run on the SCR Toolset's SMV version, and NuSMV was run on version of the SMV model
%with the minor modifications described in section \ref{utpb527}.  Lurch was run on a model
%generated from the SPIN version of the specification,
%and then SPIN was run three times, each configured differently,
%on the SPIN version of the specification.

In the SCR Toolset, we used the command-line program \textit{testtool}
via scripts to automatically run consistency checks on the
specification to check for syntax and type errors, duplicate names,
unspecified or unused variables, missing or inconsistent initial
values, circular definitions, and violations of disjointness or
coverage properties.
%%%%% deleted (covered in added text above)
% Disjointness violations
% occur when, from a certain state of the system, for a given input,
% the specification allows more than one possible next state.  This
% nondeterminism is considered an error in SCR.  Coverage violations
% occur when, from a certain state of the system, for a given input,
% no next state is specified.
For our verification experiments we used only fault-seeded
specifications for which no errors were detected by
\textit{testtool}. Any specification that failed any of the checks
was removed from the set to be used in the experiments.  Our focus
is on back-end verification tools, so there is no reason to use
%%%%% put some of the text in a footnote here...
models that fail these basic checks.\footnote{In addition to a \textit{pass}
or \textit{fail} result, it is possible to get a \textit{warning}
from the SCR Toolset consistency checker. These \textit{warning}
specifications were not removed from the experiments since in
practice additional back-end verification tools would be used to
determine whether the \textit{warning} result corresponded to a real
error.}
%%%%% deleted (already said this above)
% If the specification passed these checks, the SCR Toolset's
% translators were used to automatically generate Salsa, SMV and SPIN
% versions of the specification.

To create NuSMV versions of the SMV models offered by the SCR Toolset's
translator, we developed a script to substitute \texttt{INVARSPEC}
for \texttt{SPEC} and delete \texttt{AG} from the portion of the SMV
model representing assertions in the original SCR specification.
This was to remove the possibility of inconsistent results
between NuSMV and Cadence SMV, discussed in section \ref{examples}.
To create Lurch versions of the SPIN models output by the SCR
Toolset's translator we created the script mentioned earlier.

Next, we ran Salsa on the fault-seeded specification and compared
the results to those produced from the original, correct
specification. Specifications were divided into five categories
based on the results produced by Salsa:

\begin{enumerate}
\item Those for which Salsa was able to prove \textit{fewer} of the assertions
than could be proved for the original SCR specification (94 specifications).
\item Those for which Salsa could prove \textit{additional} assertions (16).
\item Those for which Salsa's results for the assertions matched results on the original
specification but Salsa proved \textit{fewer} generic properties (36).
\item Those for which results for the assertions matched the original but Salsa
proved \textit{more} generic properties (7).
\item Those for which Salsa's results, for assertions and generic properties,
were identical to results on the Salsa version of the original SCR specification (170).
\end{enumerate}

%(How much should we say about these five sets?  And where should we say it?)
%Time and memory requirements were recorded for
%each salsa run on each specification, although there was little variation
%from one run to another.  Average time required was 1.20 seconds; memory
%required for every run was the same:  1.59 megabytes.
%%

Cadence SMV and NuSMV were next run on the SMV version of each
fault-seeded specification, with NuSMV running on a modified version
with the changes described in section \ref{examples}.  With these
minor changes for compatibility with NuSMV, Cadence SMV and NuSMV
results were always consistent.  Property violations were detected
in 141 specifications; no violations were detected in 182
specifications.  As mentioned above, the SCR Toolset's translator to SMV restricts the
type of assertions to those involving only the current state of the
system.
%%%%% deleted...
% That is, any assertion using the SCR \textit{Next} operator
% (\texttt{'}) or any event operator (\texttt{@T}, \texttt{@F},
% \texttt{@C}) is removed from the SMV version of the specification.
For our experiments this meant that \emph{only 9 of the 15
assertions} in the original SCR specification were checked by
Cadence SMV and NuSMV.  This limitation in the effectiveness of SMV
(both Cadence SMV and NuSMV) running on models generated from SCR
specifications is also beneficial, because it simplifies the input
models and is one possible explanation for the very low time and
memory requirements of Cadence SMV and NuSMV, compared to SPIN
(described below).

Because some assertions possible in an SCR specification are not
included in the SCR Toolset's SMV version of the specification,
Cadence SMV or NuSMV can be used as a preprocessor in cases where no
faults are detected.  Properties proved true by SMV can be removed
from the specification so that later verification tools can be run
on a simpler input model.

Time and memory requirements were recorded for each run of Cadence SMV and NuSMV.
%There was more variation than with Salsa, especially in the amount of memory required
%by NuSMV, but still the amount of variation was very small compared to SPIN
%(described below).
The average time required for Cadence SMV was 0.107 seconds, and for
NuSMV 1.21 seconds; the average memory required for Cadence SMV was
3.48 megabytes, for NuSMV 13.2 megabytes, all with minimal variance.

\begin{figure}
\begin{center}
\small
\begin{tabular}{cc|cc}
\multicolumn{2}{c|}{10 violations in} & \multicolumn{2}{c}{Less than 10 viol-} \\
\multicolumn{2}{c|}{under 50 runs} & \multicolumn{2}{c}{ations in 50 runs} \\ \hline
10 / 10 & (175) & 0 / 50 & (117) \\
10 / 11 & (16) & 1 / 50 & (2) \\
10 / 12 & (5) \\
10 / 13 & (4) \\
10 / 17 & (1) \\
10 / 27 & (1) \\
10 / 38 & (1) \\
10 / 39 & (1)
\end{tabular}
\normalsize
\caption{Lurch results on fault-seeded PACS specifications:  number of
  times violations detected vs.~search runs, number of specifications in parentheses.
%%%%% added... (reviewers seem to have misunderstood the table)
  For example, ``10 / 10 | (175)'' means that, for 175 of the fault-seeded specifications,
  Lurch found violations in 10 of 10 runs on that specification.
%%%%%
  }
\label{t:lurch-runs}
\end{center}
\end{figure}

Next, we ran Lurch on versions of the fault-seeded specifications
generated from SPIN versions of the specifications produced by the
SCR Toolset.  Because Lurch's random search does not necessarily
return consistent results, Lurch was run between 10 and 50 times on
each input model.  Only in cases where Lurch detected a property
violation at least 10 times was Lurch counted as having detected the
violation.  If Lurch found a violation ten times before 50 runs, we
stopped running Lurch on that input model.  As shown in Figure
\ref{t:lurch-runs}, for most input models (292 of 323) Lurch either
detected a property violation ten times in the first ten runs or
detected no violation in 50 runs.  In only a few cases (6 of 206) in
which a violation was detected did Lurch find the violation in less
than 75\% of runs.

For input models in which Lurch detected a property violation at least 10
times, average time and memory requirements for all runs, including those
in which no property violations were detected, were recorded for comparison
with the other tools.  So, for example, if Lurch had to run 20 times to detect
violations in 10 of those runs, all twenty runs were included in average
time and memory values.  Average time required by Lurch for a single input model
(in which violations were detected) ranged from 0.144 seconds to 62.7
seconds; overall average time was 2.72 seconds.  Memory requirements showed
little variation from one model to another, with an overall average of
5.68 megabytes.

Because input models used with Lurch were based on SPIN versions of
the specifications produced by the SCR tools, all assertions in the
original SCR specification (including assertions not included in SMV
versions of the specifications) were checked by Lurch.  This is why
Lurch detected a larger number of property violations than SMV. In
addition, because Lurch input models were derived from the SCR
Toolset's SPIN version of the fault-seeded specifications,
\texttt{NATURE} constraints are ignored by Lurch as well (see
Section \ref{examples}).


Finally, SPIN was run on versions of the fault-seeded specifications produced
by the SCR Toolset's Promela translator, in the following three ways:

\begin{enumerate}
\item First, run SPIN with default settings (default depth limit 10,000).
\item If no violation found, run with settings necessary to get complete
verification runs even on input models for which no violations were detected
(compile with minimized automaton memory compression, run with depth limit 2,000,000).
\item If (still) no violation found, run on input model with final \texttt{d\_step}
marker removed, as described in section \ref{utpb23}, and with settings
necessary for complete verification runs on models for which no violations
were detected (compile with minimized automaton memory compression, run with
depth limit 3,200,000).
\end{enumerate}


With default settings (option 1), SPIN detected property violations
in 205 of 323 input models, averaging 3.41 seconds and 45.9
megabytes per verification run. With settings adjusted to insure a
complete verification run, SPIN was able to detect violations in 26
additional models.  For SPIN run in this way, the average time
required was 561 seconds, and the average memory 488 megabytes.
Section \ref{utpb23} showed that in order to get a fully reliable
verification result running SPIN on an input model translated from
an SCR specification by the SCR tools, it is necessary to remove the
final \texttt{d\_step} marker from the model.  Running SPIN on input
models with this change, with settings adjusted to enable a complete
verification run, SPIN was able to detect property violations in two
more of the models.  The average time required by SPIN run in this
way was 1,340 seconds, and the average memory 475 megabytes.  As
stated above, SPIN's minimized automaton compression option was used
for these runs, which is why they require less memory but far more
time than the second set of SPIN runs.

SPIN requires much more time and memory, in most cases, then the
other tools described above.  But
in our experimental framework
%%%%% added...
(primarily because of the translation tools available)
%%%%%
only SPIN can be used to fully verify all 15 of the assertions in the
original SCR specification.  Based on results from SPIN, we
determined that 90 of the fault-seeded specifications were
equivalent mutants; that is, they specify behavior identical to the
original, as far as the assertions are concerned.  Also, as stated
earlier, SPIN in the context of the SCR Toolset ignores SCR
\texttt{NATURE} constraints, so property violations reported by SPIN
must be validated using Salsa or one of the SMV model checkers, or
manually using the SCR Simulator.


\begin{figure}
\begin{center}
\includegraphics[angle=90,width=3in]{venn.pdf}
\caption{Summary of verification results for all tools except Salsa---sets of fault-seeded
specifications for which each tool detected property violations.}
\label{f:venn}
\end{center}
\end{figure}

Figure \ref{f:venn} summarizes experimental results for all tools
except Salsa, showing sets of specifications in which property
violations were detected by all (122 of 233 non-equivalent mutants);
Lurch and SPIN only (82); Cadence SMV, NuSMV and SPIN only (19);
SPIN only (10); and equivalent mutants (90).  Results for Cadence
SMV and NuSMV are shown together, denoted (Nu)SMV, since these tools
detected property violations in exactly the same set of
specifications.  Results for Salsa are not shown, because, as
explained above, when Salsa fails to prove a property it does not
necessarily mean that the property is violated.  Thus there is no
straightforward way to include the results from Salsa in this kind
of diagram. In section \ref{discussion} we consider how Salsa
results might be integrated with other verification tools in a
useful way.

For the 122 specifications in which all four tools detected a
property  violation, using Cadence SMV (the fastest) vs.~SPIN (the
only tool capable of fully verifying all specifications) saves 345
seconds, or about 6 minutes.  For the set of 82 specifications in
which property violations were detected only by Lurch and SPIN,
running Lurch vs.~SPIN saves 2,463 seconds, or about 41 minutes.
The greatest time benefit is for the set of 19 specifications in
which Cadence SMV, NuSMV and SPIN, but not Lurch, detected property
violations.  For this set running Cadence SMV vs.~SPIN alone saves
12,043 seconds, or about 3.5 hours.  So even though this is a small
number of specifications, they are among the easiest for Cadence SMV
and the most difficult for SPIN (assuming a framework using the
SCR-to-SMV and SCR-to-SPIN translation tools available to us).
Similarly, running Cadence SMV on
these specifications requires far less memory than SPIN.  Section
\ref{discussion} considers these results in more detail, from
various perspectives.
