
\section{Preliminaries}
Our discussion on {\vvai} begins with a general tutorial on {\VV} and
{\AI}.

\subsection{What is {\VV}?}\label{sec:vv}

The standard definitions for {\VV} are based on the work of Barry
Boehm~\cite{boehm81}:
\begin{defs}{\em Verification}: was the system built right?

\end{defs}
\begin{defs}{\em Validation}: was the right system built?
\end{defs}

Validation is usually some assessment of a system according to some
external semantic criteria such as (e.g.) correspondence to system
requirements. Verification usually is some  internal assessment of a
system according to internal syntactic criteria such Practitioners
often find these definitions problematic since activities defined for
verification are often applied to validation and vice versa. For
example: \bi \item Dondossola~\cite{don99} describes a suite of {\VV}
techniques for {\AI} systems. A careful reading of that list shows
many overlaps. For example, {\em formal inspections} to find
differences between the specification and the implementation is
supposedly a {\em verification} technique. Yet if automatic support
is provided to simplify that formal inspection, this becomes a
validation {\em validity proof}. \item {\em Model checking} is an
automatic method for generating counter-examples showing how an model
might violate a set of constraints\cite{clarke86,holzmann97}. Using
model checking to tests for deadlocks can be called an internal
verification check. However, using model checking to test that a
devastating business situation can never occur can be called an
external validation check.  \ei

Since separating verification from validation can be problematic, we
will combine them into one  area with one general goal:
\begin{defs}
{\VV} aims to find {\em anomalies} within software artifacts
\end{defs}

\begin{figure}
\begin{center}
\includegraphics[width=2.5in]{time.eps}
\end{center}
\caption{Models growing with time.}\label{fig:modelstime}
\end{figure}
In this definition, {\em anomalies} are either true errors or ``false
negatives''. False negatives are issues which, after careful review,
prove not to be a problem. Also, the {\em artifacts} of this
definition are any product generated over the entire software life
cycle. As shown in \fig{modelstime}, such artifacts typically grow in
size and detail as the development progress.
\begin{figure}
\begin{center}
\includegraphics[width=3in]{life.eps}
\end{center}
\caption[A standard {\VV} cycle.]{A standard {\VV} cycle. Rectangles
are the inputs and outputs of the functions shown as ellipses.
}\label{fig:vv}
\end{figure}
Regardless  of when the artifact is generated, {\VV} progress is that
of \fig{vv}: \bi \item Based on the knowledge of domain, a summary is
generated from the artifact.  For example, the dependency graph
between terms in a program could be extracted. This summary is in the
format required for the subsequent assessment function and may
contains only the features required for that assessment. \item This
summary is then queried looking for anomalies. For example, the
dependency graph could be examined for loops in the reasoning. \item
The generated anomalies are then checked to find the true errors. \ei






\fig{p1} shows the ratio of anomalies to true errors for real world
{\AI} systems.  Note that a large number of anomalies are not errors.
A good assessment function generates few false negatives. However,
such an assessment can be prohibitively expensive. For example: \bi
\item Model checkers  explores all pathways through a mathematical
description of the implementation looking for violations to global
constraints. Such an exploration can take exponential memory and so
is often only conducted on a very small portion of a total system.
\ei

\lhead{Menzies: \vvai}

 \rhead{\sl
page~\thepage~of~\pageref{LastPage}}\subsection{What is  AI?}


 Consider the  model of \fig{econ0} which summarizes
the causal claims made in a one hour meeting where economists are
discussing influences on the economy\footnote{Note: logic programming
researchers distinguish between {\em theories} written by humans and
the a {\em model} that is automatically generated at runtime by an
inference engine from the theory. Having noted this distinction, this
article will use the less technically correct but common definition
of ``model'': i.e. the thing generated by humans after modelling a
domain.}
 We denote {\tt x=up} as \up{x} and {\tt x=down} as
\down{x}.  In that figure, {\tt
x}~\(\stackrel{++}{\rightarrow}\)~{\tt y} denotes that \up{y} and
\down{y} can be explained by \up{x} and \down{x} respectively; and
{\tt x}~\(\stackrel{--}{\rightarrow}\)~{\tt y} denotes that \up{y}
and \down{y} can be explained by \down{x} and \up{x} respectively.


To make our example interesting, we will suppose that  a {\VV}
analyst is  suspicious that some of these edges in \fig{econ0}
represent unsupported speculations from our economists. Hence, she
views edges in our theories are {\em plausible but optional}
inferences. The utility of using an edge is assessed via its eventual
contribution to world coverage.

How can our {\VV} analyst assess  a collection of subjective
statements like \fig{econ0}? A {\KBS} approach might be to check
their explanatory power;  i.e. model one is better than model two if
model one can explain more observations than model two. To implement
this assessment, we need a {\KBS} that reflects over \fig{econ0} to
see what parts, if any, can reproduce known observations.
\begin{figure}[!t]
\footnotesize
\begin{center}
\begin{tabular}{cp{2.8in}}
\nth{P}{1}:& \down{domesticSales}, \down{companyProfits},\newline
             \down{inflation}\\
\nth{P}{2}:& \up{foreignSales}, \up{publicConfidence},\newline
             \down{inflation}\\
\nth{P}{3}:& \down{domesticSales}, \down{companyProfits},\newline
             \down{corporateSpending}, \up{wagesRestraint}\\
\nth{P}{4}:& \down{domesticSales},     \down{companyProfits},
\newline
             \down{inflation},         \up{wagesRestraint}\\
\nth{P}{5}:& \up{foreignSales},        \up{publicConfidence},
\newline
             \down{inflation},         \up{wagesRestraint}\\
\nth{P}{6}:& \up{foreignSales},        \up{companyProfits},
\newline
             \up{corporateSpending},   \up{investorConfidence}\\
