\section{Introduction}

We need to reduce the cost of formal verification methods.
Formal verification  is often used to improve the
reliability of mission-critical or safety-critical applications
(e.g. see~\cite{holzmann97}). A single formal query such
as "always, the elevator door never opens more than twice between the
source floor and the destination floor" can represent a very large
number of specific tests cases. Running this query once
can find many errors. However, funding the same
errors with   specific test
cases may require many example inputs. Further, model checkers
return {\em counter examples} showing exactly how an invariant is violated.
Such counter examples are useful in localizing and repairing faults.

The benefits of formal verification come at a cost that is often
prohibitively expensive. These costs
including the
{\em writing cost}, the {\em running cost} and the {\em re-writing
cost}.  Scarce and expensive PhD-level
mathematical expertise may be required to {\em write} the formal
 temporal logic\footnote{ Temporal logic
is classical logic  augmented with
 temporal operators such as
 $\square X$ (always $X$ is true),
$\lozenge X$ (eventually $X$ is true), $\bigcirc  X$ ($X$ is true
at the next time point), $X \,{\cal U}\, Y$: ($X$ is true until
$Y$ is true).} expressions  needed for these tools. For example, if $P$ is
the elevator doors opening and $Q$ is the arrival at the source floor
and $R$ arrival at the destination floor, then the following daunting
expression models our rule about the elevator doors:


{\footnotesize
\newcommand{\always}{$\Box$}
\newcommand{\eventually}{$\lozenge$}
\newcommand{\aand}{$\wedge$}
\newcommand{\oor}{$\vee$}
\newcommand{\until}{${\cal U}$}
\newcommand{\nope}{$\neg$}
\newcommand{\so}{$\rightarrow$}
\begin{alltt}
\always((Q \aand \eventually R) \so ((\nope P \aand \nope R)
     \until (R \oor ((P \aand \nope R)
        \until (R \oor ((\nope P \aand \nope R)
           \until (R \oor ((P \aand \nope R)
              \until (R \oor (\nope P \oor R))))))))))
 \end{alltt}}

Once expressed, automatic methods such as the SPIN
model checker~\cite{holzmann97} can
 search an formal representation of a program to find
 counter-examples to the supplied constraint. This search
 explores all the interactions within the program. In the worst case,
 the number of such interactions is exponential on the number of different assignments
 to variables
 in the system.
 Hence,
 the {\em running cost} of this query can be excessive.
This large {\em running cost} often forces analysts to
rewrite and shorten the formal models or formal constraints.
Such a rewrite incurs the {\em rewrite cost}
 and  may ignore some, potentially significant,
system detail.

Much research has tried to reduce these costs. For example,  simplified
modelling environments have been developed such as
SCR~\cite{heitmeyer02,heitmeyer96automated,heitmeyer95} or simple
influence diagrams~\cite{me00q} where users can express
their models  in simple and intuitive
framework.
Models written in these toolkits
can be mapped into model checkers such as SPIN,
thus combining easy model specification with exhaustive formal verification.
In other work
Dwyer,
Avrunin \& Corbett~\cite{dwyer97,dwyer98a} have identified
{\em temporal logic patterns} within the constraints  seen in many real-world
properties models. For each pattern, they have defined an
expansion from the intuitive pseudo-English form of the pattern to
a formal temporal logic formula. In this way, analysts are
shielded from the complexity of formal logics. For example, our {\em writing
cost} for the above expression about the elevator was minimal. We just looked up
the ``bounded existence'' temporal logic pattern
at \url{http://www.cis.ksu.edu/santos/spec-patterns/ltl.html}
and extracted the  expression associated with
{\em transitions to P-states occur at
most 2 times  between Q and R}.

These tools reduce the {\em writing cost}  but don't
necessary reduce the {\em running cost} or the {\em rewriting cost}.
The {\em rewrite cost} is incurred only when the {\em running cost} is too high
and the models or constraints must be abbreviated.
There is no guarantee that
formal verification is tractable over the
constraints and models built quickly using temporal logic patterns and tools like SCR.
Restricted modelling languages {\em may} generate models simple enough to rigorously
formerly verify, but the restrictions on the language can be excessive.
For example, checking temporal properties within simple influence diagrams
can take merely linear time~\cite{me00q}, but such a language can't model common
constructs such  sequences
of actions or recursion.
Hence, analysts may be forced back to using more general formal verification languages.
Unfortunately, as discussed in our related work section,
 the hight {\em running cost} of such general verification languages persists despite
  decades of work.


In an attempt to resolve the {\em running cost} (and hence remove the {\em rewrite cost}),
we have for some years now
been exploring  formal models compiled into
a variant of
and-or graphs called {\em NAYO graphs}~\cite{me00b,me01h,me99q}.
These NAYO graphs have the advantage
that they can be auto-generated from commonly used representations
such as finite state machines, but
don't require the exponential memory of standard model checkers. As we shall see
later on, a complete search of NAYO graphs has a prohibitively high
{\em running cost} (exponential on the size of the graph).

The logical form of a NAYO graph is close to
the  SAT (satisfiability) problem studied at length by the artificial intelligence
community (e.g.~\cite{mack85}).
This community often applies {\em random search} to SAT problems.
When competing constraints
block further progress, a random search tosses a coin (metaphorically)
to favor one constraint over the rest. The random search then continues
and future impasses are resolved using the same random method. This means that a single
random search explores some randomly selected subset of a formal model.
After some time, the random search device resets and starts all over again.
In this new search, another randomly selected subset of the formal model is explored.
After $N$ resets, the best solution seen in any run is returned as the result.

A repeated result from the SAT community
is that random search can solve large satisfiability problems
that defeat complete
search~\cite{kautz96,hoos00,smith96}. This result motivated us to explore
random search over NAYO graphs generated from finite state machines which lead to the
following discovery:
\begin{quote}
{\em Random search over formal models exhibits a  {\em saturation effect}.}
\end{quote}

\begin{figure}
\begin{center}
\begin{picture}(150,140)(-10,-15)
\qbezier(-5,-5)(100,-5)(135,-5)
\put(45,-15){\footnotesize \sffamily Time $\longrightarrow$}
\qbezier(-5,-5)(-5,35)(-5,100)
\put(-15,6){\rotatebox{90}{\footnotesize \sffamily unique errors detected}}
\qbezier(0,0)(10,35)(20,50)
\qbezier(20,50)(100,50)(135,50)
\put(22,52){\footnotesize \sffamily saturation}
%\qbezier(0,0)(5,75)(10,75)
%\qbezier(10,75)(100,75)(135,75)
%\put(12,77){\footnotesize \sffamily Best}
\qbezier(0,0)(50,60)(135,85)
\put(38,28){\footnotesize \sffamily no saturation}
\end{picture}
%\vspace{-5pt}
\caption{The saturation effect.}\label{fig:sateffect}
\end{center}
\end{figure}

The saturation effect is shown in the {\em saturation} curve of \fig{sateffect}.
In that curve,
most of what is discovered is
discovered very early in the process. Saturation usually manifests as a sharp initial
increase in the number of unique errors discovered, followed by a plateau
where extra effort does not yield more unique errors.

Assessment methods with the saturation effect support early stopping
rules. Such rules reduce the cost of testing since additional useless assessment
can be avoided.
Assessment methods that lack the saturation effect have the property that the longer
the assessment, the more unique errors are found: see the {\em no saturation} curve
of \fig{sateffect}.

Assessment methods using early stopping rules run the risk of false positives: i.e. reporting
that no bugs are present when further assessment would have found them.
Early stopping can hence only be endorsed for {\em adequate} and {\em flat plateau} methods:
\bd
\item[Adequate:]
If the assessment method is {\em not adequate} then errors will be missed prior to plateau.
\item[Flat plateau:]
If the saturation curve does not generate a {\em flat plateau} then additional errors
are present and will be missed by early stopping.
\ed

Our claim is that random search of NAYO graphs generated from finite state machines
is both adequate and demonstrates flat plateaus. Hence, early stopping is possible
for finite verification, assuming random search over NAYO graphs. If true, this would
remove the {\em runtime cost} and the need for the {\em rewrite cost}.

The rest of this paper defends this claim. After a discussion on related work, we describe
an environment for translating communication finite-state machines into NAYO graphs.
Experiments with random search over these graphs reveals a saturation effect. Case studies will
be presented showing that our method is  {\em adequate}, and generates {\em flat plateaus}.

\section{Related Work}

\subsection{The Saturation Effect}

Saturation is consistent with programs containing zones
that are easily reachable and zones that are not reachable at all.
Elsewhere,  we have surveyed the numerous reports
of this effect in the software engineering and knowledge engineering
literature~\cite{me99q,me00y}.
This section is a brief sample of those surveys.

Horgan \& Mathur~\cite{horgan96} document systems were most
program paths get exercised early with little further improvement
as testing continues.
Mutation testers often report that a small sample of their
mutations\footnote{A {\em mutant} of a program is a syntactically
valid but randomly selected variation to a program; e.g. swapping
all plus signs to a minus sign.}
find as much as a much larger sample of mutations~\cite{michael97,wong95,budd80,acree80}.


Numerous  researchers report
that much of the apparent complexity of their program collapses into a very small
zone where all program paths traverse.
For example,
Avritzer et.al. \cite{avri96}
found that a sample of 6\% of all  inputs to a telecommunications expert system
covered  99.9\% of all inputs seen  in
one year's operation of that program.
In other work,
Bieman \& Schultz~\cite{bieman92} document a natural language process system where
less than 50 inputs were enough to exercise all the du-pathways\footnote{A du-path is a link
from where a variable is {\em defined} to where it is {\em used}.} in 95\%
of the system modules.
A similar effect was noted by
Harrold et.al. \cite{harrold98} who studied how control-flow diagrams grow as
program size grows.
A worst-case control-flow graph is one where
every program statement links to every other statement; i.e. the edges in
graph grow with the square of the number of statements. However,
for over 4000 Fortran routines and 3147 ``C'' functions, the
control flow graph grows linearly with the number of statements.
That is, at least in the systems seen in the Harrold et.al. study
study, the program pathways
form  single-parent trees.
This collapsing effect has been
called {\em
master-variables} in scheduling~\cite{crawford94}, {\em backbones} in
the satisfiability community~\cite{parkes99lifted,singer00backbone}, and
{\em minimal environments} in truth maintenance systems
ATMS~\cite{deKleer86}.

Saturation is such a widespread effect that it has prompted several mathematical
studies.  Menzies \& Singh concluded that saturation is an property which
should emerge in most programs, in the average case~\cite{me00t}.
Another simulation-based analysis,
reported at ISSRE 2000~\cite{me00b}, made a similar conclusion.

\subsection{Other Stopping Rules for Testing}


Early stopping rules in testing are well studied.
Certification tests using reliability demonstration charts have been
introduced by Musa, Iannino and Okumoto \cite{musa87,musa98}.
A {\em reliability demonstration
chart} is shown in \fig{relChart}.  There are three regions on the
chart: {\em reject}, {\em test} and
{\em accept}.  A failure is plotted to the chart when it
occurs during random testing in which tests are selected
according to the {\em operational profile} (an operational profile is
a statement of what input
values are expected at runtime).  The vertical axis on the chart denotes
the failure number, while the horizontal axis denotes normalized occurrence
time (for example, occurrence time multiplied by the failure intensity
objective).  Depending on where the failure is plotted with respect to
the graph regions, testing is stopped (with the program either accepted
or rejected) or continued.
The number of tests required for reliability certification test in this
technique depends on the position of the lines between reject, continue and
accept regions.

\begin{figure}
\begin{center}
\includegraphics[width=2in]{musa.eps}
\end{center}
\caption{The reliability demonstration chart.}\label{fig:relChart}
\end{figure}


Another method for defining early stopping rules is to use bayesian prior
probabilities. Testing can stop early when new tests make little change to the priors.
Consider the case when failure occurs within a run of (say) 5,000 tests.
Suppose that  failure is detected at test 3,500.
The problem is how many additional tests need to be
executed
successfully following one or more failures,
to be able to certify
requested reliability without debugging.
Littlewood and Wright
\cite{Litt95} proposed one solution, based on bayesian
statistics. At the
start of the certification test, compute $n_1$, the number
of failure
free executions for the certification test to succeed and stop.
This figure might come from the standard sampling-with-replacement
equation\footnote{
After $N$ tests, the odds of see a bug which occurs at frequency $x$
is $y=1-\left((1-x)^N\right)$. Hence, the number of tests required
to be  99\% certain  of seeing that
bug $N=\frac{-4.6}{log(1-x)}$}.
If all $n_1$ executions succeed, stop testing
and
software reliability can be certified at the required
level.
Otherwise, a failure is observed at execution $s_1$ and testing
stops. In the light of evidence of one failure in $s_1$
executions, a
number of further failure free executions, $n_2$, where
$n_2>n_1$,
is determined.
Test executions proceed and either
$n_2$ executions succeed (and
reliability certified), of a failure is
observed on demand $s_1 + s_2$.
In the later case, the testing continues.
Note that if the program does not
have the required reliability, testing
may continue forever.  In a
sense, this technique is similar to
Musa's reliability certification
charts, but the reasoning that leads
to accept or continue testing
decisions is different.
Readers interested in understanding
the details of
this approach are encouraged to read \cite{Litt95,littlewood97,cukic00}.

Despite all this work, our reading of the literature is that we
are the first to discuss early stopping rules for randomized formal verification.

\subsection{Reducing the Runtime Cost in Formal Verification}

Many researchers have explored reducing the {\em runtime cost} of formal verification
 using a variety
of techniques:
\begin{smallitem}
\item
{\em Abstraction or partial
ordering}: use only the part of the space required for a
particular counter-example. Implementations exploiting this
technique can constrain how the space is
traversed~\cite{god97}, or constructed in the first
place~\cite{schnieder98}.

\item
{\em Clustering}: divide the
systems model into  sub-systems which can be reasoned about
separately~\cite{clarke89a}.

\item
{\em Meta-knowledge}: study only succinct
meta-knowledge of the space. One example used an
eigenvector analysis of the long-term properties of the
systems model under study~\cite{ishida89}.

\item
{\em Exploit symmetry}: find properties in some part of
the systems model, then reuse those counter-examples if
ever those parts are found elsewhere in  the systems
model~\cite{clarke93}.

\item
{\em Semantic minimization}: replace
the space with some smaller, equivalent space. For example,
the BANDERA system~\cite{corbet00} reduces both the systems
modeling cost and the execution cost by automatically
extracting (slicing) the minimum portions of a JAVA
program's bytecodes which are relevant to particular
properties models.
\end{smallitem}


While the above techniques have
all been useful in their  test domains,
they may not be universally applicable.
Certain optimizations, such as those of \cite{ishida89},
require expensive pre-processing.
Also,
these methods may rely on
certain combinatorial features of the system
being studied. Exploiting symmetry
is only useful if the system under study is highly
symmetric.
Clustering generally fails for tightly connected models.
Hence, in the general case, it seems that only small models can be tested
using state-space search techniques.