\end{tabular}
\end{center}
\normalsize \caption[Reflections of the model of \protect\fig{econ0}.
]{Reflections of the model of \protect\fig{econ0}. These are the
connections between \myset{\up{investor confidence}, \up{wages
restraint}, \down{inflation}} and  \myset{\up{foreign sales},
\down{domestic sales}} across }\label{fig:proofs}
\end{figure}
\begin{figure}
\begin{center}
\includegraphics[width=3in]{econw1.eps}
\caption[Whatif \#1 is generated from~\fig{econ0}.]{Whatif \#1 is
generated from~\fig{econ0} by combining \nth{P}{2}, \nth{P}{5}, and
\nth{P}{6}. Whatif \#1 assumes \up{company profits} and covers 100\%
of the known \my{OUT}puts.} \label{fig:world1}
\end{center}
\end{figure}
\begin{figure}
\begin{center}
\includegraphics[width=3in]{econw4.eps}
 \caption[Whatif \#2 is generated from~\fig{econ0}.]{Whatif \#2 is generated from~\fig{econ0} by
combining \nth{P}{1}, \nth{P}{2}, \nth{P}{3}, and \nth{P}{4}. Whatif
\#2 assumes \down{company profits} and covers 67\% of the known
\my{OUT}puts.}
 \label{fig:world2}
\end{center}
\end{figure}

Consider  the following set of observations: \bi \item

\my{OUT}= \up{investor confidence}, \up{wages restraint},
\down{inflation} \item \my{IN}= \up{foreign sales} and \down{domestic
sales}. \ei \fig{proofs} shows a reflection over all the what-ifs of
this model and includes  all the pathways that connect \my{OUT}puts
back to \my{IN}puts. These paths may contain {\em controversial
assumptions}; e.g.  if we can't believe that a variable can be both
{\tt up} and {\tt down}, then we can declare the known values for
{\tt company profits} and {\tt corporate spending} to be
controversial. Due to these controversies, we can't believe all the
of paths in \fig{proofs} at the same time since (e.g.) path
\nth{P}{1} and \nth{P}{6} contain controversial assumptions.

While our paths can't be believed all at the same time, they can
still offer an explanation for all our \my{OUT}puts. To see this, we
continue {\KBS} reflection and sort out these paths into the two {\em
what-if} scenarios shown in \fig{world1} and \fig{world2}. Each
scenario contains a {\em maximal} (w.r.t size) {\em consistent}
subset of the paths. Each what-if is internally consistent but
contradicts the other what-if. Note that {\em what-if \#1} can reach
our \my{OUT}puts.

There are certain {\VV} benefits to such an elaborate reflection
process. A standard inference procedure might stop when it finds the
contradiction \up{company profits} and \down{company profits} in
\fig{proofs}. On the other hand, our {\KBS} can continue reflection
since it can manage multiple {\em what-ifs}. Such reflection is a
useful {\VV} aid since it can give out analyst clues on how to {\em
repair} a model. For example, in this case, our analyst might explore
the relative strengths of {\tt foreign sales} and {\tt domestic
sales} on {\tt company profits}. If it could be shown that foreign
sales dominates over domestic sales, then what-if \#2 would not be
generated and the this model would always cover the known
\my{OUT}puts.

The cost of this kind of reflection is that the generation of
multiple what-ifs from a model introduces nondeterminacy. For
example, consider \fig{world1} and \fig{world2}: it is not
determinate if we believe in increased or decreased profits and
spending.

\subsubsection{AI Execution = Reflection}



\subsubsection{Examples}

This section samples some of the more common variants on
MATCH-SELECT-ACT  scheme.

\begin{defs} {\em Rule-based expert systems:} The {\KB} is a set
of rules of the form
\[\mbox{if CONDITION then ACTION}\]
\end{defs}
If rule-based expert systems, MATCH finds all the satisfied
CONDITIONs and ACT fires the SELECTed rule's
ACTION~\cite{brownston92,buch84a,rosen93}.
\begin{defs}
 {\em Abduction:} Abduction finds the assumptions that lead
to desired goals, without generating contradictions.
\end{defs}
Abductive MATCH generates multiple what-if scenarios  and SELECT
returns the what-ifs that satisfy some preference criteria. For
example, \fig{econ0} MATCHed to two what-ifs and SELECT returned
what-if \#1 in \fig{world1} using a SELECT of the following form:
return the what-if(s) that contain the greatest number of
\my{OUT}puts we wanted to
explain~\cite{fecosm89b,me97a,me96b,kakas98,by91}.
\begin{defs}
{\em Diagnosis systems:} Diagnosis is a special case of abduction
where the selected {\em what-if} explains the most number of
observations~\cite{hamscher90}.
\end{defs}
Optionally, diagnosis might demand that the explanation uses the {\em
minimum number of inputs}.  For example, in {\em single-fault
diagnosis}, the assumption is that a single faulty device can explain
all the abnormal observations.
\begin{defs}
{\em Planning systems:} The {\KBS} reflects over the set of available
{\em operators} to generate a {\em plan}; i.e. a sequence of
operations that link initial conditions to a goal
state~\cite{allen90}.
\end{defs}

Planning systems might SELECT between different what-ifs using a
preference criteria that favors faster or simpler plans, or plans
that avoid components with a track record of faulty operation. For
example, consider an {\AI} planning robot manipulating objects in a
room containing a table holding up   two objects\footnote{This
example is adapted from~\cite{kendall01}}.  argument's sake, we will
say that we want to move the table and the objects to another room.
Before we can move the table we need to move the two objects. Our
robot can access a set of {\em operators} that can change state in a
room. Before action, our robot pauses to consider what operators they
might apply to the room. That is, they MATCH and SELECT before they
ACT. Each operator has {\em preconditions} describing when that
operator is applicable and {\em postconditions} that describe the
effects of the operator:

\begin{center}
{\scriptsize
  \begin{tabular}{c|p{0.9in}|p{0.9in}}
Operator &Preconditions &Postconditions\\\hline PUSH(obj,loc)&
At(robot,obj) AND Clear(obj) AND ArmEmpty &At(obj,loc) AND
At(robot,loc)\\\hline CARRY(obj,loc)& At(robot,obj)  &At(obj,loc) AND
At(robot,loc)\\\hline WALK(loc) &None &At(robot,loc)\\\hline
PICKUP(obj) &At(robot,obj) &Holding(obj)\\\hline PUTDOWN(obj)&
Holding(obj)& NOT Holding(obj)\\\hline PLACE(obj1,obj2)
&At(robot,obj2) AND Holding(obj2) & On(obj1,obj2)\\
\end{tabular}}\end{center}

At runtime, our {\AI} system must build a {\em sequence} of operators
which take us from some initial {\em start state} (i.e. objects on
table) to some {\em goal state} (i.e. objects on table in another
room). These operators might be too low-level for our human
programmers, so we could define a language that maps higher-level
constructs into these operators. A sample of such macros are shown
below:


\begin{center}
{\scriptsize  \begin{tabular}{r|c|c|c|c|c|c}
\multicolumn{1}{c}{}&\multicolumn{6}{c}{Operators used for each
macro}\\\cline{2-7}
 macro& push& carry
&walk &pickup& putdown &place\\\hline Move object &\XX
&\XX&&&&\\\hline Move robot && &\XX&&&\\\hline Clear object &&&&
\XX&&\\\hline Object on object &&&&&& \XX\\\hline Get arm
empty   &&&&&  \XX &\XX\\\hline Hold an object &&&  & \XX &\\
\end{tabular}}\end{center}

Our robot might shock our {\VV} analyst due to its nondeterminacy and
adaptability: \bd \item[{\em Adaptability:}] The above above planning
system is very suited to machine learning algorithms. {\em
Explanation-based generalization} systems convert repeated sequences
of operators~\cite{mitchell86} into shorter sequences; i.e. this
learning approach find short-cuts in the operator sequences. Note
that our V\&V analyst might be shocked by a system under-going
explanation-based generalization since old behavior may not repeat in
the current version of the software. \item[{\em Nondeterminacy:}]
Note in the above table that MATCH might find two alternate methods
for {\em moving an object} and {\em be holding an object}. This means
that our {\AI} system may be free to select at runtime between
alternate operators. If no other information is available, then
SELECT might choose one operator at random. Note that our {\VV}
analyst might be shocked by a system using nondeterminism since the
choices made nondeterministically at runtime could result in
different behaviors resulting from the same inputs.
 \ed

%XXX families of operators

\section{{\vvai}: What Won't Work}

From the proceeding section, we can see that nondeterminism and
adaptivity are clearly problematic for {\VV}. What certification can
we possibly offer for a piece of software that will change its
structure after we are finished testing it and that will generate
different outputs from the same outputs? Surely, it could be argued,
we should just forbid the use nondeterminism and adaption. This
section rejects this argument. Adaptation and nondeterminism are
issues that can't be  deferred or avoided.

\subsection{Adaptivity = Unavoidable}

Opponents of adaptive software   might argue that after an initial
analysis period, adaptation could be disabled because there is
nothing more to learn. While this may be true in some domains, it is
not true in all domains.
\begin{figure}
\begin{center}
{\footnotesize
\begin{tabular}{|c|c|c|}\cline{2-3}
\multicolumn{1}{c}{}& \multicolumn{2}{|c|}{Changes in the learnt
tree's\ldots}\\\hline
 domain &{\ldots}  size  &\ldots
classification error\\\hline
demon&0.97&0.51\\

wave&1.91&0.95\\

diff&1.46&0.69\\ othello&1.68&0.8\\ heart&1.61&0.65\\
sleep&1.73&0.91\\ hyper&1.74&0.83\\ hypo&1.45&0.85\\
binding&1.51&0.82\\ replace&1.38&0.8\\ euthy&1.33&0.61\\\hline
mean&1.52&0.77\\\hline
\end{tabular}
}
\end{center}
\caption[Impact of learning a decision tree from $N$ or $2N$
examples.]{Impact of learning a decision tree from $N$ or $2N$
examples. From \protect\cite{catlett91}. }\label{fig:catlett}
\end{figure}
For example, Catlett~\cite{catlett91} gave a machine learner N or 2N
examples from different domains. He found that you should never
disable adaptation since, in nearly all cases, more experience lead
to much better and bigger theories with fewer errors (see
\fig{catlett}).

Adaptation is too powerful a tool to disable. Adaption in runtime
software lets a device adapt to changing conditions. For example,
suppose: \bi \item
 A planning
robot moves from a house where objects have the same weight to a
house where objects have different weight. \item After a few days,
our robot notices that that {\em carrying} heavy objects results in
more wear and tear that {\em pushing} heavy objects. \item It would
sensible to let our robot adapt its operators with the extensions
shown here in italics: \ei

{\scriptsize \begin{center}
\begin{tabular}{c|p{2in}} Operator &New
preconditions\\\hline PUSH(obj,loc)=& At(robot,obj) AND Clear(obj)
AND ArmEmpty AND {\em light(obj)}\\\hline CARRY(obj,loc)=&
At(robot,obj) AND {\em light(obj)}
\\\
\end{tabular}\end{center}}

The above example is a simple case of a more general process. {\AI}
systems can be {\em fielded before they are fully finished}. That is,
even before the particulars of a domain are understood, we can
release an adaptive. Given some general knowledge about a domain, an
adaptive system can acquire data at runtime, then specialize itself
to its domain.
\begin{figure}
\begin{center}
\includegraphics[width=1.5in]{cirt.eps}
\end{center}
\caption{A circuit.}\label{fig:cirt}
\end{figure}
To illustrate this specialization process, suppose: \bi \item
 An adaptive robot has limited number of sensors that
can be moved around the robot's body according to current performance
problems of the robot's hardware. \item The illumination circuit of
the robot is shown in \fig{cirt}. This circuit  is used to light up
some area where the robot is working. Our robot needs to ensure that
at least two of the three bulbs in \fig{cirt} are operational and
needs to do so using the minimum number of sensors. \item The robot
can change the bulbs and switched in the circuit, according to what
spare parts are available. Hence, the exact voltages and amperages of
the bulbs and switches in \fig{cirt} are unknown. The best we can is
an incomplete {\em qualitative description} of the circuit, shown in
\fig{qual}. \ei
\begin{figure}[!t]
\begin{tabular}{|p{3.2in}|}\hline
\footnotesize Qualitative numbers replaces all numerics $x$ with a
qualitative number $x'$ as follows:
\begin{eqnarray}
x'\;=\;+& if & x > 0\nonumber\\
x'\;=\;0&if & x = 0\nonumber\\
x'\;=\;-&if& x < 0\nonumber
\end{eqnarray}
The {\tt sum} relation describes  qualitative addition.  For example,
{\tt sum(+,+,+)} says that the addition of two positive values is a
positive value. Some qualitative additions are undefined. For example
{\tt sum(+,-,Any)} says that we cannot be sure what happens when we
add a positive and a negative number.
\begin{alltt}
%sum(X,Y,Z).
sum(+,+,+). sum(+,0,+).   sum(0,+,+). sum(0,0,0). sum(0,-,-).
sum(-,0,-). sum(-,-,-). sum(+,-,Any). sum(-,+,Any).
\end{alltt}
The {\tt bulb} relation describes our qualitative knowledge of bulb
behavior. For example, {\tt bulb(blown,dark,Any,0)} says that a blown
bulb is dark, has zero current across it, and can have any voltage at
all.
\begin{alltt}
%blub(Mode, Light,Volts,Amps)
bulb(blown, dark,  Any, 0). bulb(ok,    light, +,   +). bulb(ok,
light, -,   -). bulb(ok,    dark,  0,   0).
\end{alltt}
The {\tt switch} relation describes our qualitative knowledge of
electrical switches. For example {\tt switch(on,0,Any)} says that
that if a switch is on, there is zero voltage drop across it while
any current can flow throw it.
\begin{alltt}
%switch(State,Volts,Amps)
switch(on,    0,    Any). switch(off,   Any,  0).
\end{alltt}
The {\tt circuit} relation of \fig{cirt} describes our qualitative
knowledge of the circuit. This relation just records what we know of
circuits wired together in series and in parallel. For example, {\tt
Switch3} and {\tt Bulb3} are wired in parallel. Hence, the voltage
drop across these components must be the same (see line 2).
\begin{alltt}
circuit(Sw1,Sw2,Sw3,B1,B2,B3,L1,L2,L3) :-
    VSw3 = VB3,              %  2
    sum(VSw1, VB1, V1),      %  3
    sum(V1,VB3,+),           %  4
    sum(VSw2,VB2,VB3),       %  5
    switch(Sw1,VSw1,C1),     %  6
    bulb(B1,L1,VB1,C1),      %  7
    switch(Sw2,VSw2,C2),     %  8
    bulb(B2,L2,VB2,C2),      %  9
    switch(Sw3,VSw3,CSw3),   % 10
    bulb(B3,L3,VB3,CB3),     % 11
    sum(CSw3,CB3,C3),        % 12
    sum(C2,C3,C1).           % 13
\end{alltt}\\\hline
\end{tabular}
\caption[A qualitative circuit description.]{A qualitative circuit
description. Adapted from~\protect\cite{bratko89}.}\label{fig:qual}
\end{figure}


\begin{figure}
\begin{alltt}\scriptsize
example(circuit(
     Sw1,Sw2,Sw3,B1,B2,B3,L1,L2,L3)) :-
   classification(B1,B2,B3,Class),
   format('~a,~a,~a,~a,~a,~a,~a~n',
          [Sw1,Sw2,Sw3,L1,L2,L3,Class]).

%classification(B1, B2, B3,Class)
classification( ok, ok, B3,   good):- !. classification( ok, B2, ok,
good):- !. classification( B1, ok, ok,   good):- !. classification(
B1, B2, B3,   bad).
\end{alltt}

\begin{center}
\includegraphics[width=1.5in]{circ0.eps}
\end{center}
\caption[A decision tree from by C4.5]{A decision tree from by C4.5
learnt from data generated by backtracking over the output of the
{\tt circuit/7} relation of \fig{qual}.}\label{fig:learnt}
\end{figure}

\fig{learnt} shows what can be learnt from our incomplete knowledge.
The small Prolog program shown in \fig{learnt} generates over 700
solutions to the constraints shown in the {\tt circuit} description
of \fig{qual}. Each solution is ``good'' if
 if two out of the tree bulbs
are {\tt ok} and ``bad'' otherwise (see the {\tt classification}
relation of \fig{learnt}). A machine learner (C4.5~\cite{quinlan92})
can take these examples and learn the decision tree of \fig{learnt}.
According to our learner, to an accuracy of 85.2\%, we can detect
when two of our three bulbs are blown by just watching {\tt Bulb1}.

Based on this learning strategy, we can now define a minimal
monitoring policy:
 monitor only {\tt Bulb1} and ignore the other 6
electrical components in the circuit. Note that once the designer has
specified \fig{cirt}, the rest of the learning is automatic and could
be repeated at runtime by the robot if ever new information comes to
light.

This is a toy example. A more realistic example of this process is
the satellite diagnosis system learnt by Pearce~\cite{pearce88}. In
that study, a 36KB Prolog qualitative model was built of the
electrical circuitry in a European Space Agency satellite. This was
exhaustively simulated and summarized using a machine learner. The
learnt  knowledge was a diagnosis device and was assessed by
comparing it to a manually constructed diagnostic expert system
constructed by a separate team. Note that: \bi \item The manual
system took nearly twice as long to build as the  learnt system.
\item The manually constructed knowledge base contained more
syntactic errors (e.g. type errors and dead-end rules) than the
automatically learnt knowledge base. \item When compared to a FORTRAN
simulator of the circuitry, the manually constructed knowledge base
could reproduce less of simulator's behavior than the automatically
learnt system. \ei

Examples like the above strongly suggest that automatic adaptation of
software may be too useful a tool to be disabled in all cases.


\subsection{Nondeterminism = Unavoidable}


\section{Verification of AI Systems}

Having defined AI systems and discussed some of their benefits and
drawbacks, this paper now turns to specific techniques that can be
applied to \vvai. This section offers some general principles for the
assessment of the syntactic structure of  AI systems.




\section{Software Engineering Techniques for \vvai}

For several decades now, conventional software engineering (SE) has
faced the challenge of assessing complex nondeterministic software.
Examples of such software include programs with concurrent threads
such as certain JAVA programs.

In response to this challenge, the


Recent work on autonomous satellites has prompted NASA scientists to
build AI into their systems. A primary focus at NASA is mission
safety and so once a system is built, it must be tested. Several
techniques have been proposed for V\&V\&AI including {\em
model-checking}, {\em runtime verification}, and {\em static
analysis}. These  techniques have been defined in various places as
verification or validation techniques\footnote{For example, {\em
model checking} has been called validation at
\url{http://ase.arc.nasa.gov/vv2000/asilomar-report.html} and
verification at
\url{http://www.sei.cmu.edu/publications/documents/98.reports/98tr013/98tr013abstract.html}}.
Regardless of how they are categorized, we see below that much
research has been devoted to these techniques. While this research is
clearly the bleeding edge in automatic V\&V, as we shall see, it does
not address the entire  V\&V\&AI problem.


%XXX martins, lots of partial models

\subsection{Model Checking}\label{tion:mc}

Model checking is a method invented by Edward Clarke in the 1980s to
test asynchronous protocols~\cite{clarke86}. Model checking requires
the construction of two models:\be \item The {\em systems model}
which is some abstract description of the essential characteristics
of a program. \item The {\em properties model} which is a set of
constraints that should hold across the systems model. \ee

The properties model is expressed as a formal mathematical
 constraint such as:
 \begin{quote}
{\em Always, the elevator door never opens more than twice between
the source floor and the destination floor.} \end{quote} A model
checker running this query tries to search all pathways through the
systems model looking for ways to violate the properties. If
successful, the model checker return {\em counter examples} showing
exactly how an invariant is violated. Such counter examples are
useful in localizing and repairing faults.

The benefits of model checking 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 of the properties model\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}{$\square$}
\newcommand{\eventually}{$\lozenge$}
\newcommand{\aand}{$\wedge$}
\newcommand{\oor}{$\vee$}
\newcommand{\until}{${\cal U}$}
\newcommand{\nope}{$\neg$}
\newcommand{\so}{$\rightarrow$}
\begin{minipage}{1\linewidth}
\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}
 \end{minipage}}

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.

The model-based nature of AI systems   can significantly reduce the
initial writing cost of the systems model. Automatic tools can
usually be quickly written to convert the AI model into the format
required for a model checker. However, the writing cost of the
properties model remains, as does the running and rewrite cost.

Much research has tried to reduce these costs. For example: \bi \item
 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. \item
 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}. \item The writing
cost of the systems model can disappear to zero if that model can be
auto-extracted from the source code. For example, the BANDERA system
extracts systems models from JAVA source code via a consideration of
the JAVA virtual machine~\cite{corbet00}. \ei

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 model checking 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 explored with model checking-like approaches, 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 model checking languages.
Unfortunately, despite decades of work (see \fig{mlno}),
 the high {\em running cost} of such general model checking
 persists.

\begin{figure}
\begin{center}
{\small \begin{tabular}{|p{3in}|}\hline Each of the following
techniques has proven to be useful in reducing the runtime cost of
model checking or variations on model checking. However,
\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,clancy97}.  \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 internal memory requirements of a model checker can be reduced if
the state space is compacted using binary decision
diagrams~\cite{bryant92}. Another system of interest is the BANDERA
system~\cite{corbet00} that reduces both the systems modelling 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 assessed using model
checking techniques.\\\hline
\end{tabular}}
\end{center}
\caption[Experiments in reducing the state-space explosion
problem]{Experiments in reducing the state-space explosion problem in
model checking.}\label{fig:mlno} \end{figure}



\subsection{Runtime Verification}

\subsection{Static Analysis}

\begin{figure}[!t]
\begin{center}
\includegraphics[width=3in]{codesurger.eps}
\end{center}
\caption[Slicing in Grammatech's CodeSurfer tool]{Slicing in
Grammatech's CodeSurfer tool (see
\protect\url{http://www.grammatech.com/products/codesurfer/example.html}).}\label{fig:codes}
\end{figure}

\section{Discussion}
As we have seen above, there has been much research conducted into
V\&V\&AI. This work does do not solve the V\&V\&AI problem since, the
following problems remain outstanding: \bi \item V\&V of AI {\em
reflection mechanisms}. \item The high {\em writing, running}, and
{\em rewriting} costs  of model checking; \item The {\em coverage
problem} of static analysis and random search. \ei


Next, TAR2 was applied to see what was the {\em second-most}
influential factor. To do this, TAR2 was configured to ignore all
treatments that included configuration information. After 10-way
cross validation, it was observed that the second-best treatment was
\[specstaff=0 \wedge detcap4 \ge 0.365653\] where {\em specstaff} are
the number of staff allocated to the inspections of the functional
specifications; and {\em detcap4} was the defect detection capability
of the code inspections. Given this treatment, TAR2 predicted the
distribution of utility values seen as the {\em second-best} plot of
\fig{utils}. Note that it significantly improves on the baseline, but
does not perform as well as the {\em best} plot.

 The recommendation of
{\em specstaff=0} can be read as a synonym for the above best
recommendation.


 We regard it as a
strength of our $modelling+validation+simulation+sensitivity$
approach that our conclusions are specialized to a certain project.
However, this strength could also view this as a problem. Opponents
of this work might argue that our conclusions are mere quirks arising
from particular projects executing within particular models tuned to
the particulars of certain software organizations. We would agree:
our specific results relate only to the case studies shown above.

So what is the external validity of this research? As stressed above,
we are not proposing new truisms to replace old truisms. Instead, we
offer two results. Firstly, general truisms did not apply in
particular situations. It was not hard to find those situations. In
fact, the counter-examples to the truisms shown above were found in
the {\em very first case studies} we explored.


Using $modelling+validation+simulation+sensitivity$, it was possible
to find other factors that significantly out-performed the factors
recommended by the truisms. That is,   when truisms failed, we could
offer alternate advise to management.

Based on this work, what are we saying about the role of truisms in
software engineering? For ourselves, we have become very skeptical of
their value.


\subsection{Belief Networks: an Alternative to DUMB Reasoning}

A belief network (BN) is a directed acyclic graph whose nodes
represent random variables~\cite{poole98}. The parents of   node $n$
are the nodes on which $n$ directly depends. Each random variable has
a domain and a set of conditional probability tables for every
variable given its parents (including priors for nodes with no
parents). BNs have also been called been called {\em probabilistic
networks, probabilistic belief networks, probabilistic causal
networks}, and - with certain extra constraints on node types- {\em
influence diagrams}).

BN
 update algorithms can shift the probability mass within
the BN in order to better match known observations. The adjusted
priors for a node can be interpreted as the probability that a node
has a certain value, given the observations. For a more details,
see~\cite{poole98}. For a public-domain version of such a BN update
algorithm, see
\url{http://www.cs.ubc.ca/spider/poole/ci/code/apc/bnet.pl}.

The benefit of BNs is that they can simplify our preferred method of
decision making; i.e. $modelling + validation + simulation +
sensitivity$. The process described above to update the prior
probabilities in a BN can be viewed as alternatively: \bi \item
 A {\em simulation
method} since beliefs are moved around the BN in response to
observations; \item A {\em validation method} since faulty BNs can be
tuned to better match observations. \item A {\em sensitivity
mechanism}. If the ``observations'' presented to the BN are desired
goals, then the updated priors can be read as goals to be pursued in
order to reach those goals. \ei

The cost of BNs is that models in other formats have to be rewritten
as BNs. Sometimes, this is not desirable. For example, this paper was
simple to write since it  {\em reused}, rather than {\em rewrote}
existing models of\ldots \bi\item Software effort; i.e. the COCOMO-II
model~\cite{chulani99}; \item Software processes; i.e. the Raffo
discrete event simulation of a software company~\cite{raffo95}. \item
Software project management concerns; i.e. the Madachy
model~\cite{madachy97}. \ei Hence, for cost reasons, this research
strives to be agnostic about the model representation language. Our
preferred framework is to {\em augment}, not {replace} current
methods. Hence, we let analysts develop a model in using their
preferred language, then apply a general sensitivity analysis to the
inputs and outputs of that model.


\subsection{Truisms of Software Defect Detection}
Fenton \& Neil review simple input-output models of factors effecting
software process~\cite{fenton99,fenton00}.  Their opinion of such
models is scathing:
\begin{quote}
Suppose you know that a large number of defects are found in a
software module prior to release. Is it likely that this module will
reveal many defects post-release? A ``yes'' answer here is no more
reasonable than a ``yes'' answer for a person likely to eat a large
dinner after a large lunch. ~\cite{fenton00}.
\end{quote}
Fenton \& Neil note that it is widely believed that  pre-release
fault densities are predictors of   post-release failure rates; i.e.
\begin{equation}\label{eq:one} delivered\; defects \propto
defects\;detected\;in\;testing  \end{equation}
 However, their empirical evidence is exactly the opposite.
For the systems described in~\cite{fenton96}, software modules that
were highly fault-prone prior to release revealed very few faults
after release (and vice versa).

\begin{figure}[!t]
\begin{center}
\includegraphics[width=3in]{bbn.eps}
\end{center}
\caption[Factors effecting defects  in  software]{Factors effecting
defects seen in running software.
From~\protect\cite{fenton00}.}\label{fig:bbn}
\end{figure}

Fenton \& Neil prefer models like \fig{bbn} to simplistic models like
\eq{one}. \fig{bbn} contains a richer internal structure and can
cover more behavior than \eq{one}. For example, given low {\em
defects detected} and high {\em operational defects}, we could infer
that the {\em testing effort} might have been sub-standard. Further,
in~\cite{fenton99}, they show that models like \fig{bbn} can easily
explain certain phenomena in the literature such as the Goldilocks''s
effect\footnote{There is an optimum module size that is ``not too big
nor too small''.} without recourse to certain ad hoc assumptions made
by other researchers in the field.




While we endorse the general theme of the Fenton \& Neil's research
that model-based reasoning is insightful to the software engineering
process, we differ on two points. Firstly, they critique Boehm's work
on the COCOMO-II software cost estimation project, saying that
\begin{equation}\label{eq:two} development\;
effort=function(KSLOC)
\end{equation}
is just as simplistic and just as limiting as \eq{one}. However, even
a cursory    reading of the COCOMO-II literature
(e.g.~\cite{cocomoII}) quickly shows that
 \eq{two} is a gross over-simplification of COCOMO-II models.
In fact, many of the factors appearing in Fenton \& Neil's preferred
models (as described in \cite{fenton00}) include at least some of the
issues modelled  in COCOMO-II. The case study described in Section~3
uses COCOMO-II models since we have far more confidence in them than
Fenton \& Neil.

In contrast, our approach is not {\em tool-focused} but {\em
project-focused}. Sometimes, a tool-focused analysis may miss
important details of a particular project. Tool recommendations that
make sense in the general case may be incorrect for specific cases.

This paper is our case for project-focused assessment of methods to
improve software project quality. Since there is more historical data
on manual SE than automatic SE, our study will focus on optimizing
manual SE methods.

It could be argued that the tool-vs-project distinction is a false
dichotomy.

Thirdly, our practitioner might apply SE truisms (established wisdom
in the field) to make an appropriate tool selection. Many such
truisms exist such as: \be \item Faults densities seen during testing
are predictors for post-release failure
densities~\cite{dunsmore88}.\ee


Fenton \& Neil~\cite{fenton99,fenton00} offer a scathing critique of
the first truism. This truism, they argue, come from simplistic
two-variable regression and ignore important causal factors. This
paper rejects the generality of truism \#2 and \#3. Simulations over
the space of options within models of software processes show that
these truisms can offer misleading advice. While truisms \#2 and \#3
may be important factors when considered in isolation, in certain
projects other factors have a far greater impact than (e.g.) changing
early lifecycle fault detection rates or increasing software process
level.


\subsection{Testing}
The following section describes an assessment method called {\em
model checking}. To demonstrate that model checking is {\em not} a
test method. distinguished from software testing as follows.
\begin{defs}
{\em Testing} is the process where an engineer carefully selects
system inputs, runs the program, then assesses the output.
\end{defs}
\begin{defs} A {\em success test} is one that {\em covers} the static
features of a program. \end{defs} \begin{defs} {\em Coverage} of a
program can be defined in various ways from the very simple (e.g.
program statement coverage) to the very complex (e.g. coverage of
pathways between where variables are set and where they are used in
program conditions. \end{defs}

Testing is a mostly manual process, though some automatic assistance
is available for generating and handling suites of test cases
(e.g.~\cite{avri95,smith00}).


Note the {\em look before you leap} nature of an AI system. Having
determined what  {\em could} be done, we apply SELECT knowledge to
determine what {\em should} be done. Unlike an AI system, a
conventional system can run like Olympic sprinters: they have no
doubts, no hesitation. Given some initial conditions they race to
their termination. However, lacking SELECT knowledge, their successes
and failures are predetermined during their initial design. They
can't reflect as they run  so may trip and stumble over the first
bump in the road.

Continuing with the example of the Olympic sprinter, our AI system is
like a race of nervous accountants. After running a few steps, these
accountants might pause to reflect on (e.g.) what percent of the
runners must currently be within (e.g.) 10ms of the start conditions.
After some shuffling backwards and forwards, our accountants might
start running again, only to stop after another 10ms to reconsider
their position. After a few such pauses for reflection, they might
decide that no one can win this race unless they split the runners
into two groups and run two different races.

A {\VV} analyst checking this {\AI} system might be very surprised to
see that half the accountants freeze near the start while the others
 run to completion. This analyst might complain to his
co-workers ``look at this crazy {\AI} program- see the strange
behavior it generates?''. But there is method in this madness since
this so-called craziness  may still might be better than a
conventional system. For example, the conventional program running
over the same problem might get stuck halfway down the track and
never finish anything at all.





For example, a procedural program could layout a window by placing
characters in several places, then calling the window manager to
pop-up that the window.

 Problems with {\em declarative
representations} have knowledge in a format that may be manipulated,
decomposed and analyzed by the reasoning engine independent of its
content. Analysts could write an XML description of the content of a
window. This XML then be automatically rendered to generate the same
window contents as with the procedural ``C'' implementation discussed
above.

\begin{minipage}{\linewidth}
{\scriptsize
\begin{alltt}
<section>
    <type>
        "warning"
    </type>
    <contents>
        <heading>
            "Summary"
        </heading>
        <textblock>
            "oil pressure low"
        </textblock>
        <heading>
            "Details"
        </heading>
        <textblock>
            "pressure reduction noted during
            the overnight park period"
        </textblock>
    </content>
</section>
\end{alltt}}
\end{minipage}


 Procedural systems are difficult to understand du A
brittle system is one where small changes to a situation can result
in massive change or, worse still, decay of that systems performance.
Consider  a MATCH-SELECT-ACT cycle that finds two MATCHes: one of
which is very preferred and the other of which is highly undesirable.
Such a system is {\em brittle} if the pre-conditions for those
MATCHes are very similar; i.e. a small change in the pre-conditions
can result in the SELECTion of highly undesirable behavior.


What are the essential differences between conventional software and
{\AI} software? A key difference is that they are {\em model-based
systems}:
\begin{defs}
{\em Model-based systems}  store knowledge about individual
components within a domain.
\end{defs}
A model of any particular composite can be "assembled" by the system,
as required from lower-level models. This allows a far greater number
of systems to be represented than if they were all explicitly stored.
The opposite of model-based reasoning is {\em shallow knowledge}
consisting of a long list of special cases describing a system. For
example, an expert electrician's shallow knowledge of an electrical
circuit might include numerous statements like ``if the third bulb is
dark, check that bulb two has not blown''. Note that all these
shallow knowledge statements might be derivable from a more succinct
model-based representations; i.e.  (i)~bulbs two and three are wired
in series; (ii)~the properties of electrical devices linked in series
are well known.

\begin{figure}[!t]
\begin{center}
\includegraphics[width=2in]{m.eps}
\end{center}
\caption{Model-based methods are a superset of knowledge-based
methods.}\label{fig:mkb}
\end{figure}Model-based methods are a general area that include high-level
descriptions of circuit design~\cite{jenn94} and the formal analysis
of concurrent procedural programs~\cite{holzmann97}. Knowledge-based
systems are a special kind of model-based systems:
\begin{defs}A {\em \KBS} builds and
reflect over a model generated at runtime. \end{defs} Outputs are
generated when a explicit knowledge representation called the {\KB}
reflects over the inputs; e.g.
\begin{eqnarray}\nonumber
models=inference(KB,in)\\\label{eq:one} out=reflect(models)
\end{eqnarray}


One interesting feature of TAR2-style learning, are the
attributes never seen in the learnt controllers. In the
golf example, of the four known attributes, one of them
{\em outlook} was deemed worthy of manipulation. For
example, in the {\em COCOMO2} application described in
\fig{models}, XXX

Formally,
 TAR2 treatment learner is best
 described as a {\em weighted-class
minimal contrast-set association rule learner} that uses
{\em confidence measures} but not {\em support-based
pruning} (these terms are defined below).

Standard  classifiers  (e.g. C4.5~\cite{quinlan92} or
CART~\cite{breiman84}) learn connections between $items$
and a classification.  These learners  input a set of
examples containing a set of items $I_i$ of the form
$attribute=value$.  Each example is classified into one and
only one class. The runtime task of a  classifier is to
find an conjunction of items that lead to a certain class.
To find this range, the learner picks one attribute range
that split the set of examples $D$ into subsets $D_1, D_2,
...$. A split is ``good'' if, for each subset $Di$, there
is an increased percentage frequency of one class (compared
to the original set $D$) . The learner then recurses into
each subset to find sub-splits. Various heuristic measures
are used to find the splitting criteria: C4.5 uses an
measure inspired by information theory. The final decision
tree is a report of the tree of recursively-generated
splitting criteria. Each branch of such a tree can be read
as a rule:
\[
Attr_1=range_1 \wedge Attr_2=range_2  \wedge ...
\Rightarrow class=X
\]
where $range$ can be a single value or some numeric
comparison such as $> number$.

Classifiers have a small number of pre-defined targets (the
classes) while,  for {\em association rule learners}, the
target of the learning is not pre-specified. Systems like
APRIORI~\cite{agrawal94} return associations between items
of the form
\[
Rule_r\;:\;X \Rightarrow Y
\]
where $X \subset I$ and $Y \subset I$ and $X \cap Y =
\emptyset$.  In the terminology of APRIORI, $Rule_r$ has
{\em support} $s$ if $s\%$ of the $D$ contains $X \cup Y$;
i.e.
\[support(rule_r)=\frac{|X \cup Y| }{|D|}\] The {\em
confidence} of $rule_r$ is the percent of transactions
containing $X$ which also contain $Y$; i.e.
\[confidence(rule_r)=\frac{|X \cap Y|}{|X|}\]
Many association rule learners use {\em support-based
pruning} i.e. when searching for rules with high
confidence, sets of items $I_i,... I_k$ are only be
examined only if all its subsets are above some minimum
support value.

A common restriction with   classifiers is that they assume
all of $D$ can fit into RAM. Most association rule learners
remove that restriction and are designed for data sets that
need not reside in main memory (exception:~\cite{webb00}).
For example, Agrawal and Srikant report experiments
association rule learning using data sets of size 843MB and
$|D|=10,000,000$~\cite{agrawal94}.

Many variants of APRIORI have been proposed. The CBA
learner finds {class association rules}; i.e. association
rules where the conclusion is restricted to the
classification class attribute~\cite{liu98}. That is, CBA
acts like a classifier, but can process larger datasets
that (e.g.) C4.5.

Another variant are the learners that reject APRIORI-style
support-based pruning. In the case of many
 highly confident rules,   learners such as the
 Wang-He-Cheung~\cite{wang00} system ignore support-based pruning to
  find
  features that apply to a small, but interesting subset
  of $D$.

  Other researchers have
  explored
  {\em weighted association rule learning} in which
     some items are given a higher priority weighting that
     others.   Learners such as MINWAL~\cite{cai98} can use
     such
      weights to focus the learning  onto issues that are of
     particular interest
     to some audience.
     MINWAL can't use APRIORI-style support-based pruning since, with
  weighted items, it is not always true that subsets of
  {\em interesting} items (i.e. where the weights are high) are also
  interesting.

{\em Contrast set} learners such as STUCCO return a
different kind of rule. Instead of finding rules that
describe the current situation, STUCCO finds rules that
differ meaningfully in their distribution across groups.
For example, in STUCCO, an analyst could ask "what are the
differences between people with Ph.D. and bachelor
degrees?"~\cite{bay99}.





 This research makes the {\em small rule assumption}; i.e.
 controlling actions are very expensive to
 perform and monitor variables are very costly to observe. This assumption
 holds in many domains,
 including our test domain of  software independent verification and
 validation (IV\&V). IV\&V analysts collect data from projects and
 make recommendations to improve those projects. Such analysts want
 to trouble the projects the least; i.e. request minimal monitors and
 make minimal controller
 recommendations.   Hence, the size of the conjunctions in the
 rules should be minimized. Also, the total number of rules should
 also be minimal. Generating more than one
monitoring rule is not recommended: data collection in the
real world can be very expensive. Further, generating more
than one action rule can be superfluous.  At any point in
time, an agents can only commit to a single set of
conjunctions. Exploring  disjunctions of actions is only
possible if our agents  are time travellers and can
backtrack in time to explore alternative actions  (a
situation we have yet to see in our  work).

\begin{figure}
{\footnotesize
\begin{tabular}{|r@{~}p{2.4in}|}\hline
attribute:& definition\\\hline
CRIM:      &per capita crime rate by town\\
ZN:      &proportion of residential land zoned for lots over 25,000 sq.ft.\\
INDUS:      &proportion of non-retail business acres per town\\
CHAS:      &Charles River dummy variable (= 1 if tract bounds river; 0 otherwise)\\

AGE:     &proportion of owner-occupied units built prior to 1940\\
DIS:     &weighted distances to five Boston employment centers\\
RAD:     &index of accessibility to radial highways\\
TAX:    &full-value property-tax rate per \$10,000\\
B:    &$1000(Bk - 0.63)^2$ where $Bk$ is the proportion of blacks by town\\
\end{tabular}}
\caption{Attributes in the HOUSING data set from UC Irvine.
All attributes are continuous.
\protect\url{ftp://ftp.ics.uci.edu/pub/machine-learning-databases/housing/}}\label{fig:houseattr}
\end{figure}
