\section{Introduction}

\ifelse{{\sc Clarissa}\ (``Consistent Logical Automated Reasoning for Integrated
System Software Assurance'') is a project led by Honeywell within the
DARPA ARCOS Program.  Its other members are Adelard PLC, SRI
International, and UT Dallas; its purpose is to develop improved
methods and tools for assurance of critical systems.}{}

Assurance is the process of collecting evidence about a system and its
environment and developing claims and an argument that use these to
justify (or reject) deployment of the system; an \emph{assurance case}
is a way of organizing and presenting this information, together with
other relevant facts, knowledge, models, and theories in a manner that
facilitates overall comprehension and assessment.  The purpose of such
a case is to support the socio-technical process of making,
justifying, and communicating the decision to deploy a system or
service in a given context.  In particular, we propose that
evaluation of an assurance case should conclude with an explicit
``sentencing statement'': that is, a description of the evaluators'
understanding of the system and its issues, their assessment of the
case, and their decision on deployment of the system.

Assurance cases have evolved and changed over the past 30 or more
years (see \cite[Chapter 2]{Rushby-etal:NASACases15} for a brief
history); we advocate a further step in their development that we call
Assurance 2.0 \cite{Bloomfield&Rushby:Assurance2} whose slogan, which
might seem paradoxical at first, is ``simplicity through rigor.''  In
keeping with this, our fundamental requirement is that a case should
provide \emph{indefeasible justification} for the decision to deploy
the system or service concerned; this means that the justification
must be so well supported, and all reasonable doubts and objections
must have been so thoroughly considered and countered, that we are
confident no credible doubts remain that could change the decision.
(See \cite{Rushby:Shonan16} for an introduction to the epistemological
notion of indefeasibility in the context of assurance.)

The world is uncertain and our understanding imperfect, so this
assessment is very demanding.  Thus it is often necessary to examine and
evaluate an assurance case from several diverse perspectives that are
combined to yield an overall assessment of its indefeasibility.  For
example, some perspectives will focus on ``positive'' aspects of the
case, such as the evidence and argument in support of its claims,
while others will consider the ``negative'' aspects (i.e., its
potential defeasibility), such as doubts and objections that have been
considered and refuted, and any that remain as residual risks.

Notice that we may wish to perform some assessments and measures
differently during construction of a case than at its end, when the
case will be used in the judgment whether to deploy the system.
During construction, we may wish to evaluate the part of the case we
have constructed and ignore the parts that are missing (or assume they
are good), whereas the existence of missing parts would be
catastrophic in a final evaluation.  Similarly we may tolerate
uninvestigated doubts during construction but will want them resolved
for final evaluation.  Figure \ref{process} illustrates a possible
process for assessment of the perspective we call ``soundness'' at
various stages of development and review.  Other perspectives will
follow similar processes, and these may be interleaved with each
other.

This report is about different perspectives on the assessment of an
Assurance 2.0 case and the different measures that can support and
quantify those perspectives.  \ifelse{We also outline capabilities
required of tools that can manage and assist these activities and
describe those of the prototype {\sc Clarissa}\ tool, which is based on
Adelard's {\sc ASCE} \cite{ASCE}.}{We
also outline capabilities required of tools that can manage and assist
these activities; in particular we are part of a project led by
Honeywell that is developing prototype tool support for Assurance 2.0
(based on Adelard's {\sc ASCE} tool \cite{ASCE}) that we call {\sc Clarissa}\
(``Consistent Logical Automated Reasoning for Integrated System
Software Assurance'').}  These capabilities were explored and
developed during construction of the {\sc Clarissa/asce}\ prototype.  As stated
earlier, we expect evaluation of an Assurance 2.0 case to conclude
with a ``sentencing statement'' (see Section \ref{sentencing}).  This
is a description by the evaluators' of their understanding and
assessment of the case and their decision on deployment of the system.
The assessments and measures described here will be used in support of
the sentencing statement.


  

Before we proceed to describe these assessments and measures, we need
to outline some ways in which an Assurance 2.0 case may differ from
traditional interpretations of assurance cases as described, for
example, in the tutorial by Holloway \cite{Holloway:5parts}.

\ifelse{Assurance cases in {\sc Clarissa}\ follow the approach presented as
Assurance 2.0 \cite{Bloomfield&Rushby:Assurance2}, which}{Assurance
2.0 cases follow an approach that} builds on the earlier ``Claims,
Arguments, Evidence'' or CAE \cite{ASCAD}, where the main component of
an assurance case is a \emph{structured argument} represented as a
tree of \emph{claims} linked by \emph{argument steps}, and grounded on
\emph{evidence}.  As we will explain in Section \ref{structure},
argument steps in \ifelse{{\sc Clarissa}}{Assurance 2.0}\ are restricted to just five basic forms and
these are subject to strong conditions that permit a rigorous, logical
interpretation of the overall case.  We contend that these
restrictions simplify construction of an assurance case by reducing
the ``bewilderment of choice'' and clarifying what must be achieved.

Another way in which we simplify construction and evaluation of
assurance cases is by limiting the content and therefore the size of
their arguments.  Traditionally, assurance cases were largely
identified with their structured argument, but we maintain that many
parts of the case are best presented outside the argument.  We concur
with the traditional view that the purpose of an assurance case is to
collect and integrate evidence and knowledge of the diverse topics
that contribute to assurance of a complex system.  But much of the
knowledge pre-exists and the contribution of the case is to select it,
not develop it.  Similarly, evidence may be distilled from data or
produced by specialized analyses (e.g., formal verification) and
applied to specific representations of the system.  These should be
constructed as theories, models, and ``evidential assemblies'' that
use their own established methods of validation and presentation, and
are referenced and integrated by the assurance argument, not developed
within it.  For example, the argument may have a subcase concerning
hazard analysis and will cite evidence discharging side-claims that
this was performed by a competent team using accepted practice, and
will use the list of hazards found, but it will not itself present the
details of hazard analysis.

Anything that can be considered a single topic, with its own methods,
knowledge, notations and documentation is a candidate for an external
theory, model, or evidential assembly.  These are external to the
argument but part of the larger assurance case: the role of the
argument is to gather and integrate them.  The assurance
case argument will include justification that these external elements
were selected or developed and applied appropriately, but will not
include the internal details or justifications for these elements as
part of the argument itself, although it will provide links to them.
In justifying and reviewing the overall case, it is important that the
assurance argument is consistent with this wider body of knowledge and
evidence, and the ability to conduct deep dives into it is part of the
evaluative probing of the case.  The following sections develop these
ideas in a little more detail.

\subsection{Models and Theories in Support of an Assurance Case}
\label{theories}

We noted above that an assurance case will reference models and
theories in addition to evidence.  It is essential to understand the
relationships of these to each other, and how they are used in an
assurance case.  At the bottom of an assurance case, we have evidence
about the system in its operating context (henceforth we will speak of
simply the system and take this to include its context): that is say,
concrete observations, measurements, and analyses about the system in
operation or under test or about its design and construction.  This
evidence is used to justify logical claims about the system.  The
claims are relative to various descriptions of the system: for
example, if we say ``the tests show the system performs correctly'' we
must have a notion of ``correct'' that is described somewhere.  These
descriptions concern the behavior or attributes of the system from
some point of view (e.g., timing, power consumption, functional
behavior) and at some level of abstraction; we refer to all these as
\emph{models}.

\label{substitution}


The properties that can directly be stated and observed about the
system and its low-level models (e.g., percentage of objects correctly
identified by a vision system under test) will generally be far
removed from the properties about which we seek assurance: those will
generally concern emergent properties stated about highly abstract
models (e.g., safety of an autonomous car).  It follows that a central
task of an assurance case is to connect properties of the system and
its low level models to those of high level models, and this is
accomplished by argument steps that iterate through a series of
intermediate models that generally align with steps in the design and
development of the system, as in the classical ``V'' Diagram.  A
typical step of this kind will seek to justify that a property $A$ of
some model $P$ ensures property $B$ of a next higher model $Q$\@.  In
Assurance 2.0 \ifelse{and {\sc Clarissa}}{} this is precisely the purpose of a
\emph{substitution block}, one of the five kinds of step that may
appear in an assurance case argument.  The justification may be fairly
large, intricate, and possibly mathematical: it is what we call a
\emph{theory}.  The theory may depend on the models $P, Q$ or
properties $A, B$ satisfying some constraints, and these will appear
in the argument as side-claims on the substitution and must be
justified by their own arguments and evidence.  Notice that this
evidence may concern the model (e.g., is it ``well formed'') and not
the actual system.

An example theory is that underlying Modified Condition/Decision
Coverage (MC/DC) for requirements-based tests
\cite{Chilenski&Miller:mcdc,Chilenski&Miller94:mcdc,Hayhurst-etal01}:
such a theory must explain this method of testing and coverage
evaluation, how is it performed, why is it useful, what issues need to
be considered, and what claims it can support.  The theory could then
be used, for example, to explain how MC/DC coverage of executable code
can justify a claim that the code contains no unintended functions.
When using a theory, the argument must provide justification that it
is suitable and credible, and that it is applied appropriately but it
does not present the theory as part of the argument: it merely
references it.



We do this to control the size of the argument, and to allow
compositional reasoning.  The purpose of the structured argument in an
assurance case is to collect, organize, and present evidence and
information relevant to assurance of the system.  This is already a
formidable task and an assurance case argument is therefore generally
large and difficult to comprehend in its entirety.  This task should
not be further complicated by presenting and justifying technical
means of assurance or analysis within the argument.  Such analyses are
better developed, analyzed, justified, and evaluated separately as
self-contained models and theories managed by experts and presented
and assessed by the scientific and engineering methods traditional to
their fields.  These theories may conclude with suggested fragments
for the structured argument of an assurance case referencing the
theory, but those argument fragments emerge as part of the theory
rather than vice versa.

Theories and models are part of the assurance case and must be
assessed as such, but they are developed separately and not within
the argument.  The argument of an assurance case will integrate
subcases that use several different theories but, because the theories
are referenced rather than developed therein, the argument can be
fairly systematic: at each point, we choose a suitable kind of
argument step (see the ``helping hand'' in Figure \ref{helping-hand})
and the theory or other ``warrant'' that will justify it; these
determine the evidence or subclaims required, and any necessary
side-claims.



An example due to Holloway \cite{Holloway:5parts}, illustrates these
points by taking a contrary course (Holloway was using the example for
illustration, not advocating its method).  The example concerns a
teenager Jon who asks his dad if his friend Tim may drive him to the
game.  The dad would like to see an assurance case to justify the
claim that Tim is a safe driver.  In Holloway's presentation, four
topics are identified (and later elaborated) and provide the main
substructure of the argument for the case:
\begin{enumerate}
\item Tim has satisfied all legal requirements for driving.

\item Tim has not been in an accident.

\item Tim has a reputation for driving safely.

\item Nothing is going on in Tim's life that might cause him to drive
less safely than usual.
\end{enumerate}

These seem reasonable, but doubts remain: are they the most important
topics, and are they sufficient?  Surely we would like to see some
extended discussion of driving safety by young men, together with
historical data, statistics, and risk factors.  Holloway does provide
some of this but it is represented explicitly in the argument of the
case and would overwhelm it if included in full detail.  Furthermore,
we cannot expect the developers and evaluators of an assurance cases
to be experts in every topic that might be relevant to a case: for
example, this case is about driving safety, whereas another might
concern the safety of plans for radiation therapy, while yet another
is about mission risk due to pyrotechnic bolts in a spacecraft.

Instead, we advocate that such material is developed as a separate
theory; here this would be an extended ``theory of driving safety by
young men'' that is constructed and evaluated by those with specialist
knowledge of the topic.  The assurance case argument references this
theory, and is structured accordingly, but the theory is not developed
within the argument.\footnote{An alternative point of view is that
these topics are the hazards posed by young male drivers and should
emerge as part of hazard analysis.  Hazard analysis is a form of
evidence assembly (see Section \ref{assembly}), so in this approach
the topics would be delivered to the argument by an evidence
incorporation step rather than a substitution step, but the principle
remains the same: evidence assembly (and hazard analysis in
particular) is an important part of the assurance case, but it is
external to the argument, just like a theory.}

Typically, the theory will justify a substitution step in which
property $A$ of model $P$ ensures property $B$ of model $Q$; most
often, either the properties or the models are the same (i.e., either
$A=B$ or $P=Q$).  Here $P$ and $Q$ are the same ``model'' of young
men's driving, and $A$ is a collection of observable or measurable
properties of young men whose conjunction supports the claimed
property $B$ that such men are safe drivers.  It might well be that
the observable properties identified by the theory are the same four
identified by Holloway, but the structure and justification of the
assurance case will be different.  In Holloway's case, a detailed
justification for the four properties must be embedded in the
argument, whereas the alternative case justifies them by reference to
the theory, supported by side-claims attesting to the credibility of
the theory (authors, reviewers, accepted practice, previous
applications etc.) and its application to the system under
consideration.  The theory is independent of the case and is developed
and evaluated by experts and may evolve over time, whereas the
embedded justification is developed and evaluated as part of the case
by persons who presumably must also consider other topics requiring
specialized expertise such as the safety of Tim's car, and any hazards
of the route to be taken---topics that we would recommend as
additional candidates for external theories or evidence.











\subsection{Evidence and its Assembly}
\label{assembly}

An assurance case is based on evidence, and evidence can take many
forms.  For example, DO-178C \cite{DO178C} identifies 71
``objectives,'' which roughly correspond to evidentially supported
claims in an assurance case retrofitted to DO-178C\@.  Some of the
evidence supporting these claims we call \emph{monolithic} because it
is a single judgment or observation: for example, ``software load
control is established'' \cite[Section 7.1.h]{DO178C}.  Others, we
call \emph{aggregated} because they comprise judgments or
observations iterated over some set of items: for example ``test
coverage of high level requirements is achieved'' \cite[Section
6.4.4.a]{DO178C}, which iterates over the high level requirements to
deliver aggregated evidence that coverage is achieved.  In fact,
monolithic evidence often proves to be aggregated on closer
inspection.  For example, ``software load control is established,''
mentioned above, is defined as follows \cite[Section 7.1.h]{DO178C}.
\begin{quote}
``Software load control ensures that the Executable Object Code and
Parameter Data Item Files, if any, are loaded into the system or
equipment with appropriate safeguards.''
\end{quote}
This suggests that the evidence should reference a theory explaining
what load control means and what safeguards are required and how these
are achieved, and an aggregated evaluation of its application iterated
over each file that supplies ``Executable Object Code'' or ``Parameter
Data Items.''
We therefore take aggregated evidence as the standard case.

Within a structured argument, the purpose of evidence is to support a
claim; without this association, we do not have evidence, merely data.
In \ifelse{{\sc Clarissa}}{Assurance 2.0}, this association is performed by the \emph{evidence
incorporation} block of a structured argument, but it must be
justified by some process or theory that links the evidence to the claim.
Furthermore, there must be some activity that performs the
observations or judgments that provide the underlying data and, if
necessary, aggregates it into evidence.  In addition, evidence must
generally be bound together with other information about its
generation and provenance.  We refer to this entire collection of
tasks as \emph{evidence assembly}; currently this is seldom recognized
as a coherent activity and its tasks are distributed somewhat
arbitrarily between the assurance case argument and its supporting
data collection and this can have unfortunate consequences.


Consider, for example, what happens when one or a few items of
aggregated evidence are changed (for example, some tests are rerun).
Conceptually, evidence assembly updates its aggregated results and
makes these available to the argument of the assurance case.  We must
then consider where is evidence assembly performed?  The natural
location, based on the preceding description, is that it is external
to the tool that manages the assurance case argument.  But an
alternative design, which seems to be assumed in some discussions of
tools for assurance cases, is that it is part of that tool.  Both
approaches seem viable, and one could also imagine mixed forms, where
some kinds of aggregated evidence are assembled locally, by the
argument management tool, and others are assembled externally.

These choices may influence the structure of the assurance case that
is developed.  If evidence assembly is performed in the argument
management tool, then the tool potentially has access to unaggregated
or ``fine-grained'' evidence (e.g., individual test results) and
developers of the assurance case may choose to structure some part of
the argument at this level of detail.  We do not favor this option, as
some assessments of aggregated evidence (e.g., ``does every
requirement have a test?'') may move from evidence assembly, where we
believe it belongs, into the assurance case argument itself.  As we
have noted before, assurance case arguments can easily become
overwhelmingly large and complex and correspondingly difficult to
evaluate; we therefore suggest that it is important to identify
components of the case that can be delegated to separate analysis and
review: this includes models of the system and its artifacts, theories
concerning both design (e.g., fault tolerance) and review (e.g.,
various kinds of testing), and the aggregation and assessment of
evidence.

Observations and judgments may be the central focus of evidence, but
they do not stand alone.  Several other items that we refer to
generically as ``provenance'' are usually needed as well.  For
example, test results might be the primary evidence provided by some
activity, but we also need information on the test oracle, the test
suite, the method of test generation and measurement of coverage, the
execution or experimental platform employed, and the versions of the
requirements and software employed.  It is possible that some of these
could be supplied as separate items of evidence, but the advantage of
supplying it all in a single package is that it can be reviewed and
assessed as part of evidence assembly, and then bound together (e.g.,
with a cryptographic checksum) so that its integrity and coherence are
established and preserved.  Evidence assembly must manage all these
concerns, which will differ across different kinds of evidence, and

for this reason we favor an architecture where evidence assembly is
performed by tools that are specific to the kind of evidence concerned
and that are  external to, but closely allied with,
the tool that manages the assurance case argument.










\ifelse{
\subsection{Structure of an Assurance Case in C{\smaller LARISSA}}
}{
\subsection{Structure of an Assurance 2.0 Case}
}



\label{structure}

Following the discussion of the previous subsections, we see that an
assurance case argument is but part of a ``full'' assurance case that
also includes supporting models and theories, together with evidence
assembly and its underlying data.   A tool that supports assurance
cases does not need to manage the development and assessment of
models, theories, nor the data underlying evidence, but it does need
to be able to reference these\ifelse{ (e.g., {\sc Clarissa}\ can link to
spreadsheets and into text documents)}{}.  And it is a design choice
whether it manages evidence assembly or delegates this to external
tools but, however it is done, evidence assembly is separate from the
assurance case argument, whose management is the prime function of the
assurance case tool.

Assurance case arguments are typically presented graphically, as a
tree-like structure composed of \emph{nodes} and \emph{links} (see
Figure \ref{busy}).  \ifelse{{\sc Clarissa}}{Assurance 2.0}\ follows this approach and the {\sc Clarissa/asce}\ tool
provides a graphical user interface for the construction of graphical
arguments.\footnote{We are considering other representations.}  There
are three basic nodes: \emph{claims}, \emph{arguments}, and
\emph{evidence} and these combine to produce \emph{argument steps} in
which (sub)claims or evidence nodes link to an argument node that
links to a parent claim.  The argument node provides justification
that the subclaims or evidence logically entail the parent claim; the
justification may require additional (side) claims to ensure
attributes such as indefeasibility.  Other kinds of node may appear in
\ifelse{a {\sc Clarissa}}{an Assurance 2.0}\ argument, such as comment, defeater, and subcase, but these
serve dialectical rather than logical purposes; see Section
\ref{defeaters}.

An assurance case argument, as we have specified it, has rather
limited scope and can therefore take a rather restricted form: it is
not concerned with constructing intricate chains of logical
inferences, but just a few basic steps for structuring and organizing
references to external models, theories and evidence.  Thus, \ifelse{{\sc Clarissa}}{Assurance 2.0}\
uses only five different kinds of argument steps: these are called
(building) \emph{blocks} \cite{Bloomfield&Netkachova14} and they
comprise \emph{decomposition}, \emph{substitution}, \emph{concretion},
\emph{calculation}, and \emph{evidence incorporation} and are
described in more detail in Sections \ref{interior} and \ref{leaves}
and illustrated in Figure \ref{busy}.

In the typical structure of an Assurance 2.0 case, general claims at
the upper level are refined into more precise claims using concretion
steps, then substitution steps are used to elaborate these claims
about high level models into claims about low level models and their
implementations, and these lowest level claims are discharged by
evidence.  Application of evidence is generally accomplished in two
steps: the lowest step performs evidence incorporation to justify a
claim about ``something measured'' (e.g., ``we did requirements-based
testing and achieved MC/DC coverage'') and this supports a second step
(typically a substitution based on application of an external theory)
that connects this to a claim about ``something useful'' (e.g., ``we
have no unreachable code''); see Sections \ref{leaves} and
\ref{evincsec}.  At any stage, the argument may divide into subcases
using decomposition or calculation steps that enumerate a claim over
some structure (e.g., over components, requirements, hazards, etc.) or
that split the conjuncts of a compound claim.  This structure may
recurse within subcases.

We require that argument steps are \emph{deductive} whenever possible.
This means that the claim justified by a step should be logically
implied by the conjunction of evidence or subclaims supporting it.
This is in contrast to \emph{inductive} argument steps where the
evidence and subclaims merely ``suggest'' their parent claim with
various degrees of force.  \ifelse{{\sc Clarissa}}{Assurance 2.0}\ blocks generally have
\emph{side-claims} whose purpose is to enforce deductiveness: for
example, a step that decomposes over hazards will have a side-claim
that requires justification that all hazards have been identified and
that all the individual hazards \emph{and their combinations} are
considered in the decomposition.

The reasons for advocating deductivism are that a) every inductive
step harbors an anonymous \emph{doubt} (otherwise it would be
deductive) and we prefer to eliminate these if possible, or at least
to identify them explicitly so
that they can be analyzed and recorded, and b) we wish to interpret
completed arguments as logical proofs using \emph{Natural Language
Deductivism} (NLD) \cite{Groarke99}.  In NLD, the evidence
incorporation steps that constitute the leaves of the argument tree
are interpreted as \emph{premises} and the interior steps as
\emph{axioms} having the form of definite clauses: that is,
conjunctions of subclaims that deductively imply their claim.

NLD is an informal counterpart to deductive proof in formal
mathematics and logic but differs in that its premises and axioms are
``reasonable or plausible'' rather than certain, and hence its
conclusions are likewise reasonable or plausible rather than certain
\cite[Section 4.2]{sep-informal-logic}.  NLD differs significantly
from standard interpretations of informal argumentation, where weaker
or different forms of inference may be used \cite{Blair15}; the very
term ``natural language deductivism'' was introduced by Govier
\cite{Govier87} as a pejorative to stress that this style of argument
does not adequately represent ``informal argument.''  However, our
focus is not informal arguments in general, but the structured
arguments of assurance cases, where deductive validity is a natural
counterpart to the requirement for indefeasibility, and so we depart
from the association of assurance cases with informal argument and
adopt the label NLD with pride.

Because our treatment is close to that of formal logic, we adopt its
terminology and say that an argument is \emph{valid} if its reasoning
steps are logically so (i.e., true in all interpretations) and that it
is \emph{sound} if, in addition, all its steps are so well justified
that they can be accepted as true (i.e., we set a high bar for
``reasonable or plausible'').\footnote{We explain later, in Section
\ref{interior}, that we prefer (but do not require) completed
arguments to be sound and ``fully valid'' meaning that, in addition to
being logically valid, they are deductive and have no unaddressed
doubts or defeaters.  During development, we allow arguments to be
incomplete and lacking full validity; we evaluate these as best we can
and tackle their deficiencies in an iterative manner.}

As the logic used in assurance cases is elementary (basically,
propositional calculus), validity simply requires that all the
argument steps ``fit together'' correctly.  That is, if a step has a
subclaim $C$, then the subargument that justifies this must deliver
precisely $C$, and not some $C\,'.$  The \ifelse{{\sc Clarissa}}{prototype} tools
that construct Assurance 2.0 arguments do so in a way that largely
guarantees logical validity.  For example, at the top of Figure
\ref{busy}, we have a decomposition block delivering a ``more precise
claim'' that is used by a concretion block.  It would be a logical
validity fault if the two instances of the claim (i.e., the one
delivered and the one used) were different, but this is excluded
because there is just one instance of the claim and it is referenced
by both blocks.  Nonetheless, it is possible that the justification
for the lower block is inadequate, so that it really delivers only
some $C\,'$ and not $C$.  Note, however, that this is not logical
invalidity but unsoundness, which is discussed next.

A logically valid argument is \emph{sound} when all its evidence
incorporation steps cross some threshold for credibility, and all its
interior or reasoning steps have indefeasible justifications.  As we
will explain in Section \ref{confirmation}, we use \emph{confirmation
measures} to assess the ``weight'' of evidence in support of a claim
and thereby judge soundness for evidence incorporation steps.  For
interior reasoning steps, we rely on human judgment to assess the
justification supplied, but we expect most of these steps to be the
application of some well-accepted theory, so the judgment builds on a
reliable foundation.  

Observe that the requirements for soundness (indefeasibility,
deductiveness, confirmation measures), although rigorous, are
straightforward: there is no doubt what is required in both
construction and evaluation.  This is what we mean by ``simplicity
through rigor'' and it may be contrasted with the complex criteria
proposed for less constrained forms of assurance case
\cite{Chowdhury-etal:Safecomp20}.

Soundness is the most fundamental property we desire of an assurance
case, but there are other useful properties and in the next subsection
we identify different perspectives and measures that can be used to
develop confidence in a case.


\subsection{Confidence in an Assurance Case}


As we stated in the beginning, the purpose of an assurance case is to
assemble and deliver indefeasible justification for its top claim.
After assessing the case, we will have some degree of belief that this
purpose has been achieved and we call this degree of belief the
\emph{confidence} in the case.  Confidence is a human judgment that
should be based on evaluable and measurable attributes of the case but
we do not think it can be reduced to a single attribute or
measurement.  Instead, we think that confidence should be based on
three related criteria.

\begin{enumerate}
\item Does the assurance case argument justify validity of its claims,
and the top claim in particular?

\item Are there gaps, discrepancies, or weaknesses in the claims,
evidence, argument steps or justifications?

\item Are the identified gaps and weaknesses within a tolerable
    threshold of risk?
\end{enumerate}
We refer to these criteria as positive and negative perspectives
on the assurance argument and its residual risks, respectively, and
now describe them in more detail.

\paragraph{Positive Perspectives:} These consider the extent to which the
evidence and overall argument make a positive case to justify belief
in its claims.  We have already encountered one positive measure:
namely, \emph{soundness}, which interprets the argument as a logical
proof by NLD and delivers a yes/no measurement.


\begin{figure}[p]
\begin{center}
\vspace*{-12ex}
\includegraphics[height=1.10\textheight]{busy-example-vertical.png}
\end{center}
\vspace*{-5ex}
\caption{\label{busy}Example \ifelse{{\sc Clarissa}}{Assurance 2.0}\ Argument}
\end{figure}

In assessing whether the evidence provided in an evidence
incorporation step justifies its claim with sufficient ``weight'' to
be accepted as a premise in the NLD interpretation, we make use
of the measures of \emph{confirmation theory}, which are based on more
basic assessments expressed as (possibly qualitative) subjective
probabilities indicating, for example, our confidence in the claim,
given the evidence.   These valuations are discussed in Section
\ref{confirmation}.

Probabilities can be aggregated from evidence through the steps of the
argument using various kinds of probability logic to yield what we
call \emph{probabilistic valuations} for the claims (in contrast to
soundness, which is a \emph{logical valuation}), including the top
claim.  Advocates of several alternative interpretations of assurance
cases treat their preferred probabilistic valuations as \emph{the}
assessment of confidence in a case; Graydon and Holloway show these
treatments are problematic
\cite{Graydon&Holloway:quant16,Graydon&Holloway:quant17}.  We apply
probabilistic valuations only to cases that have already been judged
sound and, furthermore, our assurance cases are limited to steps
comprised of just the five building blocks; together, these
restrictions eliminate many of the sources of difficulty exposed by
Graydon and Holloway.

An alternative to probabilistic valuations constructed by external
examination of the case is to include probabilistic measures among the
claims.  This is particularly appropriate for claims concerning
properties such as reliability and for those based on probabilistic
evidence such as statistically valid random testing
\cite{Currit86,Parnas90}.  The claims will then be justified within
the argument by reference to some accepted theory.



\paragraph{Negative Perspectives:} These record doubts about the case,
and their exploration and resolution.  Reviewers will naturally have
doubts and questions about an assurance case and it is sensible to
anticipate these and respond to them within the case.  In addition,
the developers of the case need to guard against \emph{confirmation
bias} \cite{Leveson11:JSS,Nimrod09}.  To ensure that the positive
perspective does not become an optimistic one, they should actively
explore doubts and challenges as they develop the case---and should
record these, both to avoid rework, and to aid reviewers.

We refer to any concern about a case as a \emph{doubt}; as we explore
the origin and nature of a doubt we will refine it to a
\emph{defeater}, that is, a specific (counter)claim or challenge that
can be attached to a particular point in the argument.  Investigation of a
defeater may lead to correction or improvement of the assurance case,
in which case the modifications become part of the positive case and
the defeater that motivated them may be mentioned only in the text of
some of its justifications.  Alternatively, the defeater may, on
investigation, be considered a ``false alarm''; the investigation that
reveals this can be represented as a (sub)case in its own right, and
may be recorded within the main case.  {\sc Clarissa/asce}\ has functions for
recording defeaters and for developing and recording the subcases that
lead to their resolution (we refer to this as the defeaters' own
defeat), and these can be revealed or hidden as desired.

 The number of resolved defeaters might be considered a measure of
the effectiveness or diligence with which the negative perspective has
been explored \cite{Weinstock:Baconian13}; this can be subject to
gaming (e.g., using trivially different defeaters to raise the number
of resolutions), but can be effective when undertaken with care as
``eliminative argumentation''
\cite{Goodenough-etal:TR2014,Diemert&Joyce2020}.

A defeater to an assurance case is rather like a hazard to a system:
that is a conjecture why things might go wrong.  Hazard analysis is
not judged by how many hazards are found, but by the historical record
and rational justification of the method used, and the diligence of
its performance.  We think similar evaluations should be applied to
the negative perspectives of an assurance case and so we advocate use
of systematic (and potentially automated) methods for discovery of
defeaters.  These include methods based on Answer Set Programming
\cite{Gelfond&Kahl14} and application of ``knowledge bases''
concerning historical flaws in both systems \cite{Driscoll:dashlink}
and assurance cases \cite{Greenwell-etal06} (although the strict
requirements of Assurance 2.0 cases are intended to exclude most
fallacies of the latter kind ``by construction'').




\paragraph{Residual Doubts:} The world is uncertain so not all doubts
can be resolved.  For example, we may design a system to tolerate any
two faults and have good reasons and evidence to suppose that is
sufficient to cover the exposure on any expected mission.  But doubts
remain: what if more than two faults do arrive?  Or, for a security
perspective, what if advances elsewhere render our cryptographic key
length insufficient?  Here we can explore consequences and likelihoods
and thereby assess \emph{risk} (their product).  Some of these
\emph{residual risks} may be unacceptable and thereby prompt a review,
but others may be considered acceptable or unavoidable.  It is crucial
however that these judgments are conscious ones and that they are
recorded in the assurance case.


We now develop valuations and measurements for each of the
perspectives introduced above.



\newpage
\section{Positive Perspectives: Logical Valuation (Soundness)}
\label{soundness}











Recall that our fundamental requirement is that an assurance case
should provide \emph{indefeasible justification} for the decision to
deploy the system or service concerned; this means that the
justification must be so well supported, and all plausible doubts and
objections must be so thoroughly considered and countered, that we are
confident there are no credible doubts remaining that could change the
decision.

Confidence in the investigation and resolution of doubts and
objections is discussed in Section \ref{defeaters}, and confidence
that any remaining as residual doubts pose insignificant or
manageable risks is discussed in Section \ref{residuals}.  During
development, we will probably attempt to identify and resolve doubts
before proceeding to assessment from a positive perspective.
Nonetheless, we present the positive perspective first, because it
aligns with the most basic goal of an assurance case argument.

So, in this section and the next we are concerned with positive aspects
of the case: namely that its evidence and argument justify confidence
in its claims.  In the next section, we consider these positive
aspects from a probabilistic point of view, while in this section we
consider a logical point of view, which we call \emph{soundness}.

Soundness was introduced in Section \ref{structure} and is discussed
in the paper on Assurance 2.0 \cite{Bloomfield&Rushby:Assurance2} and
its more theoretical precursors \cite{Rushby:Shonan16,Rushby:AAA15}
that together provide the basis for Assurance 2.0.  Briefly, soundness
interprets the argument of an assurance case as an informal proof
based on \emph{Natural Language Deductivism} (NLD).  This means that
the leaf steps of an assurance case argument are interpreted as
\emph{premises} in which evidence establishes a claim, and the
interior steps are interpreted as \emph{axioms} in which a conjunction
of (sub)claims implies a parent claim (see Figure \ref{busy} for an
example).  The full argument is then a tree of claims (possibly with
cross links if a (sub)claim is used in support of multiple claims)
whose top claim is the conclusion of the assurance case.

We need to be sure that evidence really does establish its claim, and
that subclaims really do imply their parent, so each argument step is
supplied with a \emph{justification} why this is so.  The
justification will be in natural language but it may reference some
external theory, calculation, proof, or mechanized analysis etc.

The benchmark for an interior step is that the conjunction of its
subclaims deductively implies or entails its parent claim (so that
each interior step is what logicians call a ``definite clause'').
Doubts about the deductivism of a step---that is, a suspicion there is
``something missing'' among the subclaims, so that their conjunction
merely ``suggests'' rather than entails the parent claim---causes a
step to be considered ``inductive'' rather than
deductive.\footnote{There is a stronger form of doubt, where the
argument step is considered wrong rather than merely incomplete.
This case is discussed in Section \ref{residuals}.}

We now consider how confidence in deductivism can be established.

\subsection{Confidence in Deductiveness (Interior Steps)}
\label{interior}

Free-form arguments often challenge their developers with the
``bewilderment of choice''; in contrast, \ifelse{{\sc Clarissa}}{Assurance 2.0}\ arguments are built from
a limited repertoire of just five different argument blocks, of which
four apply to interior steps.  Selection of an appropriate block is
assisted by the ``helping hand'' pictorial memory aid shown in Figure
\ref{helping-hand}.

\begin{figure}[ht]
\begin{center}
\includegraphics[width=\textwidth]{helping-hand.png}
\end{center}
\caption{\label{helping-hand}The Helping Hand Memory Aid}
\end{figure}

\begin{figure}[ht]
\begin{center}
\includegraphics[width=4in]{decomp-block.png}
\end{center}
\vspace*{-3ex}
\caption{\label{decomp-block}Generic Decomposition Building Block}
\end{figure}

As illustrated in Figure \ref{decomp-block},
Assurance 2.0 blocks generally have a \emph{side-claim}, which is a
(conceptually distinct) subclaim whose purpose is to ensure that the
other subclaims are well formed and really do deductively entail the
parent claim.  The relationship is then
$$ \mbox{side-claim} \supset (\mbox{conjunction of other subclaims} \supset
\mbox{parent claim}).\footnote{We use $\supset$ for
material implication, $\wedge$ for conjunction, $\vee$ for
disjunction, and $\neg$ for negation.}$$
This is logically equivalent to
$$ (\mbox{side-claim} \wedge \mbox{conjunction of other subclaims}) \supset
\mbox{parent claim}$$
and so we see that although the side-claim has a conceptually
distinct status, it is logically no different from the other subclaims.

Every branch in a complete assurance case argument must terminate in
evidence (or, exceptionally, a calculation).   Assurance case
arguments or subarguments that have unsupported claims as in Figure
\ref{decomp-block} are incomplete and unfinished.
Some assurance case notations have a symbol that explicitly indicates
unfinished parts of the case; \ifelse{{\sc Clarissa}}{Assurance 2.0}\ can use subcase nodes for this
purpose, as illustrated in Figure \ref{busy}, but does not require it,
regarding unsupported claims as sufficient indication of an unfinished
branch.\footnote{ Unsupported claims can also be interpreted as
\emph{assumptions}; in this case it would be useful to distinguish
those unsupported claims that are assumptions from those that indicate
incompleteness and we may revise these aspects as we gain experience
with the {\sc Clarissa}\ prototype.}

The argument step of Figure \ref{decomp-block} illustrates a decomposition
block, whose purpose is to divide a claim into subclaims over some
explicit enumeration, such as components of the system, or time (e.g.,
past, present, future), or hazards, and so on.  In each case, the
side-claim must establish that the decomposition is complete and
satisfies any other properties that may be needed, such as that the
claim distributes over components, or that some theory justifying the
decomposition is properly applied.  For example, if the decomposition
is over hazards, then the side-claim will require that all hazards
have been identified and that the decomposition considers them all,
both individually and in combination; such a side-claim might be
discharged by evidence that attests to use of a well-accepted method
of hazard analysis, performed diligently.

\begin{figure}[ht]
\begin{center}
\includegraphics[width=4.5in]{decomp-defeaters.png}
\end{center}
\vspace*{-3ex}
\caption{\label{decomp-doubts}Three Ways to Indicate Doubt in an
    Argument Step}
\end{figure}

 Now it may be that we have doubts about the decomposition (and
therefore also about justification for its side-claim) and wish to
indicate this in the developing assurance case so that we can return
to it later.  One approach would be to annotate the argument step as
inductive.  This can be indicated informally by adding a marker to the
argument step as illustrated by the triangle in Figure
\ref{decomp-doubts}; {\sc Clarissa/asce}\ allows this, but does not provide an
interpretation for it at present.  An alternative is to use an
explicit \emph{defeater} node; the defeater can point to the argument
or to a specific subclaim to localize the perceived source of doubt,
or to both as illustrated on the right of Figure \ref{decomp-doubts}.
A third alternative is to add an unsupported subclaim (equivalently,
an uninterpreted assumption) acknowledging something is ``possibly
missing'' as shown at the bottom of Figure \ref{decomp-doubts}.  The
three options illustrated in this figure are alternatives: we should
select one.



Identified defeaters must be investigated and resolved before a case
can be considered complete, but it is not required to perform this
resolution before considering other parts and other aspects of the
case.  If the doubt motivating a defeater is found to be unwarranted,
then it is said to be a ``defeated defeater'' and the justification
and possible subargument for this assessment will be recorded as part
of the case and selectively revealed or hidden as will be described in
Section \ref{defeaters}.  If, on the other hand, the defeater
identifies a legitimate doubt, then the missing or incorrect claim(s)
must be discovered and the argument step (and the subarguments that
justify it) suitably amended.









\begin{wrapfigure}{r}{.5\textwidth}
\vspace*{-1.5ex}
\begin{center}
\includegraphics[width=0.45\textwidth]{repair-start.png}
\end{center}
\vspace*{-3ex}
\caption{\label{repair-start}Defeater to a Generic Subcase}
\vspace*{-2.5ex}
\end{wrapfigure}


Missing and suspected missing subclaims are easily added to
decomposition steps as shown by the ``possibly missing'' subclaim at
the bottom of Figure \ref{decomp-doubts}, which will either be removed
or be replaced by the truly missing subclaim(s) as the doubt is
resolved.  This is not so straightforward when the doubt concerns
other kinds of argument steps because these take only a single
subclaim.  An example is illustrated in Figure \ref{repair-start}
where a ``not deductive'' defeater is aimed at a generic subcase.
Suppose we determine that the defeater is legitimate and that an additional
subclaim is needed.  There are two approaches: we can add this
subclaim below the original argument, as shown on the left of Figure
\ref{repair}, or above it, as shown on the right of that figure.


\begin{figure}[ht]
\raisebox{16ex}{\hfill\includegraphics[width=0.46\textwidth]{repair-below-edited.png}}
\hfill\includegraphics[width=0.46\textwidth]{repair-above.png}\hfill
\caption{\label{repair}Additional Claim Added Below, or Above
    Original Argument}
\end{figure}


Notice that when the additional claim is added above the existing
argument, we must recognize that only a weakened form of the original
claim is supported by the existing subcase.  Apart from this
adjustment, however, the original case remains intact (i.e., we do not
need to introduce a weakened claim) and this may be considered an
advantage for the ``added above'' choice.

\subsubsection{Embedded Links}

The argument of an assurance case is required to satisfy certain
structural properties.  For example, claims cannot link directly to
claims (there must be an intermediate argument step), and the pattern
of links must be non circular.  These requirements are easily checked
and are also visibly obvious when all links are explicit, as we have
assumed until now.  However, the nodes of an Assurance 2.0 argument
must each be supplied with narrative descriptions of their
interpretation or justification, and in {\sc Clarissa/asce}\ these may contain
embedded links to other nodes.

\begin{figure}[ht]
\begin{center}
\includegraphics[width=\textwidth]{embedded-links.jpg}
\end{center}
\vspace*{-3ex}
\caption{\label{embedded-links}Embedded Links}
\end{figure}


These links serve a different, narrative, purpose than conventional
links, whose purpose is logical.  Consequently, they do not
participate in logical (i.e., soundness) or probabilistic valuations
of the argument.  For example, in an assurance case for an autonomous
drone, we may have a primary case that argues it is functionally safe
in the style of ``Overarching Properties'' (OPs)
\cite{Overarching18,Holloway:OP19}, and a secondary case that argues
it complies with a relevant standard called F3269-17 \cite{F3269-17}.
The narrative for the node making the latter claim may contain a table
of all the objectives required by the standard and, for each of them,
an embedded link to an existing node in the case where that objective
has been satisfied as part of the OP subcase.   {\sc Clarissa/asce}\ is able
selectively to display such links or not; they are shown displayed (in
gray) in Figure \ref{embedded-links}.  Note that the arrows are
reversed compared with conventional logical links as an indication of
their different purpose.

In this example, the secondary case serves as a source of potential
defeaters.  In particular, those objectives from the F3269-17 standard
that are not satisfied by the OP subcase can be added to the argument
as defeaters as shown on the right of Figure \ref{embedded-links}.
Notice that here we use defeater nodes for the missing objectives, as
opposed to the ordinary claim node used in Figure \ref{decomp-doubts}.
As we will see in Section \ref{defeaters}, resolution of a legitimate
defeater begins by replacing it with (or interpreting it as) a claim,
so Figure \ref{decomp-doubts} can be considered to have skipped a step
compared to Figure \ref{embedded-links}.  If (or when) all the
F3269-17 objectives are satisfied, the secondary case can be used to
increase confidence in the primary case.















Another use for embedded links is in referencing the application of a
theory and its template to an argument subcase, as described in the
following subsection.



\subsubsection{Theories and Templates}
\label{templates}

We introduced the notion of \emph{theories} early in this report, in
Section \ref{theories}; the idea is that a theory provides
justification for an argument step or series of steps, or for a
complete subcase.  Considering the general case, each of the argument
steps in a theory-supported subcase will cite some aspect of the
theory as its justification, and the side-claims (and possibly their
support) will likewise reference aspects of the theory, as will the
evidence supplied.

The linkage just described between theory and subcase is informal and
each theory-supported subcase is constructed afresh.  We might be able
to provide more automated assistance if the theory explicitly provides
a generic subcase that can be instantiated to yield the specific
subcase required in the context concerned.  Such generic subcases
would have much in common with what some other tools for assurance
cases call ``templates,'' and we will also use this term.  However,
unlike other methodologies and tools, we see templates as
representations of the syntax for a theory, rather than independent
entities, and we regard the theory as the primary item of interest,
and the focus for assurance, because it provides semantics and is the
source of justification.

When theories provide templates, we can envisage tool support that
uses templates a) to check manually constructed theory-supported
subcases, b) to construct those subcases automatically under human
direction, and c) to synthesize automatically parts of an assurance
case by searching for applicable theories and templates.

At present, {\sc Clarissa/asce}\ provides the first of these and will soon provide
the second; the third is a topic of ongoing research.  To indicate the
place where a theory/template should be applied, we use an embedded
link (recall the previous subsection) to connect the theory/template
concerned to the claim that it will justify.  The terms appearing in
that claim are used to instantiate the generic template, which is then
used to check or construct the subcase supporting the claim concerned.
By instantiate, we mean that the generic template will contain
placeholders that behave like formal parameters in a programming
language: for example, a theory to ``establish correctness of CLEAR
requirements using CLEAR tools'' may have a generic top claim
``requirements for \$x\$ are correct,'' where \$X\$ indicates a
parameter.  When this is applied to a claim ``requirements for
ArduCopter AFS are correct,'' the parameter will be instantiated as
``ArduCopter AFS,'' with similar substitutions elsewhere in the
template.\footnote{CLEAR is a tool-supported requirements notation
from Honeywell \cite{Bhatt:CLEAR18} and AFS stands for ``Advanced
Failsafe Monitor,'' which is a safety monitor for an autonomous
autonomous quadcopter (``ArduCopter'') being developed as part of the
ARCOS program by the DesCert team \cite{DesCert:phase1-arxiv,Bhatt:FM22}.}

When a theory/template is applied, we will eventually need to
discharge the instantiations of its side-claims.  If we are unable to
do so, this may indicate that the selected theory/template was an
inappropriate choice.  We would like to learn this early, before
effort has been wasted, so some side-claims in the template may be
marked as \emph{preconditions}; these must be discharged before the
theory/template may be applied.  For example, it would make no sense
to apply the CLEAR theory for correctness assurance to requirements
that are not written in CLEAR, so ``requirements for \$X\$ are written
in CLEAR'' is a precondition for this example.





\subsection{Confidence in Evidential Support for Claims (Leaf Steps)}
\label{leaves}\label{confirmation}


The argument of an assurance case is logically valid when all its leaf
claims are supported by evidence and the claims supporting and
delivered by interior steps ``match up'' to provide a coherent graph
structure.   We say the argument is \emph{fully valid} when, in
addition, all its steps are (judged to be) deductive, and there are no
unresolved defeaters other than those marked as residual doubts.  It
is not important in what order validity, deductiveness, and absence of
defeaters are tackled and assessed for full validity.  A fully valid
argument is sound when human evaluators attest that the residual
doubts are negligible (see Section \ref{residuals}), that the
justification for each interior step is satisfactory, and that the
weight of each evidential step is sufficient to justify its claim, as
we now describe.






In the logical valuation of an assurance case by NLD, we interpret
evidence incorporation steps as premises.  For soundness we therefore
require strong justification that the evidence supplied to the step
really does support its claim.  Unlike other assurance steps, which
inhabit the world of logic, evidence incorporation steps are bridges
to that world from the world of observation and measurement.
Therefore we cannot assess evidence incorporation steps by the methods
of logic, we need the methods of epistemology.  Epistemology is about
justified belief (as an approximation to truth) and it is natural to
express the strength of our confidence in a belief as a number.  We
will expect those numbers to obey certain rules (the Kolmogorov
Axioms) and so they function as (subjective) probabilities
\cite{Jeffrey04}.


A natural measure of confidence in a claim $C$ given the evidence $E$
is the subjective posterior probability $P(C \,|\, E),$ which may be
assessed numerically or qualitatively (e.g., ``low,'' ``medium,'' or
``high'').  However, confidence in the claim is not the same as
confidence that it is justified by the evidence.  It is possible that
the reason for a high valuation of $P(C \,|\, E)$ is that our prior
estimate $P(C)$ was already high, and the evidence $E$ did not
contribute much.  So it seems that to measure justification we ought
to consider the difference from the prior $P(C)$ to the posterior $P(C
\,|\, E)$ as an indication of the ``weight'' of the evidence $E.$
Difference can be measured as a ratio, or as arithmetic difference,
thereby producing the following two \emph{confirmation measures}, due
to Keynes in 1921 and Eells in 1982, respectively.\footnote{The
logarithm (which may use any positive base) in Keynes' and other ratio
measures serves a normalizing purpose so that, as with arithmetic
difference, positive and negative confirmations correspond to
numerically positive and negative measures, respectively, and
irrelevance corresponds to a numerical measure of zero.}
\begin{eqnarray*}
\mbox{Keynes}(C, E) & = & \log\frac{P(C \,|\, E)}{P(C)},\\[1ex]
\mbox{Eells}(C, E) & = & P(C \,|\, E) - P(C).
\end{eqnarray*}








There are many other confirmation measures proposed in the literature
\cite{Tentori-etal07}.  For example, some prefer to use the likelihood
$P(E \,|\, C)$ rather than the posterior $P(C \,|\, E),$ because it is
generally easier to estimate the probability of concrete observations
(i.e., evidence), given a claim about the world, than vice-versa,
thereby giving us the likelihood variants of Keynes' and Eells'
measures:\footnote{Notice that $\mbox{L-Keynes}(C, E) =
\mbox{Keynes}(C, E)$
and $\mbox{L-Eells}(C, E) = \mbox{Eels}(C, E)\times\frac{P(E)}{P(C)},$
since $P(C \,|\, E) \times P(E) = P(C
\wedge E) = P(E \wedge C) = P(E \,|\, C) \times P(C)$.}
\begin{eqnarray*}
\mbox{L-Keynes}(C, E) & = & \log\frac{P(E \,|\, C)}{P(E)},\\[1ex]
\mbox{L-Eells}(C, E) & = & P(E \,|\, C) - P(E).
\end{eqnarray*}
We can see that these will tend toward their maxima when $P(E)$ is
small, meaning that $E$ should be unlikely in general.  This suggests
that we should favor evidence whose occurrence (in the absence of $C$)
would be a \emph{surprise}.




Similarly, if we have accepted evidence $E_1$ and seek additional
evidence, we should look for $E_2$ that is (or remains) surprising in
the presence of $E_1.$  Thus, for example, if $E_1$ is evidence of
successful tests, it will not be surprising if additional tests are
successful; instead we should seek evidence $E_2$ that is ``diverse''
from $E_!,$ such as static analysis.  More formally, we have, by the
chain rule
\begin{eqnarray*}
P(C \wedge (E_2 \wedge E_1)) & = & P(C \,|\, E_2 \wedge E_1) \times
    P(E_2 \,|\, E_1) \times P(E_1), \mbox{\ and}\\
P(E_2 \wedge (C \wedge E_1)) & = & P(E_2 \,|\, C \wedge E_1) \times P(C \,|\, E_1) \times P(E_1).
\end{eqnarray*}
The left (and hence right) hand sides are equal, and so
\begin{equation}
\frac{P(C \,|\, E_2 \wedge E_1)}{P(C \,|\, E_1)} =  \frac{P(E_2 \,|\,
    C \wedge E_1)}{P(E_2 \,|\, E_1)}.\label{diverse}
\end{equation}
Thus, $E_2$ delivers the largest ``boost'' to Keynes' measure for the
justification provided by $E_1$ (i.e., the left hand side of
(\ref{diverse})) when $E_2$ would be surprising given only $E_1,$ but
not when given $C$ as well, which confirms that $E_2$ should be
\emph{diverse} from $E_1.$
These observations about ``surprising'' and ``diverse'' evidence are
intuitively plausible, but it is satisfying to see them put on a
rigorous footing.



An additional consideration when evaluating evidence is that
it is not enough for the evidence to
support a given claim $C,$ it should also discriminate between that
claim and others, and the negation, or ``counterclaim'' $\neg\, C$ in
particular.  Again, discrimination or distance can be measured as a
ratio or as arithmetic difference, leading to the following two
measures; the first is due to Good (and Turing) from codebreaking
activities during World War 2:
\[\mbox{Good}(C, E) = \log\frac{P(E \,|\, C)}{P(E \,|\, \neg\, C)},\]
and the second is due to Kemeny and Oppenheim in 1952:
\[\mbox{KO}(C, E) = \frac{P(E \,|\, C) - P(E \,|\, \neg\, C)}{P(E
\,|\, C) + P(E \,|\, \neg\, C)}.\]


We will refer to these as ``Type 2'' confirmation measures, and the
previous examples as ``Type 1.''  Likelihoods are related to
posteriors by Bayes' Rule, and appearances of $P(\neg\, x)$ in Type 2
measures can be replaced by $1 - P(x)$, so
\begin{eqnarray*}
\mbox{Good}(C, E) & = & \log\frac{P(C \,|\, E) \times P(E) / P(C)}
{P(\neg\, C \,|\, E) \times P(E) / P(\neg\, C)}\\
& = & \log\frac{P(C \,|\, E) \times P(\neg\, C)}
{P(\neg\, C \,|\, E) \times P(C)}\\
& = & \log\frac{P(C \,|\, E) \times (1 - P(C))}
{(1 - P(C \,|\, E)) \times P(C)}\\
& = & \log\frac{O(C \,|\, E)}{O(C)}
\end{eqnarray*}
where $O$ denotes \emph{odds} (i.e., $O(x) = P(x)/(1-P(x))$) and
Good's measure is therefore sometimes referred to as the ``log odds''
or ``log odds-ratio'' measure for weight of evidence
\cite{Good:weight83}.

Similar manipulations can be performed on other Type 2 measures, so
that appearances of $\neg\, C$ revert to just $C$ and the distinction
between Type 2 and Type 1 measures disappears.  Furthermore, notice
that appearances of $P(E)$ cancel out in the second line of the
derivation above; manipulations of other measures exhibit the same
behavior and we find that they then generally satisfy the following
conditions:


\begin{enumerate}
\item They can be expressed as functions of $P(C \,|\, E)$ and $P(C)$ only,

\item They are increasing functions of $P(C \,|\, E),$ and

\item They are decreasing functions of $P(C).$

\end{enumerate}


Not all confirmation measures satisfy 1 above.  For example, the
following measure due to Carnap in 1962 \[\mbox{Carnap}(C, E) = P(C
\wedge E) - P(C)\times P(E)\] depends nontrivially on
$P(E).$\footnote{Notice that $\mbox{Carnap}(C, E) = \mbox{L-Eells}(C,
E) \times P(C),$ so the L-Eells measure does not satisfy condition 1
either.}  However, such measures can be manipulated by irrelevant
evidence \cite[section 2]{Atkinson12}, so we prefer measures that do
satisfy condition 1.


All confirmation measures indicate the extent to which evidence
justifies a claim, but they are not ordinally equivalent.  That is to
say, a given confirmation measure may rank one scenario (i.e.,
combination of $P(C \,|\, E)$ and $P(C)$) higher than another, but a
different measure may do the reverse.  This is acceptable because,
although all confirmation measures evaluate the degree to which
evidence $E$ justifies claim $C,$ they do so in different ways and we
may prefer one measure to the other (or prefer different measures for
different purposes) \cite{Hajek-Joyce:confirmation08}.

Nonetheless, it is possible to add a fourth condition to the list above
and all measures satisfying this enhanced set of conditions are
ordinally equivalent.  This condition is the following
\cite{Atkinson12,Shogenji12}.
\begin{enumerate}
\setcounter{enumi}{3}
\item Let $C_1$ and $C_2$ be claims, unconditionally independent and
also conditionally independent on evidence $E.$  If both $C_1$ and
$C_2$ have measures of confirmation greater (resp.\ less) than $t$
then their conjunction must also have measure greater (resp.\ less)
than $t.$
\end{enumerate}
Measures that satisfy all four conditions are called
\emph{justification measures} \cite{Shogenji12}.  An example is
Shogenji's measure \[\mbox{Shogenji}(C,E) = 1 - \frac{\log P(C \,|\, E)}{\log
P(C)}.\]

Shogenji argues that only justification measures serve to increase
true beliefs (e.g., claims) while reducing false ones
\cite{Shogenji12}, asserting that simple confidence measures (e.g.,
$P(C \,|\, E)$) fail to do this and that traditional confirmation
measures may rank beliefs inconsistently.  In assurance, however, we
are usually seeking \emph{strong} indications that evidence justifies
a claim and the measures are likely to concur on this, so we are
generally content to use confirmation rather than justification
measures.  

 {\sc Clarissa/asce}\ can attach confirmation measures to evidence incorporation
steps and it allows these steps to be marked as ``accepted'' when the
weight of evidence (e.g., as indicated by an attached confirmation
measure) is judged to exceed some threshold.  Since the discussion
above concludes that all confirmation measures will deliver similar
conclusions, it may seem that we could have selected one and bypassed
the discussion.  However, although the conclusions may be similar,
they are based on elicitation of different judgments and we believe
there can be value in asking assessors to consider the different
points of view underlying these judgments.  For example,
$\mbox{Keynes}(C, E)$ elicits judgments $P(C \,|\, E)$ and $P(C)$,
while $\mbox{L-Keynes}(C, E)$ elicits $P(E \,|\, C)$ and $P(E)$.
Furthermore, the two measures should yield the same value; we can
therefore provide feedback to assessors if their judgments are
inconsistent.  Similarly, the original formulation of $\mbox{Good}(C,
E)$ elicits judgment of $P(E \,|\, \neg\,C)$, which requires
consideration of a contrary point of view.




Some will be skeptical that human developers and evaluators are able
to assess and manipulate probabilistic measures correctly, even
qualitatively, and will also contend that confirmation measures are
beyond everyday experience.  They may point to alleged flaws in human
evaluation of probabilities.  Here is a standard illustration
\cite{Tversky&Kahneman:conjunction83}.
\begin{description}
\item[Evidence $E$\,:]
Linda is 31 years old, single, outspoken and very
bright. She majored in philosophy.  As a student, she was deeply
concerned with issues of discrimination and social justice, and also
participated in anti-nuclear demonstrations.
\end{description}
\noindent
The challenge is to assess which of the following two claims is best
supported by the evidence.
\begin{description}
\item[Claim $C_1$:] Linda is a bank teller,


\item[Claim $C_2$:] Linda is a bank teller and active in the feminist movement.
\end{description}

When human subjects are exposed to this and similar examples, they
overwhelmingly favor $C_2.$ Psychologists label this the ``conjunction
fallacy'' because $C_2$ is the conjunction of $C_1$ with another
clause and a conjunction must always be \emph{less} probable than
either of its components; they then cite it as evidence for the
assertion that intuitive human reasoning is poor at probabilities
\cite{Tversky&Kahneman:conjunction83,Kahneman11}.  However, a more
recent interpretation is that humans evolved to weigh evidence and
actually base their judgments on mental measures more akin to
confirmation than simple probabilities
\cite{Crupi-etal08,Shogenji12,Jonsson&Shogenji19}.\footnote{There are
larger claims, widely accepted in areas of psychology and cognitive
science, that much human perception and unconscious decision making
are based on processes akin to Bayesian analysis over models
\cite{Clark13,Friston:free-energy10,Friston12:history,Knill&Pouget04,Rao&Ballard99,Gregory:eye-brain}.}
To see this, we observe that the evidence $E$ seems to add nothing to
our prior belief in $C_1$ but it does seem to support the second
clause of claim $C_2$ (i.e., ``is active in the feminist movement'')
and so by item 2 of the list of properties for confirmation measures,
we conclude that the evidence indeed confirms $C_2$ more than $C_1,$
thereby refuting the ``fallacy'' charge.

Claim $C_2$ entails the further claim that ``Linda works outside the
home'' (since she is a bank teller), but the evidence provides no
direct support for this and it could easily be false.  Thus, we have
evidence that soundly supports a claim that logically entails a
further claim, yet that second claim could be false.  For a more
extreme example, the evidence that a card drawn from a deck is an Ace
supports the claim that the card is the Ace of Hearts, and this
entails the further claim that the card is red.  But the card used in
evidence could have been the Ace of Clubs, which refutes the derived
claim that it is red.  A pragmatic resolution to this apparent paradox
is that the standard for assurance should be more demanding than basic
confirmation: if an evidentially supported claim is a conjunction,
then we need indefeasible support for all elements of the conjunction,
and so, in the context of assurance, we should not accept that the
evidence about Linda is sufficient to establish claim $C_2.$




Another approach would be to propagate probabilities and likelihoods
from evidence through the directly supported claims to these
``second-level'' claims and to evaluate confirmation there.  In the
Linda and Ace of Hearts examples, we see that the evidence provides no
support for the second-level claims (i.e., ``works outside the home''
and ``card is red'').  These ``two level'' steps for exploiting
evidence are common in assurance cases: the bottom step, using an
evidence incorporation block, connects the evidence to a claim about
``something measured'' (e.g., ``we did requirements-based testing and
achieved MC/DC coverage'') while the second step (typically a
substitution block based on application of an external theory)
connects it to a claim about ``something useful'' (e.g., ``we have
no unreachable code'').  We recommend that confirmation measures are
evaluated against the ``something useful'' claims.

Sometimes a mismatch between the claims about ``something measured'' and
``something useful'' leads to the realization that one or the other is
misstated.  Here is an example: during World War 2, the US Army Air
Force came to its Statistical Research Group in New York seeking
advice on where best to add armor to improve the survival of their
airplanes.  Many damaged planes returning from engagements had been
examined and this produced the following evidence.

\begin{center}
\begin{tabular}{|l|l|}
\hline
Section of plane & Bullet holes per sq. ft. \\
\hline
Engine & 1.11 \\
Fuselage & 1.73 \\
Fuel system & 1.55 \\
Rest of plane & 1.8 \\
\hline
\end{tabular}
\end{center}

The fuselage seems the most heavily damaged of the identified
components, so the evidence seems to support the claim ``the place
where armor will best improve survival of the plane is the fuselage.''
This is actually a second-level (``something useful'') claim; we
should begin by using the evidence to justify a first-level
(``something measured'') claim.  A plausible candidate for this is
``the fuselage is the part of the plane with heaviest damage.''  An
important difference in these two claims is that the first level
speaks of ``damage'' while the second level speaks of ``survival.''
Thus we need either some inference from damage to survival, or the
first level claim should also speak of survival.  This leads to a key
insight: the evidence comes exclusively from planes that survived.
Hence the first level claim should be changed to ``the fuselage is the
part of the plane that can survive heaviest damage.''  From there it
is a short step to deduce that planes with heavy damage to the engines
did not survive and hence the celebrated recommendation by Abraham
Wald that the best place to apply armor is where the bullet holes are
not \cite{Ellenberg15}.

Another area where human reasoning about probabilities is claimed to
be notoriously unreliable concerns the ``base-rate fallacy''
\cite{Bar-Hillel80}.  The standard examples involve diagnostic tests
for disease.  Suppose we have a test that is perfectly accurate at
diagnosing the disease when it is present (i.e., no false negatives),
but also has 10\% false positives.  A person tests positive in a
population where 1\% has the disease.  Human subjects are asked which
of the following probabilities is closest to the true probability the
person has the disease: a) 90\%, b) 10\%, c) 50\%, d) 89\%.

The correct answer is b) but human subjects overwhelmingly choose one
of the other answers, with an average of 85\% \cite[page
44]{Bandyopadhyay-etal16}.  The psychologists' explanation is that
humans overlook the very low base rate of the disease, which means
that false positives (10\%) overwhelm true positives (1\%).  (Others
would say it is because they do not know or do not apply Bayes' Rule.)
An alternative explanation again involves confirmation: the evidence
(positive test) increases the probability of the claim (having the
disease), so by item 2 of the list of properties for confirmation
measures, we obtain positive confirmation; human subjects opt for a
large number as a way of expressing this, despite being asked about
probabilities, not confirmation.\footnote{Few subjects will have
technical knowledge of probabilities or confirmation; the point is
that their intuitive reasoning is sound for many purposes, and uses
confirmation rather than probabilities.}  Although intuitive human
reasoning is again exonerated by supposing it employs (informally)
confirmation rather than probability, we would hope that developers
and evaluators of assurance cases are explicit in any choice between
probability and confirmation, and also apply Bayes' Rule in
circumstances like these (on representative numbers if only
qualitative estimates are being used).


A different example where population probabilities may confound
elementary reasoning is the ``Paradox of the Ravens'' \cite{Hempel45}.
Here, we seek evidence for the claim ``all ravens are black''; the
equally valid contrapositive of this claim is ``all non-black objects
are non-ravens'' for which a white shoe is produced in evidence,
allowing the triumphant declaration ``that proves it---all ravens
\emph{are} black!''

A plausible escape from this ``paradox'' is \emph{Nicod's criterion}
\cite{Nicod30} that only observations of ravens should affect our
judgment whether all ravens are black.  More generally, claims about
some class of objects can be confirmed or refuted only by evidence
about those objects.  Under this criterion, we expect that
observations of black ravens would tend to confirm our claim, while a
non-black raven definitely refutes it.  Good, in a cleverly titled
one-page paper \cite{Good:red-herring67}, rebuts this expectation with
an example where observation of a black raven disconfirms the claim
``all ravens are black.''
\begin{quote}
Suppose that we know we are in one or other of two worlds, and the
claim under consideration is that all the ravens in our world are
black.  We know in advance that in one world there are a hundred black
ravens, no non-black ravens, and a million other birds; in the other
world there are a thousand black ravens, one white raven, and a
million other birds.  A bird is selected equiprobably at random from
all the birds in our world and turns out to be a black raven.  This is
strong evidence that we are in the second world, wherein not all
ravens are black.
\end{quote}

Examples such as this are challenging to philosophers seeking to
explain and justify the methods of science, but for assurance the
salient points are that we need to be skeptical about evidence (hence
consideration of alternative claims and counterclaims) and may need to
collect additional evidence to rule out alternative explanations.  (In
Good's example, observations of additional birds would allow us to
determine if we are in the world with a hundred ravens, or the one
with a thousand.)
Confirmation measures provide an attractive framework in which to
probe these issues and, far from being difficult for human evaluators,
they correspond to inbuilt human faculties for the weighing of evidence.











\subsection{Overall Assessment of Soundness}
\label{overall-soundness}

As noted in Section \ref{interior}, the argument of an assurance case
is \emph{fully valid} when, in addition to being logically valid, all
its claims are supported by evidence, all its steps are deductive, and
there are no undefeated defeaters.  A fully valid argument is
\emph{sound} when human evaluators attest that the justification for
each interior step is satisfactory, and that the weight of each
evidential step is sufficient to justify its ``something useful''
claim, as explained in Section \ref{leaves}.   {\sc Clarissa}\ can check these
requirements and highlight violations.  In particular, {\sc Clarissa/asce}\ allows
argument steps to be marked when they are fully valid and again when
their justification is considered sound, and can propagate these
assessments and indicate them by coloring nodes so that developers can
readily perceive how much of the argument is considered fully valid
and sound.

The requirements for full validity are strong: in practice, it may not
be possible (or credible) to make some steps deductive or,
equivalently, they may be made so only by using an unjustified claim
(i.e., assumption).  Therefore, exceptions can be tolerated in the
assessment of full validity (and thus soundness), but the goal should
be ``as deductive as possible and inductive only as strictly
necessary.''  In particular, the residual risks due to these
exceptions must be adjudged small, as will be described in Section
\ref{residuals}.  We prefer assumptions to inductive steps as these
identify the source of doubt more precisely.  For the same reason, we
also suggest that no undefeated defeaters should be present when a
case is submitted for assessment: the source of concern should have
been eliminated or mitigated and thereby reduced to a residual risk,
or localized to an assumption.

 Thus, in evaluating an assurance case, we recommend that the
presence of inductive steps, defeaters, and unsupported claims or
assumptions should cause the case to be labeled ``inductive.''  During
development, these deficiencies should be examined and progressively
eliminated, or else reduced to residual risks that will be reported
separately and evaluated as described in Section \ref{residuals}.

\begin{figure}[t]
\begin{center}
\vspace*{-12ex}
\includegraphics[width=\textwidth]{process.pdf}
\end{center}
\vspace*{-5ex}
\caption{\label{process}Logical Assessment Process}
\end{figure}

These steps in the process of logical assessment for an assurance case
argument are portrayed in Figure \ref{process}.  If the case is
incomplete, the assessment proceeds in a relaxed mode; if minor errors
(e.g., misspelled claims) are present, these should be corrected but
we do not flag them as invalidities or defeaters.  Logically invalid
arguments should be corrected; those with nondeductive steps may
either be revised or continue their assessment with the caveat
``inductive'' attached.  Similarly, defeaters may either be addressed
or the assessment allowed to proceed in their presence.  The order in
which validity, deductiveness, and defeaters are assessed is not
important.  To the extent possible, we also assess soundness for
incomplete and inductive cases.

A completed case should have a fully valid argument and is considered
sound when all its steps are assessed to justify their claims, based
on the subclaims or evidence provided.  Confirmation measures can
assist this judgment for evidential steps but we do not recommend
developers or evaluators of assurance cases should fix on specific
confirmation measures and make their numerical assessments a rigid
criterion for judging the evidential justification for a claim.
Rather, we expect them to apply the ideas presented in Section
\ref{leaves} ``qualitatively'' and to consider prior beliefs and
counterclaims when assessing the extent to which evidence justifies a
claim.  These qualitative judgments can be developed and honed by
``what if'' experiments using numerical representations for the
probabilities concerned.  When evidence is composed of multiple items
that are assessed separately but are not conditionally independent,
then it may be necessary to use advanced methods and tools such as
Bayesian Belief Nets (BBNs)
\cite{Littlewood&Wright:tse07,Fenton&Neil12,hugin} to calculate the
probabilities that will be used in the confirmation measure.  Again,
we recommend numerical experiments using BBN tools to develop
understanding of the interactions involved and development of
appropriately simplified rules for qualitative judgments.

Summarizing the discussion from the previous section, we suggest that
selection and assessment of evidence can proceed as follows.  First,
it is sensible to seek evidence that would be surprising (i.e., not
expected) if the claim is untrue and, if multiple forms of evidence
are available, to seek those that are diverse, that is, not associated
with each other unless the claim is true.  The claim should be at the
``something useful'' level and there should be a suitable theory
available that connects such claims to the measurements and
observations delivered as evidence.  We should follow Nicod's
criterion and select evidence that supports the claim directly rather
than by delicate inference and, if the claim is a conjunction, we
should ensure that each conjunct is supported by some part of the
evidence.  Next, a confirmation measure can be evaluated and assessed
as an indication of the weight of that evidence.  Keynes' measure is
attractive as its original and likelihood forms are the same.
Numerical experiments can be performed to establish a suitable
threshold for the measure.  Finally, counterclaims should be
considered and the discriminating power of the evidence assessed with
the aid of measures such as Good's.  Again, numerical experiments can
be used to establish thresholds.

We continue our examination of assurance cases from a positive
perspective by proceeding from their logical to their probabilistic
evaluation before turning to negative perspectives and the important
role of defeaters.

\newpage

\section{Positive Perspectives: Probabilistic Valuation}
\label{propagation}

Soundness is one aspect in the positive assessment of confidence for
an assurance case, but it lacks gradation.  Suppose, for example, we
have a sound case, then reduce its threshold for weight of evidence
and reduce the quantity or quality of evidence accordingly; the case
remains sound, but we are surely less confident in the verity of its
top claim.  A different ``weakening'' is seen in DO-178C
\cite{DO178C}, where Design Assurance Levels (DALs) A to C require
both High and Low Level Requirements (HLR and LLR), whereas (the
lower) Level D requires only HLR\@.  Intuitively, the idea is that we
are less confident of the large ``leap'' in reasoning from
implementation directly to HLR than of the combination of steps from
implementation to LLR and then to HLR.

The motivation for these ``weakened'' cases is that they should be
cheaper to produce, yet might still be adequate for less critical
systems, or for less critical claims.  Dually, we would like some
basis for believing that the additional cost of the original
``strong'' cases does deliver greater confidence in their claims.
What we seek, therefore, is a way to augment soundness with a
graduated measure that indicates the strength of our confidence in the
case.

The strength of confidence in an assurance case is naturally expressed
as a probability.  We could assess this as a subjective evaluation of
the entire case, but a more principled method is to calculate it as
the composition of assessments for the basic elements of the case,
such as evidence, and individual argument steps.  This will involve
some combination of logic and probability, which is a notoriously
difficult topic, because the two fields have different semantic
foundations \cite{Nilsson86,Gaines78,Adams98}.

Nonetheless, there are numerous proposals for calculating
probabilistic confidence in assurance cases by methods of this kind
(e.g., \cite{Denney-etal11:ESEM,Ayoub-etal:SSS13}), but a study by
Graydon and Holloway \cite{Graydon&Holloway:quant17} cast doubt on
many of them.  Graydon and Holloway examined 12 proposals that use
probabilistic methods to quantify confidence in assurance case
arguments: five based on Bayesian Belief Networks
\cite{Fenton&Neil12}, five based on Dempster-Shafer \cite{Shafer76} or
similar forms of evidential reasoning such as J{\o}sang's opinion
triangle and subjective logic \cite{Josang16}, and two using other methods.
By perturbing the original authors' own examples, they showed that all
the proposed methods can deliver implausible results.

We suspect that the reason for this disappointing behavior is that the
methods concerned are attempting a double duty: they aim to evaluate
confidence in the case, but also (implicitly) its soundness.
Probabilistic methods are poorly suited to the latter task, which is
more naturally cast in terms of logic.  In \ifelse{{\sc Clarissa}}{Assurance 2.0}\ we separate these
evaluations and assess soundness as a logical property, as described
in the previous section, and only for cases assessed to be sound do we
proceed to assess probabilistic confidence.  Nonetheless, we intend to
explore Graydon and Holloway's examples when our tools are fully
developed.  Our methods for probabilistic valuation are compositional
over the five basic building blocks of Assurance 2.0 cases, as
described in the following subsections.

\subsection{Evidence Incorporation Blocks}
\label{evincsec}

\begin{wrapfigure}{r}{.5\textwidth}
\vspace*{-3.5ex}
\begin{center}
\includegraphics[width=0.5\textwidth]{evidence-block.png}
\end{center}
\vspace*{-2ex}
\caption{\label{evinc}Evidence Incorporation Block}
\end{wrapfigure}

A generic evidence incorporation block is shown in Figure \ref{evinc}.
The basic idea is that observations (e.g., measurements, tests, or
analyses etc.) on the system under consideration yield evidence $E$
that is asserted to support claim $C\,$; the assertion of support is
justified by a narrative attached to the evidence incorporation
argument block, which may be further supported by a side-claim or
warrant W.  As indicated in the figure, the claim $C$ will generally
be about ``something measured'' and the side-claim $W$ will generally
concern provenance of the evidence and will be supported by a subcase
establishing this.  For example, if $E$ is evidence from testing, then
$C$ will be a statement about the test outcomes, such as ``no failures
in $n$ tests'' or ``MC/DC coverage achieved''; it will not be an
interpretation or ``something useful'' statement about the tests, such
as ``achieved reliability 0.99'' or ``no unreachable code present''
since these are ``something useful'' inferences derived from the test
measurements via a suitable theory of testing that will be applied in
a higher-level substitution block.  The provenance side-claim $W$ and
its supporting subcase must establish that the tested artifact is the
real thing, that the test oracle and any measurement harness are
trustworthy, and that the test procedure is sound and was performed
correctly, and so on.

As we explained in Section \ref{leaves}, the subjective posterior
probability $P(C \,|\, E)$ is a natural expression of confidence in
the claim $C,$ given the evidence $E.$  However, when assessing
soundness we use a confirmation measure rather than the posterior
probability because we wish to evaluate the discriminating power, or
``weight,'' of the evidence, and confirmation measures do this.  But
once we have assessed soundness, it is reasonable to use the posterior
(or a qualitative approximation to this) as our measure of
probabilistic confidence in the claim $C$ and it is this that will be
propagated through the probabilistic valuation for the rest of the
case.  (Note that if the evidence incorporation step uses multiple
items of evidence then their individual contributions $P(C \,|\, E_1),
P(C \,|\, E_2), \ldots, P(C \,|\, E_n)$ will be combined into the
overall $P(C \,|\, E)$ using methods such as BBNs.)


Now $P(C \,|\, E)$ is an epistemic judgment and it can be performed
in several ways.  One way would consider the totality of the
information about $E,$ including its provenance and other items
represented in the side-claim $W.$ In this case, probabilistic
confidence in $C,$ which we write as $P_{\!\mathit{conf}}(C),$ will be simply the
``holistic'' $P(C \,|\, E).$ Another way might assess $P(C \,|\, E)$
using only the direct contribution of $E$ to $C,$ with the side-claim
$W$ assessed separately.  In this case, probabilistic confidence in
$C$ will be some combination of $P(C \,|\, E)$ and probabilistic
confidence in the side-claim, $P_{\!\mathit{conf}}(W),$ which will be accumulated
over the subcase supporting $W.$ There are several plausible forms for
the combination including arithmetic product (corresponding to logical
conjunction) \[P_{\!\mathit{conf}}^P(C) = P(C \,|\, E) \times P_{\!\mathit{conf}}(W)\] and ``sum
of (probabilistic) doubts'' \[P_{\!\mathit{conf}}^D(C) = P(C \,|\, E) + P_{\!\mathit{conf}}(W) -
1.\] We describe these in more detail in the following section.

\subsection{Substitution and Concretion Blocks}
\label{sub-conc}

A generic substitution or concretion block is shown in Figure
\ref{substconc}.  As described earlier, in Section
\ref{substitution}, a substitution block has a subclaim $S$
expressing some property $A$ of a model $P$ that is used to justify
property $B$ of model $Q$ as the claim $C$.  Special cases arise when
the properties or models are the same.  If the properties $A$ and $B$
are the same (so that, for example, we are justifying correctness of
the HLR on the basis of correctness of the LLR), then the method of
justification is generally to show that the models $P$ and $Q$ are
``equivalent'' which may be achieved informally by traceability
analysis, or formally by verification of a homomorphism.  If the
models $P$ and $Q$ are the same (so that, for example, we are
justifying absence of unreachable code on the basis of MC/DC coverage
by requirements-based tests) then the method of justification is
generally to appeal to some theory that addresses the topic.

Concretion blocks are somewhat similar: they justify a typically
abstract property and model (e.g., ``the system shall be correct'') on
the basis of a more concrete property and model (e.g., ``the system
shall satisfy its HLR'').

The significant feature of substitution and concretion blocks from the
perspective of probabilistic confidence propagation is that the claim
$C$ is derived from just a single subclaim $S,$ subject to a
side-claim or warrant $W.$
For soundness, we require that the parent claim is deductively
entailed by the subclaim, subject to the side-claim.  That is, $ W
\supset (S \supset C),$ which is equivalent to $ W \wedge S \supset
C.$ A narrative in the argument block must justify this relationship
indefeasibly.

\begin{wrapfigure}{R}{.5\textwidth}
\vspace*{-2ex}
\begin{center}
\includegraphics[width=0.5\textwidth]{sub-or-conc-block.png}
\end{center}
\vspace*{-3ex}
\caption{\label{substconc}Substitution/Concretion Block}
\vspace*{-4ex}
\end{wrapfigure}

When we consider probabilistic confidence, we apply a probabilistic
interpretation to the implication above, so that \[P_{\!\mathit{conf}}(C) \approx
P_{\!\mathit{conf}}(W \wedge S).\] The probabilistic confidence $P_{\!\mathit{conf}}(W \wedge S)$
is given by $P_{\!\mathit{conf}}(W) \times P_{\!\mathit{conf}}(S \,|\, W)$ but we expect the lower
steps of the argument (i.e., the subcases supporting $W$ and $S$) to
supply $P_{\!\mathit{conf}}(W)$ and $P_{\!\mathit{conf}}(S)$\@.  Since $P_{\!\mathit{conf}}(S)$ is not the same
as $P_{\!\mathit{conf}}(S \,|\, W)$ (unless $S$ and $W$ are independent), this is
not quite what is required.  However, the structure of a sound
assurance case is such that all the claims and subclaims appearing in
its argument must be true---so when we evaluated the subclaims and
evidence contributing to $S,$ we implicitly did so in a context where
$W$ is true.  Hence, our assessment of probabilistic confidence in the
subclaim $S$ is really confidence \emph{given} the rest of the case,
and so the confidence we labeled $P_{\!\mathit{conf}}(S)$ is ``really'' $P_{\!\mathit{conf}}(S
\,|\, W)$ and probabilistic confidence in $P_{\!\mathit{conf}}(W \wedge S)$ can
indeed be taken as the product of probabilistic confidence in its two
subclaims.  Thus \[P_{\!\mathit{conf}}^P(C) = P_{\!\mathit{conf}}(S) \times P_{\!\mathit{conf}}(W)\] where we
use the superscript $P$ in $P_{\!\mathit{conf}}^P(C)$ to indicate this is the
``product'' calculation.



Some may feel that this calculation is too aggressive and would prefer
a more conservative approach.  One such is the ``sum of doubts''
approach: our doubt in the parent claim is no worse than the sum of
doubts for its subclaims and side-claims \cite{Adams98}.

The ``doubts'' referred to here are \emph{probabilistic doubts} as
opposed to the other use of the term to mean general disquiet or
concern.  Probabilistic doubt in a claim $C$ is probabilistic
confidence in its negation $P_{\!\mathit{conf}}(\neg C),$ so
\begin{eqnarray*}
P_{\!\mathit{conf}}(\neg C) & \approx & P_{\!\mathit{conf}}(\neg(S \wedge W))\\
 & = & P_{\!\mathit{conf}}(\neg S \vee \neg W)\\
 & = & P_{\!\mathit{conf}}(\neg S) + P_{\!\mathit{conf}}(\neg W) - P_{\!\mathit{conf}}(\neg S \wedge \neg W)\\
 & \leq & P_{\!\mathit{conf}}(\neg S) + P_{\!\mathit{conf}}(\neg W).
\end{eqnarray*}
Then, since $P_{\!\mathit{conf}}(\neg C) = 1 - P_{\!\mathit{conf}}(C),$ and similarly for $\neg S$
and $\neg W,$ we have
\[P_{\!\mathit{conf}}^D(C) \geq P_{\!\mathit{conf}}(S) + P_{\!\mathit{conf}}(W) - 1\]
where the superscript $D$ indicates this is the ``sum of
(probabilistic) doubts'' calculation.

These derivations of $P_{\!\mathit{conf}}^P(C)$ and $P_{\!\mathit{conf}}^D(C)$ also justify the
similar formulas presented in the previous subsection for evidence
incorporation steps.

Choosing a method for propagation of probabilistic confidence is a
matter for judgment by the developers and evaluators of an assurance
case.  We have proposed two candidates for $P_{\!\mathit{conf}}(C)$: one,
$P_{\!\mathit{conf}}^P(C)$ is aggressive but makes strong assumptions; the other,
$P_{\!\mathit{conf}}^D(C)$ is conservative but requires only weak assumptions.
There is no reason to think that either candidate is ``correct'' and
developers may use either of these or an alternative method (with a
satisfactory explanation) of their own devising.  We do, however,
consider it reasonable that any good estimate will lie between those
given by $P_{\!\mathit{conf}}^P(C)$ and $P_{\!\mathit{conf}}^D(C).$

The indefeasibility criterion of Assurance 2.0 requires that the
conjunction of subclaim and side-claim should deductively entail the
parent claim; hence we identify confidence in the parent claim with
confidence in this conjunction.  However, it is possible that,
although we are persuaded of the logical entailment, our probabilistic
confidence in the parent claim differs from that suggested by the
calculation above.  For example, we noted earlier that DO-178C
requires both High and Low Level Requirements at DALs A--C, but only
HLR at DAL D.  Intuitively, the idea is that the more costly
combination of substitution steps from implementation to LLR and then to HLR
engenders more confidence than the single large step from
implementation directly to HLR, even though all the steps are
assessed as deductive.  This can be accommodated by defining a factor $f$ such
that confidence in the parent claim $C$ is given by
\begin{equation}\label{factor-f}
P_{\!\mathit{conf}}(C) =
f \times P_{\!\mathit{conf}}(S \wedge W)\footnote{Alternatively, $f$ could be a function
$f(P_{\!\mathit{conf}}(S \wedge W))$.}
\end{equation}
\footnotetext{Alternatively, $f$ could be a function: $f(P_{\!\mathit{conf}}(S \wedge W))$.}
(or a qualitative approximation thereto), where
$P_{\!\mathit{conf}}(S \wedge W)$ represents the chosen method for combining $P_{\!\mathit{conf}}(S)$
and $ P_{\!\mathit{conf}}(W)$.

Exceptionally, we allow the \emph{inductive} justification of an
argument step, where the conjunction of the subclaims and side-claims
``strongly suggest'' but do not imply the parent claim.  This means
there must be some missing element\footnote{It is possible that $W$ or
$S$ are \emph{wrong} rather than weak, and therefore cannot be
corrected by conjoining an $M.$ See the discussion of residual
interior doubts in Section \ref{resinterior}.} $M$ that would make the
relationship deductive: \[ W \wedge M \wedge S \supset C.\] Presumably
$M$ is unknown (otherwise we would have included it), but the fact
that we have labeled the argument step inductive means that we
recognize its (possible) existence.  The reason we deprecate inductive
steps is that the absent $M$ represents a \emph{defeater}, that is a
condition that can invalidate the argument, and we prefer these to be
identified more specifically.

Rather than label the step inductive, we could instead represent $M$
explicitly as an unsupported claim labeled ``something missing here.''
This may be conjoined either to $W$ (i.e., the side-claim is too
weak) or to $S$ (i.e., the subclaim is too weak), or split between
them.  Alternatively, $M$ could be represented by an explicit defeater
node.  We prefer these alternatives to inductive steps because they
are more explicit about the existence and location of the potential
defeater.

Recall, from the discussion around Figure \ref{process} in Section
\ref{overall-soundness}, that in evaluating the soundness of an
assurance case with inductive steps or with unsupported ``something
missing'' claims or explicit defeaters, we ignore these elements, but
label the whole case ``inductive'' and therefore in need of intense
and skeptical scrutiny.

When evaluating probabilistic confidence in such a case, a strict
approach would assess zero confidence for inductively justified
claims, unsupported ``something missing'' claims, and the targets of
defeater nodes.  Such assessments will propagate upwards and deliver
zero confidence in the top claim.  However, we have already labeled
the case ``inductive'' and are aware of its defeasible character, so
we would like the confidence assessment to say something useful beyond
this.  {\sc Clarissa/asce}\ accommodates this by allowing manual adjustment to
calculated values for probabilistic confidence: confidence in a
defeated claim can be left unchanged, or set to zero, or reduced to
some intermediate value.  Nodes are color coded according to
user-selected thresholds on their probabilistic confidence and
adjustment to these settings can provide developers with
visualizations that help focus their attention on weak areas of the
case and to comprehend the scope of their impact.


\subsection{Decomposition Blocks}

Decomposition blocks are used when a claim can be decomposed into
subclaims distributed over some set or structure, such as components,
properties, configurations, hazards, or time, and so on.  A side-claim
ensures that the decomposition is valid: that is, all elements of the
decomposition are considered, and the subcases are disjoint, etc.  A
generic example was shown earlier, in Figure \ref{decomp-block}.
















As with substitution and concretion blocks, there are several plausible
ways to estimate probabilistic confidence in the parent claim $C$ from
that in its subclaims $S_1,\ldots,S_n$ and side-claim $W.$  These
include the product calculation
\[P_{\!\mathit{conf}}^P(C) = P_{\!\mathit{conf}}(W) \times \prod_{i=1}^n P_{\!\mathit{conf}}(S_i)\]
and the sum of probabilistic doubts
\[P_{\!\mathit{conf}}^D(C) = P_{\!\mathit{conf}}(W) - n + \sum_{i=1}^n P_{\!\mathit{conf}}(S_i),\]
which can each be derived by generalizing the corresponding description
in the previous subsection.


Also as with substitution and concretion blocks, developers and
evaluators of assurance cases may choose one of these two methods or
invent some other way to estimate propagation of confidence.  The
product calculation assumes that the subclaims to the decomposition
are independent, which may not be so.  For example, we might establish
partitioning among tasks by decomposing this into time partitioning
and space partitioning.  These are logically disjoint, but both might
be enforced by the operating system kernel, so they are hardly
independent.  Conversely, the sum of probabilistic doubts calculation is very
sensitive to subclaims with low confidence, but analysts may consider
those subclaims to apply only to unimportant (i.e., low risk)
circumstances.  Thus, analysts may adjust either of these estimates or
use one of their own devising, perhaps employing BBNs or
Dempster-Shafer's theory of evidence \cite{Shafer76}, but we do suppose
that reasonable estimates will lie between $P_{\!\mathit{conf}}^D(C)$ and
$P_{\!\mathit{conf}}^P(C).$

Also as we have seen before, it may be that the method of
decomposition raises or reduces confidence in the parent claim, and
this can be represented by applying some factor or function $f$ to the
calculation of $P_{\!\mathit{conf}}(C).$

\begin{figure}[t]
\begin{center}
\begin{tabular}{|c|c|c||c|c|}
\hline
 n  & $P_{\!\mathit{conf}}(S_i)$ & $P_{\!\mathit{conf}}(W)$ & \rule[-1.5ex]{0ex}{3.9ex}$P_{\!\mathit{conf}}^P(C)$ & $P_{\!\mathit{conf}}^D(C)$\\
 \hline \hline
 1 & 0.99 & 0.99 & 0.98 & 0.98 \\
 1 & 0.95 & 0.95 & 0.90 & 0.90 \\
 1 & 0.90 & 0.90 & 0.81 & 0.80 \\
 1 & 0.95 & 0.80 & 0.76 & 0.75 \\
 \hline 
 2 & 0.99 & 0.99 & 0.97 & 0.97 \\
 2 & 0.95 & 0.95 & 0.86 & 0.85 \\
 2 & 0.90 & 0.90 & 0.73 & 0.70 \\
 2 & 0.95 & 0.80 & 0.72 & 0.70 \\
 \hline
 3 & 0.99 & 0.99 & 0.96 & 0.96 \\
 3 & 0.95 & 0.95 & 0.81 & 0.80 \\
 3 & 0.90 & 0.90 & 0.66 & 0.60 \\
 3 & 0.95 & 0.80 & 0.69 & 0.65 \\
 \hline
 5 & 0.99 & 0.99 & 0.94 & 0.94 \\
 5 & 0.95 & 0.95 & 0.74 & 0.70 \\
 5 & 0.90 & 0.90 & 0.53 & 0.40 \\
 5 & 0.95 & 0.80 & 0.62 & 0.55 \\
 \hline
\end{tabular}
\end{center} 
\caption{\label{conftab}Confidence Calculations for
Representative Decomposition Blocks}
\end{figure}

We have often advocated numerical ``what if'' experiments to develop
intuition on the behavior of probabilistic measures and in Figure
\ref{conftab} we present the results of one such experiment.  We
consider a decomposition block with claim $C$ having $n$ subclaims
$S_i$ and a side-claim $W.$  The first three columns of the table list
values for $n,$ $P_{\!\mathit{conf}}(S_i)$ (assumed to be the same for all
subclaims), and $P_{\!\mathit{conf}}(W),$\footnote{Of course, the results would be
unchanged if the same probabilities were distributed differently among
the subclaims and side-claim.}  while the two rightmost columns list
corresponding values for $P_{\!\mathit{conf}}^P(C)$ and $P_{\!\mathit{conf}}^D(C),$ respectively.
The first four rows consider the case $n=1,$ which covers substitution
and concretion blocks (and, to a certain extent, evidence
incorporation blocks as well). 

We see that for most combinations, $P_{\!\mathit{conf}}^P(C)$ and $P_{\!\mathit{conf}}^D(C)$ are
very close\footnote{Note that the product calculation with $n$ total
side- and subclaims yields $(1-d)^n$, where $d$ is probabilistic doubt
in each of these claims and, by the binomial expansion, this is
$1-n\times d+ \mathrm{smaller\ terms}$.  Similarly, the sum of doubts
is $n \times d$, which yields confidence $1- n\times d$.  Thus the
product and sum of doubts calculations deliver very similar values for
confidence when $d$ is small.}; they diverge as confidence in the
subclaims is reduced (corresponding to the third row in each block)
and their number is increased.  We also see that one low-confidence
input (corresponding to the fourth row in each block) has a
substantial impact and that this is most marked for the sum of doubts
measure and for larger $n.$

The main conclusions seem to be that decomposition blocks with many
subclaims require strong confidence in those subclaims, and that all
subclaims (and side-claims) need similar levels of confidence.





\subsection{Calculation Blocks}

Calculation blocks are much like decomposition blocks except the claim
and subclaims concern the values of some (usually numerical)
quantities and the quantity in the parent claim is calculated from
those in the subclaims using a formula justified (presumably by citing
some theory) in the body of the calculation block, subject to
constraints cited in the side-claim.  The analysis of probabilistic
confidence then follows that for decomposition blocks.

\subsection{Overall Assessment of Probabilistic Confidence}
\label{probs}

If the goal is to make a strongly argued case for some probabilistic
assessment of the system under consideration, such as its reliability,
then it seems best to make this quantity a part of the top claim and
to arrange the case to justify it explicitly, probably by reference to
suitable theories for reliability estimation (see \cite[Section
3.2]{Bloomfield&Rushby:Assurance2} for an example).  We call this an
\emph{internal} probabilistic assessment because it is constructed
inside (i.e., as part of) the argument.  A variant is an
\emph{indirect} probabilistic assessment where we use a substitution
block to justify a probabilistic claim by adherence to a standard.
For example, DO-178C \cite{DO178C} and governing regulations
\cite{10-9,CS-25} indicate DO-178C Level A is suitable for a
probability of failure on demand (\emph{pfd}) of $10^{-9}$
while Level D is
sufficient for \emph{pfd} of $10^{-3}$.  (The
notion of \emph{demand} is flexible; for example, it can be
interpreted as a single iteration of a cyclic control system, or an
hour of operation---the usual case in avionics, or a complete
mission.)

In contrast to these approaches, an \emph{external} probabilistic
assessment is constructed outside the (otherwise independent) argument
in the manner illustrated by the previous subsections, and will
generally be much more approximate as it depends on generic analyses.
Note that an external assessment will deliver \emph{probabilistic
confidence in a (logical) claim} (e.g., 99.9\% confident in the absence for
critical faults), not a \emph{probabilistic claim} (e.g., reliability
wrt.\ critical failures better than 99.9\%).  Additional work is
required to connect these concepts, as described in Section
\ref{cbi}.

Unlike other authors who develop theories for probabilistic confidence
in assurance cases, we do not advocate any particular approach
(although the chosen approach should be used consistently) nor
consider any of them ``correct.''  Because these analyses are generic,
they are conservative to the point where their actual numerical
estimates may be of little direct value.  For example, if we take the
$n=3$ case in Figure \ref{conftab}, we see that when confidence in the
subclaims or evidence supporting the block, and in the side-claim, is
0.99, then confidence in the parent claim is 0.96 (i.e., 0.99 to the
fourth power, using the product calculation); if we iterate this
(i.e., we use four such blocks to support the three subclaims and the
side-claim for another such block), confidence in the next level will
be 0.85 at best (i.e., 0.96 to the fourth power), then 0.52 at the
third level, and a mere 0.07 at the fourth level.  Using sum of
doubts, the corresponding doubts are 0.04 (i.e., 0.01 times 4) at the
first level, 0.16 at the second, then 0.64 at the third, and 1 (since
doubts cannot exceed 1) at the fourth level, corresponding to a
confidence of zero.  These calculations seem to suggest that larger
arguments, with larger quantities of evidence, tend to reduce total
confidence.  This might be true, all other things being equal, but
they do not remain equal as we will now see.

First, we recognize that the basic product and sum of doubts
calculations do indeed depend only on confidence in the evidence
supplied and in any assumptions\footnote{We treat unsupported claims
as assumptions, and expect some probabilistic assessment of confidence
to be assigned to them.}, but not on the shape or size of the argument
tree above them.  That is, for the product calculation, probabilistic
confidence in the top claim is simply the product of probabilistic
confidence in all evidence and assumptions (as can be proved by
induction on the height of the argument tree).  Similarly, for the sum
of doubts calculation, the doubt in the top claim is simply the sum of
probabilistic doubts over all evidence and assumptions.

However, although the basic calculation of confidence depends only on
the evidence and assumptions and not on the argument, this does not
imply that confidence is invariant under transformation to the
argument---for different arguments may require different evidence, and
even the same evidence may deliver different confidence for different
claims.  Furthermore, the transformed argument must remain sound and
this may lead to different side-claims that require different evidence
or assumptions.  More significantly, a transformed argument may have
better justification.  Recall that in Section \ref{sub-conc} formula
(\ref{factor-f}), we introduced a factor or function $f$ that is used
to adjust probabilistic confidence according to the strength of the
justification provided, and this may change as the argument changes.

DO-178C illustrates these topics.  Design Assurance Levels (DALs) D
and E of DO-178C reason directly from code to HLR, whereas the higher
DALs A, B, and C insert intermediate steps involving LLR.\@ These
extra steps involve additional evidence and it might seem this will
reduce overall confidence.  It certainly would do so if confidence in
the additional steps were comparable to that in the originals but, as
described earlier, confidence in the smaller steps from code to LLR
and then to HLR can be much greater (due to stronger theories and
methods for verification) than the single large leap from code to
HLR\@.  This will be reflected in stronger confidence in the evidence
and in the justifications (and hence in the factors $f$), resulting in
greater confidence overall.


As we noted earlier, the absolute numbers delivered by our external
methods of probabilistic assessment must be used with caution.
Because it is based on human assessment of confidence in evidence and
assumptions, and because this may vary greatly with different
assessors or circumstances \cite{Kahneman21:noise}, the very
foundation of the calculation may be considered unstable.
Furthermore, because the methods of propagation are generic and
conservative, they likely underestimate the overall confidence that a
``more exact'' probabilistic calculation would assess, if such were
available.



We are comfortable with these limitations: we consider soundness to be
the critical property, with probabilistic confidence as a useful but
inexact augmentation that assessors can use to keep track, in a
rational manner, of the location and extent of weak and strong parts
of an argument and that may be particularly valuable when exploring
residual doubts (see Section \ref{residuals}) and graduated assurance.
That is to say, although probabilistic confidence calculated for the
top claim may be small, the reasons for this apply uniformly and so it
can be used to compare different assessments of residual risk and
different methods for graduating an argument by trading cost
(typically, for gathering evidence) against confidence for less
critical components or properties.

Accordingly, {\sc Clarissa/asce}\ can calculate probabilistic confidence based on
user-specified confidence in evidence and using a variety of
propagation rules (e.g., the product or sum of doubts methods, or
those defined by the user) and can color nodes (e.g., red, amber,
green) according to user-selected thresholds to indicate the
confidence calculated for them, as illustrated in Figure
\ref{traffic}.  In addition to valuations of probabilistic confidence
calculated by propagation from evidence, {\sc Clarissa/asce}\ allows manual
adjustment to these values (as an informal version of the factors
$f$), both to increase (e.g., due to justification by a strong theory)
or reduce them (e.g., due to residual doubts).

\begin{figure}[t]
\vspace*{-4ex}
\begin{center}
\includegraphics[width=1.0\textwidth]{traffic.png}
\end{center}
\vspace*{-2ex}
\caption{\label{traffic}Portion of {\sc Clarissa/asce}\ Canvas Showing Probabilistic Valuations}
\vspace*{-2ex}
\end{figure}


We might wonder how it can be that the record shows modern aircraft,
say, to be safe and reliable when the calculations discussed here
deliver rather small estimates for probabilistic confidence in these
properties?  One response is that the conservative and generic
calculations considered here severely underestimate the true values
because they take no account of the particular kinds of system
concerned.  In general, these are highly redundant control systems.
As control systems, they sample sensors and inputs and drive actuators
and signals many times a second, and substantial state is stored in
the physical plant itself.  Thus, a ``small'' fault in a calculation
(i.e., one encountered very infrequently) will affect only one or a
few iterations of a controller (otherwise it would be a ``big'' fault
and we are confident these will be found and eliminated) and the
controller will correct the effects of these in the next few cycles,
just as it does for environmental disturbances.\footnote{Of course,
Murphy's Law ensures that some ``small'' defects can have major
consequences: for example, the in-flight upset to an Airbus A330
\cite{VHQPA}.}  In addition, the system will generally be heavily
redundant with a lot of voting and averaging: these are present to
tolerate major failures, but will often mask small defects, too.
Truly accurate assessment of probabilistic confidence would need to
consider these contextual and architectural factors.  

A second response is that the confidence assessments we apply to
individual argument steps \emph{a priori} severely underestimate those
that can be applied retrospectively based on \emph{a posteriori}
experience.



In the next section we present a method for deriving estimates for
long run safety (i.e., reliability with respect to critical failures)
on the basis of \emph{a priori} probabilistic confidence in the
absence of faults as delivered by an assurance case, plus limited
\emph{a posteriori} operational or test experience.  This method
employs Conservative Bayesian Inference (CBI) to derive posterior estimates
for safety from prior confidence in the absence of faults (or, in a
more detailed analysis, absence of ``large'' faults).  To generate
useful conclusions, these methods require the prior probabilistic
confidence to exceed 0.9.  We have seen that generic methods of
confidence propagation may struggle to achieve this and so we expect
the final determination that the assurance case is ``good enough'' to
justify adequate confidence will be a holistic human assessment, based
on a number of factors (such as are being developed throughout
Sections \ref{soundness}--\ref{residuals}), rather than a conservative
calculation of probabilistic confidence using the methods described in
this section.


\newpage
\section{From Confidence to Safety}
\label{cbi}

The top claim of an assurance case often asserts that the system has
some logical property (e.g., ``is safe''); implicitly, this implies
that the system has no faults that could jeopardize the property.  We
have explored methods for gaining and assessing confidence in such
claims, but how does that relate to the properties we really care
about, which are typically absence (or rarity) of critical failures?
In other words, how do we get from confidence in absence of faults to
rarity of failures?

In this section we present a theory called \emph{Conservative Bayesian
Inference} (CBI) that can accomplish this step.  We present it as a
separate theory, external to any assurance case argument, but we note
that it could be incorporated by extending an argument above
its existing top claim using a substitution block to take that
(logical) top claim to a new higher-level top claim concerning the
probability of critical failures over the life of the system.










Confidence in the case can be expressed as probabilistic confidence in
its top claim $P_{\!\mathit{conf}}(C^T).$  The top claim $C^T$ typically concerns
absence of faults or defects that could lead to a critical failure.
Let us abbreviate ``suffers a critical failure'' by simply ``fails''
and ``has a fault that could lead to a critical failure'' as
``faulty'' (with ``nonfaulty'' as its negation); these definitions are
consistent with standard usage \cite{Laprie:dependability}.  Then, by
the formula for total probability
\begin{eqnarray}
\lefteqn{P(\mbox{system fails [on a randomly selected
demand]})}\label{one}\\ & = & P(\mbox{system fails} \,|\, \mbox{system
nonfaulty}) \times P(\mbox{system nonfaulty})\nonumber\\ & & \mbox{} +
P(\mbox{system fails} \,|\, \mbox{system faulty}) \times
P(\mbox{system faulty}).\nonumber 
\end{eqnarray}

The first term in this sum is zero, because the system does not fail
if it is nonfaulty (as we have defined those terms).  We
let $P_{\mathit{fif}}$ be the probability that the system ``fails if faulty,'' we
have $P_{\!\mathit{conf}}(C^T)$ as the probability the system is nonfaulty (so that
$P(\mbox{system faulty}) = 1 -P_{\!\mathit{conf}}(C^T)$), and therefore its
probability of failure on demand, $P_\mathit{fd}$ is given by
\begin{equation}\label{two}
 P_\mathit{fd} = P_{\mathit{fif}} \times (1-P_{\!\mathit{conf}}(C^T)).
\end{equation}

Different industries make different assessments about the parameters
to (\ref{two}).  Early nuclear protection, for example, seemed to
presume the system \emph{is} faulty, so in effect it set $P_{\!\mathit{conf}}(C^T)$
to 0 and performed extensive random testing to substantiate
(typically) $P_{\mathit{fif}} < 10^{-3}.$  If those regulators had accepted that
modest amounts of assurance could deliver $P_{\!\mathit{conf}}(C^T) \geq 0.9,$ then by
(\ref{two}) the same probability of failure could be
achieved\footnote{We are cutting a lot of corners here: the full
treatment must distinguish \emph{aleatoric} from \emph{epistemic}
assessment and must justify that beliefs about the two parameters can
be separated;
\cite{Littlewood&Rushby:TSE12,Littlewood&Povyakalo13,Littlewood&Povyakalo13b,Littlewood-etal:RESS17}
give details.} with the much less costly testing required to validate
merely $P_{\mathit{fif}} < 10^{-2}.$

Dually, FAA AC 25.1309 \cite{10-9} and the corresponding European
regulations \cite{CS-25}  for aircraft certification indicate $P_\mathit{fd}
\leq 10^{-9}$ for catastrophic failure conditions and seem to presume
the system \emph{will} fail if it is faulty, so in effect they set $P_{\mathit{fif}} =
1.$  The whole burden for assurance then rests on the value assessed
for $P_{\!\mathit{conf}}(C^T)$---so that we need $P_{\!\mathit{conf}}(C^T) \geq 1 -10^{-9},$ which
is completely implausible.  In fact, there is no credible assignment
of values to the parameters of (\ref{two}) that delivers $P_\mathit{fd} \leq
10^{-9}$ per hour \cite{Butler&Finelli91}; an alternative model is
needed.

Rather than the figure of $10^{-9}$ per hour, which is intended only
as ``an aid to engineering judgment'' \cite{10-9}, let us look at the
fundamental requirement of these regulations: that a catastrophic
failure condition is ``not anticipated to occur during the entire
operational life of all airplanes of one type.''  Extending
(\ref{two}), the probability of surviving $n$ independent demands
without failure, denoted $P_\mathit{srv}(n),$ is given by
\begin{equation}\label{longrun}
P_\mathit{srv}(n) = P_{\!\mathit{conf}}(C^T) + (1-P_{\!\mathit{conf}}(C^T)) \times (1-P_{\mathit{fif}})^n.
\end{equation}


Demands can be interpreted as hours of operation, or flights, or some
other measure of exposure and, whichever is chosen, a suitably large
$n$ can represent ``the entire operational life of all airplanes of
one type.''  The notable feature of (\ref{longrun}) is that the first
term establishes a lower bound for $P_\mathit{srv}(n)$ that is independent of
$n.$  Thus, if assurance gives us the confidence to assess, say,
$P_{\!\mathit{conf}}(C^T) \geq 0.9$ (or whatever threshold is used to interpret
``not anticipated to occur'') then it seems we have sufficient
confidence to certify the aircraft as safe.

However, we can imagine using this procedure to provide assurance for
multiple airplane types; if $P_{\!\mathit{conf}}(C^T) = 0.9$ and we assure 10 types,
then we can expect that one of them will have faults.  In this case,
we need confidence that the system will not suffer a critical failure
despite the presence of faults, and this means we need to be sure that
the second term in (\ref{longrun}) will be well above zero even though
it decays exponentially.  This confidence could come from prior
failure-free operation (e.g., flight tests).  Calculating the overall
$P_\mathit{srv}(n)$ can then be posed as a problem in Bayesian inference: we
have assessed a value for $P_{\!\mathit{conf}}(C^T),$ have observed some number $r$
of failure-free demands, and want to predict the probability of seeing
$n-r$ future failure-free demands.  To do this, we need a prior
distribution for $P_{\mathit{fif}},$ which may be difficult to obtain and
difficult to justify for certification.  However, Strigini and
Povyakalo \cite{Strigini&Povyakalo13} show there is a distribution
(specifically, one in which $P_{\mathit{fif}}$ is concentrated in a probability
mass at some $q_n \in (0,1]$) that delivers \emph{provably worst-case}
predictions; hence, we can make predictions that are \emph{guaranteed} to be
conservative, given only $P_{\!\mathit{conf}}(C^T),$ $r,$ and $n.$  Using this
approach, which is known as Conservative Bayesian Inference (CBI),
Strigini and Povyakalo show that if $P_{\!\mathit{conf}}(C^T)$ is above $0.9,$ then
$P_\mathit{srv}(n)$ is well above this floor, provided $r > \frac{n}{10}.$

If we regard a complete flight as a demand, then ``the entire
operational life of all airplanes of one type'' might require $n$ to
be in the range $10^{8}$ to $10^{9}$ (e.g., as of 2019, the Airbus
A320 series had performed over 150 million flights
\cite{Boeing:accidents}).  Flight tests prior to certification might
provide only $r = 10^3,$ so it appears this is insufficient for
certification by the criterion above.  However, it can be argued that
when an airplane type is certified we do not require (and in fact
cannot feasibly obtain) sufficient evidence to predict failure-free
operation over the entire lifetime of the type; instead, we initially
require sufficient confidence only for, say, the first six months of
operation and the small number of aircraft that will be manufactured
and deployed in that period.  This will be a much smaller value of
$n,$ and our $P_{\!\mathit{conf}}(C^T)$ (from assurance) and our $r$ (from flight
tests) will be sufficient for confidence in its failure-free
operation.  Then we will need confidence in the next six months of
operation, with a larger fleet, (i.e., a larger $n$) but now have the
experience of the prior six months failure-free operation (i.e., a
larger $r$) and in this way we can ``bootstrap'' our way forward
\cite{Strigini-etal21:bootstapping}.

It remains to consider what happens if experience in operation does
reveal a fault (by manifesting a failure, hopefully not
catastrophic---indeed, there is an FAA requirement that no single
fault may cause a catastrophic failure condition).  Commercial
airplanes operate in a legal and ethical framework where all incidents
and accidents are promptly reported and dispassionately investigated.
The FAA issues Airworthiness Directives mandating workarounds or
corrections to detected faults; in extreme cases it may temporarily
ground the fleet (as it did for Boeing 787 battery problems in January
2013 and 737 MCAS faults in 2019\footnote{The fatal crashes caused by
design faults in the MCAS system of 737 Max aircraft may seem to
repudiate the safety and certification arguments made here.  However,
it is clear that Boeing was not following either the spirit or the
letter of established safety requirements and guidelines, and FAA
oversight was weak and possibly captured.  Thus, although this example
does not repudiate the methods described here, it does illustrate that
they cannot operate outside a genuine safety culture.}).  Bishop
\cite{Bishop13} constructs a statistical model for this scenario and
shows that, under plausible assumptions, detection and repair of
faults significantly increases long run safety, even if the fleet
continues to operate after a fault has been discovered, and even if
repairs may be imperfect.



In its totality, the analysis above (which is based on research at
Adelard and City University in London
\cite{Bishop13,Bertolino&Strigini98,Bloomfield96:t-of-n,Strigini&Povyakalo13,Strigini-etal21:bootstapping})
provides---for the first time, we believe---a plausible statistical
model that retrospectively explains the success of aircraft
certification, and other certification regimes based on similar
practices.  At the base of this analysis is an assessed confidence
(e.g., $P_{\!\mathit{conf}}(C^T) > 0.9$) that the system is nonfaulty or
``fault-free'' with respect to critical requirements.

Traditionally, software assurance cases have delivered a top claim
that the software is nonfaulty with respect to critical requirements.
Confidence in this claim was generally assessed separately (or left
implicit) but we suggest that the case should now be expanded to
include this attribute.  The connection from confidence in
nonfaultiness to reliability in operation was also assessed separately
(or left implicit as prior to CBI and other conservative approaches
\cite{Bishop&Bloomfield02:ISSRE} there was no good theory to account
for it) and we suggest that this, too, should now be made explicit and
included in an expanded assurance case whose top claim would now
become reliability with respect to critical failures.

There are other top claims, architectures, and methods of analysis
that function similarly to that described above.  A modification to
the analysis above replaces strict fault-freeness by \emph{quasi}
fault-freeness, meaning the system is either nonfaulty or is faulty
but with only a minuscule probability of failure
\cite{Littlewood-etal:RESS17}.  This is a more robust model and yields
attractive results \cite{Zhao-etal19:AVtests}, but the details are
more complicated.  Alternative properties to nonfaulty and
failure-free include mission risk, and the claim that a new system is
no worse than the old one.  And an alternative to external calculation
of probabilistic confidence in the case is internal justification of
probabilistic quantities such as these within the case itself (i.e.,
the claims in the case make probabilistic statements; recall section
\ref{probs}).  And as an alternative to single-threaded architectures,
Littlewood and Rushby \cite{Littlewood&Rushby:TSE12} provide a
rigorous analysis of ``monitored architectures'' in which a highly
trustworthy monitor checks the behavior of a less trusted primary
system as advocated, for example, by the F3269-17 standard for
unmanned aircraft \cite{F3269-17}.  Bishop and Bloomfield
\cite{Bloomfield96:t-of-n,Bishop&Bloomfield02:ISSRE} develop an
alternative worst-case analysis that predicts long term reliability
from an estimate of the number of faults $N$ at time of release (as
opposed to confidence in their absence) and the operating time $T$.
The predicted number of faults can be based on models of the software
development process, such as the empirically validated ``barrier''
model \cite{Bloomfield&Guerra-dsn02}.




This concludes our discussion on the positive view of assurance cases
and we now turn from these to negative perspectives and the important
role of doubts and defeaters.

\newpage
\section{Negative Perspectives: Doubts and Defeaters}
\label{defeaters}

In \ifelse{{\sc Clarissa}}{Assurance 2.0}, the criterion for a completed assurance case is that it should
be \emph{indefeasible}, meaning that all identified doubts have been
addressed, and we are confident no credible doubts remain that
could change the decision supported by the assurance case 
\cite{Rushby:Shonan16,Bloomfield&Rushby:Assurance2}.  When we say that
all doubts have been addressed, we do not require that they are
eliminated; in appropriate circumstances, some doubts may be accepted as
residual risks, as will be discussed in Section \ref{residuals}.  What
makes the case indefeasible is that we know about these doubts, have
examined them, and made a conscious decision about them so that no
credible information would make us change our decision.
Indefeasibility is lost when there may be doubts that we do not know
about, or doubts we do know about but have not consciously addressed.


Doubts are suspicions that some part of a case may be inadequate or
wrong.  On investigation, the location and nature of the doubt should
become sharpened so that it can be expressed as a \emph{defeater}:
that is, a node in the assurance case argument that challenges or
refutes the specific claims, arguments, or evidence represented by
other nodes.  There are several ways to address doubts and their
associated defeaters.  One way is to argue that the defeater is
unjustified or incorrect, so there will be a subcase that
\emph{defeats the defeater}.  If a doubt is legitimate, however, we
must adjust either the argument, or the system (and then possibly the
argument as well) to eliminate or mitigate its defeater(s).  A
defeater that requires adjustment to the system (as opposed to just
its assurance case) is more properly considered a \emph{hazard} than a
defeater, but the issues we are developing here will apply to these as
well.

Pollock \cite{Pollock87} was the first to examine defeasible arguments
of the kind that interest us, and he distinguished between
\emph{undercutting} and \emph{rebutting} defeaters.  Weinstock et al
\cite{Goodenough-etal:TR2014} later added \emph{undermining} defeaters
in an approach to assurance that they call \emph{eliminative
argumentation} (because one proceeds by eliminating doubts).
Generally speaking, an undercutting defeater challenges an argument
(i.e., its justification), a rebutting defeater challenges a claim,
and an undermining defeater challenges evidence.    However, when we
first explore a doubt we may not know exactly how it should be
manifested as a defeater.  For example, we may have doubts whether a
formal verification handles concurrency correctly, but until we
investigate further we may not know if the problem is in the claim,
the evidence, or the argument, or even in the mechanisms of the system
itself.  So the doubt may initially be represented in the case as a
generic defeater expressing concern and aimed at the relevant claim
and, as the investigation proceeds, it may become a specific defeater
(i.e., one that makes its own claim) supported by its own subcase and
targeted more precisely at one element of the case.   Because their
role evolves, \ifelse{{\sc Clarissa}}{Assurance 2.0}\ is somewhat relaxed about the representation of
defeaters and the constraints applied to them (see the discussion
around Figure \ref{decomp-doubts}).  For example, we
usually represent a defeater by a node having the same shape as a
claim, but we allow it to point to another claim with no intervening
argument block.  Dually, it may point to an argument block without
being referenced in the justification for that block.  In these ways,
a defeater operates rather like a comment; on the other hand, it can
also be interpreted as a (counter)claim and be justified by its own
subcase as will be outlined in Section \ref{countercases}.

Investigation and resolution of doubts and defeaters serves two
purposes: firstly, it is the primary means by which we avoid
confirmation bias and drive the case toward soundness and
indefeasibility; secondly, it helps reviewers comprehend the case as
they find their own doubts have been anticipated and answered.  For
the first of these, it is enough just to deal with the doubts and move
on, but for the second it is necessary to record the changes made and
to support some kind of \emph{dialectical} examination that allows
reviewers to see how the case responded to previously considered
doubts.  This raises significant issues in the representation of an
assurance case.

For example, one step in a case may decompose a claim into subclaims
over some enumeration and we may doubt that this is done
correctly, so we establish a defeater that attacks the decomposition
step (e.g., by making the claim that the decomposition is incomplete).
We may then develop a subcase that refutes this claim.  But that
subcase may include an element that is itself challenged by another
defeater, and that is defeated by a further subcase, and so on.  One
issue is how to represent and evaluate assurance cases in the presence
of defeaters and their subcases.  We have the basic case that is
attempting to substantiate some positive claim, then defeaters
(negative claims) and subcases to substantiate them, and then further
counter-defeaters and their subcases.  Do we show all of these layers
of defeat and counter-defeat?  And do we have some way of showing
which subcases are contributing to the basic case and which to a
defeater or counter-defeater or counter-counter-defeater?  We will
refer to this as the problem of representing \emph{defeasible
arguments} and will briefly examine it in Sections \ref{defeasible}
through \ref{elimarg}.

When we have satisfied ourselves that a defeater is itself defeated,
the investigation has served its purpose and we could eliminate
everything associated with it because the original case was valid
after all.  But reviewers may have the same doubts, and so for them it
is desirable to retain the defeaters and their subcases in a way that
permits interactive replay and exploration.  We will refer to this as
the problem of representing \emph{dialectical arguments} and will
examine it in Section \ref{dialectics}.

The problem of representing dialectical arguments becomes more
complex when the original case, or system, or both, need to be
adjusted in response to a defeater.  Whereas the subcase for an
unsuccessful defeater and the subcases for its counter-defeaters and
so on can be seen as decorations to the basic, sound, case, a
successful defeater requires a change to the original case and so we
might need to retain the original case and its defeaters and then
branch to the adjusted case.

An important special case is that of missing assumptions.  Slavoj
{\v{Z}}i{\v{z}}ek \cite{Vzivzek06} identified the ``unknown knowns,''
the ``silent presuppositions we are not aware of,'' as a significant
source of error in all human deliberation.  In an assurance case, a
defeater that identifies a missing assumption may be defeated by
supplying the required assumption and, possibly, a subcase with
evidence, to justify it.  This amendment to the case is an addition
rather than a change and its representation and management can be
simpler than those for more general amendments in response to
defeaters.







\subsection[Defeaters in Reasoning, Argumentation, and Dialectics]{Defeaters in Reasoning, Argumentation, and Dialectics}
\label{theory}

Classical formal logic cannot tolerate contradictions among premises:
these render the argument invalid.  But in AI and in the study of
human and commonsense reasoning it is reasonable to draw conclusions
on the basis of incomplete and inconsistent information, and to revise
these as new information becomes available.  Consider, for example, an
emergency room physician, updating her diagnosis and adjusting her
treatment plan as new observations and test results become available.

In AI, the topic of drawing reasonable conclusions from incomplete,
inconsistent, and changing information is referred to as ``defeasible
reasoning''; much the same topic is considered in formal logic as
``nonmonotonic logic'' (``nonmonotonic'' because conclusions are not
stable and may need to be withdrawn as more knowledge is acquired).  A
standard example has premises ``birds can fly'' and ``Tweety is a
bird'' but then we learn that, contrary to the obvious conclusion,
Tweety cannot fly.  It turns out that Tweety is a penguin and the
first premise needs to be modified to ``most birds can fly.''  A
different, though related, application arises in the study of
``argumentation'': here, different parties have different views and
may advance premises that contradict each other.

We briefly examine defeasible argumentation seeking ideas that might prove
useful for our application.  We look first at methods for defeasible
reasoning, followed by argumentation theory, eliminative
argumentation, and dialectics.

\subsubsection{Defeasible Reasoning}
\label{defeasible}

The crucial notion of \emph{defeater} is from Pollock in
1987 \cite{Pollock87} (although he published on these topics as early
as 1967) where he proposed what is known as an epistemological
approach to evaluation of defeasible arguments.  This is a set of
rules that defines how a cognitively ideal agent would arrive at
warranted conclusions given a set of premises and their defeaters.
Pollock's system has been criticized for lacking a ``normative
standard,'' being based on ad hoc intuitions about how a reasonable
agent would respond to this or that cognitive situation, but Koons
\cite{sep-defeasible-resoning} observes that the same criticism can be
lodged against several other theories of defeasible reasoning.  




Theories for nonmonotonic logic do have more justified foundations,
starting with McCarthy's \emph{circumscription} \cite{McCarthy80}
which, roughly speaking, prefers the most specific applicable
premises.  However, this approach gives intuitively incorrect answers
in some cases, epitomized by the ``Yale Shooting Problem''
\cite{Hanks&McDermott87} and so, as with defeasible reasoning,
there is a large literature of attempts to find more satisfactory
treatments.


The goal of defeasible reasoning and of nonmonotonic logic is to work
out what can be concluded when there are contradictory premises or
when premises can change (e.g., in the Yale Shooting Problem, the gun
is initially unloaded but later becomes loaded).  However, these are
not really relevant for assurance cases.  In Assurance 2.0 we use
Natural Language Deductivism (NLD) and expect completed assurance
cases to be deductively sound, although we may tolerate some
``inductive'' argument steps\exfootnote{In an inductive argument step,
the subclaims and evidence ``strongly suggest'' the parent claim but
do not imply or entail it as a deductive step would.  We discourage
inductive steps because there is always a defeater hidden in the
``gap'' that prevents the step being deductive.  In our opinion, it is
preferable to acknowledge this ``gap'' by supplying an explicit
``something missing here'' subclaim that makes the argument step
deductive.  This subclaim is never discharged, so it highlights and
documents a residual risk.}  if necessary.  That is, we may accept
some ``gaps'' in our knowledge, but not contradictions or changes.

While developing a case, and in supporting its review, we use
defeaters (i.e., contradictions) to probe and challenge a case, but we
do not expect to conclude anything from a case with unresolved
defeaters: such a case is acknowledged as imperfect and incomplete.
What we would like to know is: how much of the overall argument does a
defeater cast into doubt, and how much is repaired by a
counter-defeater?  Unfortunately, these purposes are not served by
defeasible reasoning and so we next turn to argumentation theory.


\subsubsection{Argumentation Theory}
\label{argtheory}

Defeasible reasoning and nonmonotonic logic attempt to understand
what conclusions can be drawn from a single argument when some of its
premises are inconsistent.  The field of argumentation on the other
hand, considers multiple competing arguments and tries to deduce which
ones emerge from the competition with their plausibility intact.
Defeasible reasoning employs a defeater relation on premises, whereas
argumentation has the relation of \emph{attack} between arguments.
The two ideas are related however.  If we have an argument and then
introduce a defeater, we can think of this as two arguments: the
original, and a new one consisting of that plus the defeater, and in
which the second attacks the first.

This is \emph{abstract argumentation} theory, introduced by Dung
\cite{Dung95:AIJ} in a paper that has over 4,500 citations.  Despite
the term ``argumentation'' appearing in the name, the level of
abstraction reduces it to an exercise on graphs: arguments are nodes
in a graph that are connected by attack relations and we ask for rules
to determine which sets of nodes are ``accepted.''  Dung defined this
in terms of ``extensions'' but ``labeling'' provides a more intuitive
treatment \cite{Caminada06}: each argument in the graph is labeled
\emph{in} (accepted), \emph{out} (rejected) or \emph{undecided}.  The
\emph{reinstatement} rule on labeling stipulates: an argument is
\emph{in} iff all arguments that attack it are \emph{out}; an argument
is \emph{out} iff it is attacked by at least one argument that is
\emph{in}; arguments that are neither \emph{in} nor \emph{out} are
\emph{undecided}.

As with defeasible reasoning, the purposes served by abstract
argumentation theory are sufficiently different from those in
assurance cases that we do not find any direct application for its
methods.

However, argumentation theory has a connection to logic programming
that supports a computational interpretation for defeasible reasoning
\cite{Chesnevar-etal00} and this may suggest methods for applying
Answer Set Programming (ASP) \cite{Gelfond&Kahl14} that are being
explored \ifelse{by UT Dallas as part of}{in} {\sc Clarissa}.

\subsubsection{Eliminative Argumentation}

\label{elimarg}

``Eliminative Induction'' is a method of reasoning that dates back to
Francis Bacon who, in 1620 \cite{Bacon-organon}, proposed it as a way to
establish a scientific theory by refuting all the reasons why it might
be false (i.e., its defeaters).  Modern treatments see falsifiability
as the key characteristic of science \cite{Popper:2014logic} but the
two can be related via Bayesian Epistemology \cite{Bovens&Hartmann03},
where Bayesian methods are seen as the best way to select among so-far
unfalsified theories \cite{Hawthorne93,Vineberg96}.  These Bayesian
methods relate to Confirmation Theory, discussed in Section
\ref{confirmation}.

Weinstock, Goodenough, and Klein \cite{Goodenough-etal:ICSE2013}
develop the idea of Eliminative Induction as a means of assurance they
call \emph{Eliminative Argumentation}.  An argument is presented as a
\emph{confidence map}, which is rather like an assurance case with
defeaters included and rules for accepting a claim only if all its
defeaters have been eliminated.  Colors are used to highlight the
``positive'' and ``negative' parts of a case.  Diemert and Joyce
report successful application of eliminative argumentation in
assurance of real systems \cite{Diemert&Joyce2020}.  We apply some of
these ideas in \ifelse{{\sc Clarissa}}{Assurance 2.0}, as described in Section \ref{defeaters-in-cl}.

\subsubsection{Dialectics and Agreement Technologies}
\label{dialectics}

Dialectics refers to the back-and-forth nature of arguments employed
in active debate.  One of the goals of dialectical debate is to reach
an agreed conclusion, so its methods are sometimes referred to as
agreement technologies \cite{Ossowski13}.  

There are many approaches to dialectics and agreement, but an
influential one that has been applied in several domains and is
supported by tools is framed in terms of \emph{argument schemes}
\cite{Walton96,Walton-etal08}.  These are outlines for many canonical
kinds of argument: for example, argument from analogy, argument from
expert opinion, and so on (there are about 30 in Walton's book
\cite{Walton96}).  These are supported by \emph{critical questions},
which can be thought of as defeaters customized to each specific
frame.  For example, argument from expert opinion has six critical
questions (e.g., ``how credible is E as an expert source?'').  Raising
and responding to critical questions gives rise to the dialectical
element, just as it does in an assurance case challenged by defeaters.

Despite this apparent similarity, the compendium on agreement
technologies \cite{Ossowski13} contains no reference to assurance or
safety cases.  Nor do more than 1,000 articles available online that
were published in the journal \emph{Argumentation} (Springer).
Assurance and safety cases likewise make no reference to agreement
technologies.  An exception is the work of Yuan and Kelly, who have
applied argument schemes and critical questions to assurance
\cite{Yuan&Kelly11,Yuan&Kelly15}.

\emph{Carneades} \cite{Gordon-etal:Carneades07} is a system that
supports dialectical reasoning in a different way, allowing a
subargument to be \emph{pro} or \emph{con} its conclusion and allowing
weights to be attached to premises.  A \emph{proof standard} is
calculated by ``adding up'' the \emph{pro}s and \emph{con}s supporting
the conclusion and their attendant weights (rather like the labelings
of argumentation theory).  For example, a claim is ``in'' if it is not
the target of a \emph{con} that is itself ``in'' (unless it is also
the target of an ``in'' \emph{pro} \ldots); a conclusion is supported
to the \emph{preponderance of evidence} proof standard if it has at
least one \emph{pro} argument that is ``in'' and weighs more than any
``in'' \emph{con} argument.  The system, which is available at
\url{http://carneades.github.io/}, provides several kinds of argument
graphs for visualizing arguments.  Recent work by Takai and Kido
\cite{Takai&Kido14} builds on these ideas and is implemented in the
commercial tool Astah GSN \cite{Astah-gsn}.


\subsection[Approach Adopted in {\sc Clarissa}]{Approach Adopted in C{\small LARISSA}}
\label{defeaters-in-cl}

We have briefly reviewed how defeaters are used and represented in
defeasible reasoning, argumentation theory, eliminative argumentation,
and in dialectics and agreement technologies.  The crucial notion of
``defeater'' comes from defeasible reasoning, but we did not find much
else in that field that is relevant to our concerns, since we require
inconsistencies (i.e., defeaters) to be resolved rather than to reason
in their presence.  Argumentation theory has the same defect, but
provides the useful notion of an argument being \emph{in} or
\emph{out} and argumentation schemes and dialectics apply this to
subarguments and provide tool support in the Carneades framework;
this idea is applied to assurance cases in Astah GSN\@.
Eliminative argumentation uses several of these ideas and strongly
advocates that the search for and elimination of defeaters should be a
key element in assurance.  We build on these latter elements in the
{\sc Clarissa/asce}\ platform.

 As described earlier, there are three ways in which defeaters can
affect the development of a case.
\begin{enumerate}

\item The defeater is itself defeated by a counterargument, and this
can proceed to arbitrary depth.  We represent this by a refutational
subcase (see Section \ref{countercases}) with additional nodes that
can be revealed or hidden and are color coded to represent \emph{in}
and \emph{out} (i.e., active vs.\ defeated) status.  The desired end
state is that defeaters pointing to elements of the main case are all
\emph{out} (and are hidden by default).

\item The defeater is sustained (possibly by a supporting subcase)
and requires adjustment to the existing case, which can take two forms.
\begin{enumerate}

\item The defeater identifies a missing assumption (an ``unknown
known'') and the response is to add this assumption to the argument as
a new claim, which may have a supporting subcase.  We represent this
in a similar way as the first case: that is, the additional claim and
subcase can be revealed or not, but here the desired end state is that
the defeater is \emph{out} and the subcase is revealed.

\item The defeater identifies a flaw in the argument and/or the system
(in which case it is a hazard).  The {\sc Clarissa/asce}\ canvas can record
multiple snapshots of a case and we use this to capture the ``before
and after'' versions of the case, with the optional display of
defeaters and their subcases providing additional opportunities for
dialectical examination.  The default case is that defeaters are
\emph{in} and revealed in the ``before'' version, and \emph{out} and
hidden in the ``after'' version.

\end{enumerate}

\end{enumerate}

The desired conclusion to the development of an assurance case is that
all defeaters are resolved (i.e., \emph{out}), so that only a positive
case remains, although this may contain residual doubts (see Section
\ref{residuals}).  

During development, active defeaters may be present and it can be
useful to see how much of the case is thereby called into question.
We believe there are two useful views.  One is to ignore defeaters and
evaluate soundness, full validity, and probabilistic confidence as if
they were not present.  This enables assessment of the state of the
basic case, apart from defeaters.  The other is to mark (e.g., by color
coding) those defeaters that are \emph{in} and the ordinary nodes that
are \emph{out} as a result.  This allows the impact of active
defeaters to be assessed.  {\sc Clarissa/asce}\ mechanizes both views using manual
overrides on the propagation of probabilistic confidence: confidence
in a defeated claim can be left unchanged for the first view, and set
to zero (or reduced from its prior value) for the second; nodes are
color coded according to user-selected thresholds on probabilistic
confidence.  The purpose of these manipulations is not to assess
justifiable confidence in a case, but to provide visualizations that
help focus developers' attention on the weakest areas and the scope of
their impacts (recall Figure \ref{traffic}).






In addition to defeaters, there are several other reasons why an
assurance case may be considered imperfect or unfinished.  These
include minor errors (e.g., misspellings), non deductiveness, logical
invalidity, unsoundness, and undeveloped subcases.  Figure
\ref{process} suggests a process to examine and incrementally remove
these defects.  The {\sc Clarissa/asce}\ platform provides ways to assess these
different flaws and to annotate the case, some automatically and some
by hand, but most of them can also be indicated by use of defeaters,
as described earlier, and we prefer this method as it can be more
informative and precise, and also allows more uniform assessment.

We consider its facilities for the dialectical examination of
defeaters and other imperfections to be the main support for
assessment of negative perspectives in the {\sc Clarissa/asce}\ platform.  In
particular, the narrative associated with each defeater node can
record the origins of the defeater and whether and how it has been
addressed: for example, it might have been considered out of scope
and no action taken, it might have led to a claim being modified to
include an extra assumption, or it might have led to significant
changes to the case with new nodes added to the case.  {\sc Clarissa/asce}\ also
provides statistical summaries on its ``Dashboard.''  These can
include, for example, number of defeaters proposed and examined during
development (as an indication of developer diligence) and during
assessment (as an indication of assessor diligence).

\subsection{Counterarguments and Refutations}
\label{countercases}

The intended end state in development of an assurance case is a fully
valid and sound argument whose defeaters have all themselves been
defeated or mitigated.  The defeaters, therefore, serve only a
transient purpose and we could decide that there is no need to define
an interpretation for arguments with defeaters as these will not be
present in the finished case; in this view defeaters function rather
like specialized comments and seldom need to be supported by their own
subcase: the reasons for accepting or rejecting them can be recorded
in the narrative associated with the defeater.

However, there are circumstances in which it is appropriate for a
defeater to be supported or refuted by a subcase.  An example is
where different parties do not agree on the validity of a given
defeater: e.g., the evaluators of a case propose a defeater and are
not convinced by the developer's informal arguments against it, so
each party develops a subcase to advance its point of view.

This introduces the notion of a \emph{counterargument}, which can be
useful in circumstances quite apart from contested defeaters.  One
such is where developers of an assurance case find it difficult to
build a subcase to justify some claim $A$: they may be able to develop
their understanding or to gain insight by attempting instead to
justify the \emph{counterclaim} $\neg A$, or by attempting to
\emph{refute} the claim $A$.  Another is where the developers of a
large case are unpersuaded by the subcase for a claim supplied by
others; again, it may be useful to develop the case for a counterclaim
or refutation to the given claim.


Counterarguments can take two forms: positive or refutational.  A
positive counterargument aims to establish a counterclaim $\neg A$ in
the standard way, whereas a refutational counterargument aims to
refute the original claim $A$.

Counterclaims and refutations are equivalent in classical logic: that
is to say, verifying $\neg A$ is the same as refuting $A$.  However,
this may not be so straightforward in an assurance argument.  One
reason is philosophical: in an assurance case we generally prefer a
positive argument to a refutational one: that is, we prefer to
establish that the system is safe, rather than it is not unsafe
(eliminative argumentation would take the contrary position).  In
logic, this preference for positive arguments corresponds to use of
\emph{intuitionistic} rather than classical reasoning: intuitionistic
logic eschews the axiom for ``excluded middle'' (i.e., $A \vee \neg
A$) so that all proofs must be of a positive, constructive nature.  It
might seem that this would be a good choice for assurance case
arguments, but there difficulties in doing so.  The interior steps of
an assurance argument are axioms, and in an intuitionistic setting we
must be careful that these do not accidentally introduce the excluded
middle.  For example, most assurance cases have essential steps that
decompose over hazards and since we cannot \emph{know} that all
hazards have been identified (although we try very hard to do so),
these steps have a somewhat non-intuitionistic character: instead of
arguing that the system is safe in all circumstances, we are saying
that we know of no circumstances where it is unsafe.

In general, it seems very onerous to insist and to check that all
argument steps are intuitionistic (it is hard enough to insist that
they are deductive) so we suggest it is best to conduct assurance
arguments within classical logic, but with an informal preference for
positive perspectives.

A second way in which counterclaims and refutations differ in
assurance cases is that assurance arguments use a very limited logic:
all argument steps reduce to a parent claim implied by a conjunction
of subclaims or evidence (these structures are called definite clauses).
Claims may involve negation, which is how we state a counterclaim, but
there is no argument step that performs negation and so it is not
possible to invoke a refutational setting.

 To overcome this limitation, {\sc Clarissa/asce}\ will allow a counterargument to
be explicitly marked as refutational.  The negative nature of
refutational counterarguments will invert aspects of their
interpretation.  For example, in a positive counterargument, the
conjunction of subclaims should entail the parent counterclaim but, in
a refutational counterargument any one subclaim is sufficient to
refute the parent, so a \emph{disjunction} is the appropriate
interpretation.  Similarly, the \emph{absence} of evidence can serve
to refute a claim.

We are still exploring how tool support for positive and refutational
counterarguments should be handled in {\sc Clarissa/asce}.






\newpage
\section{Residual Doubts and Risks}
\label{residuals}

A sound assurance case delivers confidence in its top claim.
Typically, this is either an internal probabilistic assessment (recall
Section \ref{probs}) of some property related to critical failure
(e.g., failure rate or time to failure), or a logical claim asserting that the
system has no faults that could lead to a critical failure.  In the
latter case, the degree of confidence in the claim can support a
conclusion concerning rate of critical failure (see Section
\ref{cbi}).  Thus, in either case, we derive strong confidence in the
related claims that the system contains no critical faults and that it
will suffer few critical failures.

However, the assurance case may contain residual doubts: these are
potential defeaters that we are unable to eliminate or mitigate.  They
may be due to uncertainty in the environment: for example, the system
is designed to withstand two faults and evidence indicates this is
sufficient, but it is always possible for it to encounter more than
that.  Or they may be due to limitations of human review (e.g., human
requirements tracing cannot be guaranteed to be free of error), or of
automated analysis (e.g., automated static analysis may be unable to
discharge some proof obligations, leading to alarms that may be false
and must be reviewed by humans).  If true, these defeaters may expose
a hazard and hence a fault.

In assessing soundness and probabilistic confidence in an assurance
case, we ignore residual doubts (recall Sections \ref{soundness},
\ref{propagation} and \ref{defeaters-in-cl}): thus we achieve
confidence in the absence of faults by ignoring the remaining doubts
and defeaters that could possibly expose their existence!  The
justification for doing this is that we assess the likelihood of such
faults, or more particularly the risk that they pose (i.e., the
likelihood of activating them multiplied by the potential cost of the
failure they may incur) to be insignificant.

Let us first consider the kinds and significance of residual doubts
that may be present.  Our concern is that these doubts may be
sufficient to undermine the indefeasible justification of the claim
$C$, so that we have to consider the possibility that $C$ is false and
$\neg C$ is true.  The probability of this event can be conditioned on
whether or not the argument supporting $C$ is deductive or not.  Thus,
\begin{eqnarray*}
P(\neg C) & = &
 P(\neg C\,|\, \mbox{deductive}) \times P(\mbox{deductive})\\
&& \mbox{}+ P(\neg C\,|\, \neg \mbox{deductive}) \times P(\neg \mbox{deductive}).
\end{eqnarray*}
It is conservative to set any term in this equation to 1.  Hence
\begin{eqnarray}
P(\neg C) & \leq &
P(\neg C\,|\, \mbox{deductive}) \times 1
\mbox{}+ 1 \times P(\neg \mbox{deductive})\nonumber\\
& \leq & P(\neg C\,|\, \mbox{deductive}) + P(\neg \mbox{deductive}).\label{ded}
\end{eqnarray}

If we have correctly identified all residual doubts to the argument,
then $P(\neg \mbox{deductive})$ will be the cumulative probability of
those doubts that concern deductiveness (e.g., the unsupported
``something missing here'' claims), which we can write as
$P(\mbox{deductiveness doubts}).$

That takes care of the second term in the right hand side of
(\ref{ded}), so we now consider the first term.  We can condition this
on whether the deductive argument supporting $C$ is valid or not.
\begin{eqnarray*}
P(\neg C\,|\, \mbox{deductive}) & = &
P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid}) 
\times P(\mbox{deductive} \wedge \mbox{valid})\\
&&\mbox{} +
P(\neg C\,|\, \mbox{deductive} \wedge \neg \mbox{valid}) 
\times P(\mbox{deductive} \wedge \neg \mbox{valid}).
\end{eqnarray*}
Again, It is conservative to set any term in the equation to 1.
Furthermore, validity of the argument can be assured mechanically (in
\ifelse{{\sc Clarissa}}{Assurance 2.0}\ it is assured by construction), so we assume any invalid argument
has already been rejected; hence $P(\mbox{deductive} \wedge \neg
\mbox{valid}) = 0.$ Thus
\begin{eqnarray}
P(\neg C\,|\, \mbox{deductive}) & \leq &
P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid}) 
\times 1 + 1 \times 0\nonumber\\
& \leq &
P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid}). \label{valid}
\end{eqnarray}

\label{resinterior}


Finally, we consider (\ref{valid}) and condition
this on whether the deductively valid argument is sound or not.
\begin{eqnarray*}
\lefteqn{P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid})=}\\
&\lefteqn{P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid}
    \wedge\mbox {sound})
\times
P(\mbox{deductive} \wedge \mbox{valid} \wedge\mbox {sound})}\\
&&\mbox{}+
P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid}
    \wedge \neg \mbox {sound})
\times
P(\mbox{deductive} \wedge \mbox{valid} \wedge \neg \mbox {sound}).
\end{eqnarray*}
If the argument is deductive and valid and sound, then $C$ is true and
$\neg C$ is false.  Hence, the first term on the right hand side is 0
and then, again setting some terms conservatively to 1, we have
\begin{eqnarray}
P(\neg C\,|\, \mbox{deductive} \wedge \mbox{valid})& \leq &
0 \times 1 + 1
\times
P(\mbox{deductive} \wedge \mbox{valid} \wedge \neg \mbox {sound})\nonumber\\
& \leq & P(\mbox{deductive} \wedge \mbox{valid} \wedge \neg \mbox {sound}).\label{sound}
\end{eqnarray}
Now, $P(\mbox{deductive} \wedge \mbox{valid} \wedge \neg \mbox
{sound})$ will be the probability of all residual doubts concerning
soundness of the argument, which we can partition into those
concerning the evidence incorporation steps, which we write as
$P(\mbox{evidential doubts}),$ and those concerning the interior
reasoning steps of the argument, which we denote $P(\mbox{interior
doubts}).$ Thus combining (\ref{ded}) to (\ref{sound}),
we have
\begin{eqnarray}
\lefteqn{P(\neg C) \leq }\nonumber\\
& P(\mbox{deductiveness doubts})
+P(\mbox{evidential doubts})
+P(\mbox{interior doubts}).\label{doubts}
\end{eqnarray}


We have already described deductiveness doubts; an example would be
the case that more than two faults afflict a system that is designed
to withstand only two faults.  Presumably the argument will contain a
decomposition step on the number and nature of faults, and this will
not be deductive unless the ``impossible'' case of more than two
faults is taken into account.

Evidential doubts are an interesting topic.  We devote considerable
attention to the assessment of evidence (recall Sections
\ref{confirmation} and \ref{evincsec}) so any doubts are
surely already included in those assessments.  However, it may be that
we have systematic doubts about certain types of evidence: for
example, static analysis may generate ``false alarms'' that must be
rejected by human review.  We could reduce our probabilistic
assessment $P(C \,|\, E)$ for claims $C$ supported by such evidence
$E$ due to doubts engendered by false alarms---but presumably this
reduction will be minor, or we would do something about it.  But then
concern about false alarms risks being lost in the details and the
cumulative impact of these doubts may not be recognized.  Thus, we
think there may be some merit in recording small systematic concerns
about evidence as residual evidential doubts.

Interior doubts can arise for two reasons.  One is that the
justification for a reasoning step may be unconvincing; the other is
that we may suspect that the step could be \emph{wrong}.  In the first
case, we accept that the subclaims entail the parent claim but are
dissatisfied with the justification provided; in the second, we have
doubts that the subclaims really do entail the parent claim (and
therefore distrust the justification also).  The latter case may have
serious consequences: if accepted, its correction may require a change
to the argument step, which may propagate to additional changes in
other nearby steps.  Hence, we suggest that interior doubts of this
kind cannot be considered merely ``residual'': they should be
investigated and eliminated.

With these caveats, (\ref{doubts}) provides a classification of the
residual doubts that should be investigated in validation of an
assurance case.  We do not need precise assessments of their
likelihood of occurrence, merely a sufficiently good estimate to
determine if it is significant or not.  We earlier, at the end of
Section \ref{sub-conc} and in Section \ref{defeaters-in-cl}, described
how {\sc Clarissa/asce}\ allows manual adjustment to the accumulated probabilistic
confidence at selected nodes and color-coding of nodes according to
user-selected thresholds on these values.  We attach little
significance to the actual values, but the visualization can help
comprehend and assess the potential impact of residual doubts (again,
recall Figure \ref{traffic}).  Assessment of their significance might
be refined by taking into account the potential consequences of
failures that could arise if the doubt were to be realized: that is,
the \emph{risk} (product of likelihood and consequences) posed by each
residual doubt.  Initially, we suggest that these risks, and the
threshold where they are considered significant, should be assessed
and documented by best-efforts expert review.  Later, we hope to
develop ways of using historical experience and conservative
probabilistic modeling to assist this process.

It may not be necessary to assess each residual risk individually, nor
to strive for exactness: all we need to know is that the risk is well
below some acceptable threshold.  We suggest it is useful to categorize
residual risks into three (plus 1) levels.
\begin{description}

\item[Significant:] an individual residual doubt poses a risk that is
    above the threshold for concern.  In this case, the issue cannot
    be considered a merely ``residual'' risk, but must treated as a
    defeater and later eliminated or mitigated.

\item[Minor:] an individual residual doubt poses a risk that is below
    the threshold for concern, but it is possible that many such might
    cumulatively exceed the threshold.  These risks may need to be
    managed explicitly.

\item[Negligible:] multiple residual doubts of a similar kind
    collectively pose a risk that is below the threshold for concern.
    This case may arise when the source of doubt occurs many times but
    is adjudged to be trivial.  An example might be static analysis,
    where we use human review to evaluate proof obligations that the
    automation cannot decide.


\end{description}

 {\sc Clarissa/asce}\ allows unmitigated defeaters to be annotated with their
estimated severity, based on the scale above (4 = significant, 3 =
minor, 2 = negligible, 1 = default---indicating severity not yet
determined), and can report on the totals in each category.  Those
judged significant must be eliminated or mitigated.  Those judged
minor should be monitored and their cumulative impact should be
assessed.  If the number and cumulative severity of some category of
minor risks can be kept below the threshold of concern, then we
consider that category to be \textbf{Manageable}.  At final
assessment, the only residual doubts that remain should be those
considered minor and manageable and those considered negligible.

Ideally, assessment of residual doubts should consider the faults they
might precipitate, the failures those faults might cause, together
with the frequency of their occurrence and severity of their outcomes
(i.e., their risk), all in the worst case.  This is feasible for some
doubts, such as those concerning the maximum number of sensor failures
that might occur.  For others it seems less so.  Suppose for example,
that we have residual doubts about static analysis because it
generates many proof obligations that cannot be discharged
automatically and require human review.  Here, the best we can do
might be to collect statistics on human reliability for this task in
an effort to constrain the potential frequency of failure, since the
potential consequences seem very hard to ascertain.  If we assume the
worst case, that all human reviews are in error and these cases
represent real bugs, then each bug might be encountered very rarely,
but collectively they could arise unacceptably often.  This would be
an example where each residual risk is minor but their aggregate is
not manageable, and action must therefore be taken to eliminate or
further mitigate their cumulative impact (for example, by using a
better theorem prover or diverse means of analysis) so that it can be
assigned to the manageable or negligible categories.\footnote{Observe
that autonomous systems, such as self-driving cars, can exhibit this
behavior, but for different reasons.  For example, the vision system
of the car may misinterpret some scenes; each reason for
misinterpretation may apply very rarely, but in total they cause the
vision system to fail quite often, suggesting a minor but unmanaged
residual doubt.  On the other hand, misinterpretations may have little
consequence if they are localized, for the preceding and following
frames will be interpreted correctly and the misinterpreted frame will
be but a negligible ``blip'' \cite{Jha-etal:Safecomp20}.}




\newpage
\section{Sentencing Statement}
\label{sentencing}

Assurance cases generally serve a single purpose: to support the
decision whether a system may be deployed.  However, they may be
evaluated by reviewers occupying different roles within the
processes leading up to that decision.  For example, an auditor might
be focused on process and regulatory compliance in the construction
of the system and its assurance case, whereas a technical evaluator
will want to gain a deep understanding of how the system works and how
its safety is ensured.  It is important that an assurance case and its
supporting tools provide information and means for comprehending it
that support these diverse viewpoints.  

Graydon contends \cite{Graydon17:visions} that cases developed to
support one perspective or ``vision'' may be misunderstood by those
with different viewpoints.  We are not so pessimistic but we believe
that assurance cases and their tools must support communication, so
that diverse reviewers can develop confidence and consensus in their
understanding of the system and its case, and reasoning, so that they
can test their understanding and can also challenge the case.  We have
described several mechanisms by which Assurance 2.0 and {\sc Clarissa/asce}\ hope
to achieve these goals.  These include a limited number of basic
building blocks so that arguments are readily interpreted, strict
criteria on what constitutes a soundly reasoned argument step or
evidence of adequate weight, tools for inspecting and navigating
arguments and for evaluating them from both logical and probabilistic
perspectives, and methods and tools for challenging them by means of
defeaters.

The final assessment of an assurance case and the corresponding
decision on system deployment are serious matters; assessors cannot
merely sample the case with its claims, argument, and evidence and
then ``sign off'' on the top level claim.  We expect them, assisted by
those in supporting roles, to avail themselves of the tools and
intellectual structures mentioned above to actively explore both the
positive and negative aspects of the case and to challenge their
understanding by proposing defeaters and exploring other questions.

The evaluators' task should be informed by and conclude with a
``sentencing statement'' that indicates their diligent execution of
these tasks and declares their understanding of the system and its
context, the key points of its architecture and design, its hazards
and their mitigations, the soundness and probabilistic confidence of
the assurance argument with its supporting theories, models, and
evidence assembly, and the relationship of the top claim to acceptance
criteria for deployment.

Possible headings for a sentencing statement could be the
    following.\\[2ex] ``\emph{On the basis of this assurance case and
    an examination of other relevant documentation, I judge the
    proposed system to be adequately safe/unsafe}\ldots'' (or
    ``\emph{the case is insufficient to make a judgment}'').\\[2ex]
``\emph{I believe my judgment of this case is sound and valid
because}\ldots
\emph{\begin{itemize}
\item I understand the context and criticality of the decision\ldots
\item I understand the system\ldots
\item I find a clear thread of reasoning from evidence to claim\ldots
\item The evidence provided is sufficient/insufficient to support evidence-based
decision making\ldots
\item I have actively explored doubts\ldots
\item I have also identified what evidence would be capable of disproving\ldots
\item I have considered and addressed biases and fallacies\ldots''
\end{itemize}}

 {\sc Clarissa}\ is experimenting with the decision support needed to assist
evaluators make and substantiate these judgments, with explicit links
from Assurance 2.0 concepts and {\sc Clarissa/asce}\ functions to the bullet points
above.



\newpage
\section{Summary and Conclusion}

We have explored methods for gaining and assessing confidence in
assurance cases based on Assurance 2.0 and its automated assistance
with {\sc Clarissa/asce}.  Here, we summarize these methods and provide brief
conclusions.  We do not provide references here: they can be found in
the earlier sections specific to each topic.

Assurance 2.0 is more rigorous and demanding than earlier treatments
of assurance cases, but we argue that this simplifies the development
and assessment of cases because issues that were previously treated in
an \emph{ad hoc} manner and subject to contention and challenge are now made
explicit and treated systematically.


In particular, we are explicit that the goal of Assurance 2.0 is
indefeasible justification, meaning we must be confident there are no
overlooked or unresolved doubts that could change evaluation of the
case.  A consequence of this is a strong preference in Assurance 2.0
for argument steps to be deductive, and for steps that are merely
inductive to acknowledge this and to explicitly manage the doubts
thereby admitted.  Similarly, evidence in Assurance 2.0 is weighed
very deliberately using confirmation measures and we distinguish
carefully between facts established by the evidence (claims about
``something measured'') and inferences drawn from it (claims about
``something useful'').



These rigorous requirements and other supporting constraints enable
straightforward evaluation of the positive criterion for assurance
case arguments that we call soundness.  Note that we say the
evaluation is straightforward, meaning it is clear what must be done,
not that it is easy: it requires sophisticated technical judgment, but
this judgment can focus on technical issues without being distracted
by unmanaged doubts and contested interpretations.

Another way in which Assurance 2.0 simplifies the assessment of
assurance cases is by being clear what is developed within the
assurance argument and what is referenced and integrated by it through
application of external theories and models.  The overall case will
include all necessary theories, models, and evidence assemblies but
the detail of these items is excluded from the argument, not because
they are unimportant but because they each have specialized form and
content and are therefore well suited to presentation and assessment
by scientific and engineering methods traditional to their fields.
The assurance case argument, on the other hand, must integrate these
disparate items and its structured, logical form is tailored for that
function and dedicated to it.




Whereas traditional assurance case arguments seem almost arbitrary in
their structure, so that reviewers do not know what to expect,
arguments in Assurance 2.0 generally follow a systematic pattern where
general claims at the upper level are refined into more precise claims
using concretion steps, then substitution steps are used to elaborate
these claims about high level models into claims about low level
models and their implementations, and these lowest level claims are
discharged by evidence.  Substitution steps relate a claim about one
model to a possibly different claim about a possibly different model,
although either the claim or the model is typically held constant.
Along the way, the argument may divide into subcases using
decomposition or calculation steps that enumerate a claim over some
structure (e.g., over components, requirements, hazards, etc.) or
split the conjuncts of a compound claim.  This structure may recurse
within subcases.  For example, we may have a lower-level claim that
software development conforms to standards, and will use a concretion
step to refine this to a specific standard and then develop the rest
of the subcase in the manner just described.

Their systematic structure allows argument steps in Assurance 2.0 to
be limited to just the five basic forms mentioned above (concretion,
substitution, evidence incorporation, decomposition, and calculation).
These each have a precise and obvious purpose and it is generally
straightforward to decide which to use at each argument step (see the
``helping hand'' visual mnemonic of Figure \ref{helping-hand}).  Each
type of argument step has side-claims that ensure it is used
appropriately and with a sound (e.g., deductive) justification.

Soundness is the most fundamental valuation for an assurance case: it
tells us that the argument and its evidence truly do support the top
claim, but it does not tell us how strongly they do so.  We therefore
define a method for probabilistic valuation that does this and
{\sc Clarissa/asce}\ can color argument nodes accordingly to support visual
comprehension of the weak and strong parts of an argument.  We apply
probabilistic valuation only to sound assurance case arguments, and
this eliminates (although we need to confirm this claim) the
vulnerabilities that have been found in other probabilistic forms of
assessment.  Our probabilistic methods are conservative and the
numerical valuations are of limited absolute value, but they do serve
to explore the risk of residual doubts and the relative
strengths of different cases for the same system.  This allows
rational tradeoffs of effort and cost versus confidence, which is
needed in developing graduated forms of assurance for different levels
of risk, as exemplified by the SILs (Software Integrity Levels) of IEC
61508, the ASILs (Automotive SILs) of SAE 26262, and the DALs (Design
Assurance Levels) of DO-178C.



While building a forceful positive case, the developers of an
assurance case must guard against confirmation bias.  This can be
assisted by vigorous and active exploration of challenges to, and
doubts about, the case during its construction.  In Assurance 2.0,
doubts are refined and recorded as defeaters, which are nodes in the
graphical representation of the assurance case argument that
explicitly challenge other nodes and that may have their own subcases
to validate or refute them.  Valid defeaters require revision to the
assurance case and possibly the system itself.  

{\sc Clarissa/asce}\ can selectively
reveal or hide defeaters and their subcases and can display the
changes made in response to valid defeaters.
In addition to guarding against confirmation bias, the record of
doubts explored as defeaters assists assessors of the case.  Assessors
begin their work by gaining an understanding of the case, perhaps by
posing ``what-if'' questions, and then probing it more deeply for weak
spots and oversights.  When previously examined defeaters are recorded
as part of the case, assessors may find that their own questions and
doubts have been anticipated and answered, thereby streamlining their
task and also enabling a constructive, dialectical examination of the
case by ``eliminative argumentation.''




All identified defeaters must be examined and resolved.  However, a
conscious decision may be made to accept some as residual doubts.  For
example, a subcase that uses testing to justify absence of runtime
exceptions may have residual doubt due to incompleteness of testing.
The risks posed by such doubts (i.e., the likelihood that they may be
falsified, and the potential impact and cost if they are so) must be
assessed and only those considered tolerable (technically, those
considered minor and manageable, and those considered negligible, see
Section \ref{residuals}) can be allowed to remain as residual risks:
others must be eliminated or mitigated by revisions to the argument or
the system.  The probabilistic valuation of {\sc Clarissa/asce}\ can be used to
help visualize the potential impact of residual doubts on the overall
argument.

In conclusion, Assurance 2.0 assesses confidence in an assurance case
by considering both positive and negative aspects.  The positive
aspects are logical soundness and (optionally) a probabilistic
valuation; the negative aspects are vigorous exploration of potential
defeaters, and careful evaluation of all residual doubts.  Assessors
should not simply inspect and ``sign off'' on an assurance case; we
expect them to actively explore and question both its positive and
negative aspects and to conclude with a ``sentencing statement'' that
declares their understanding of the system and its context, its
hazards and their mitigations, the key points of its architecture and
design, the soundness and probabilistic confidence of the assurance
argument with its supporting theories, models, and evidence assemblies,
their defeaters and residual doubts, and the relationship of the top
claim to acceptance criteria.  {\sc Clarissa/asce}\ provides assistance in these
evaluations and together they provide a comprehensive and rigorous
assessment for assurance cases that should be independent of the
vagaries of individual assessors.

These ideas were developed and explored during construction of
{\sc Clarissa/asce}\ using a variety of examples and represent a work in progress.
We plan to develop worked examples to will support more detailed
exploration and exposition that will be published in a companion
report.  In particular, we wish to explore what forms of guidance and
automated support are most useful for developers and assessors.

\paragraph{Acknowledgments.}

The work described here was developed in partnership with other
members of the {\sc Clarissa}\ project, notably Kevin Driscoll and Brendan Hall
of Honeywell, Gopal Gupta of UT Dallas, and Kate Netkachova of
Adelard.  Separately, N. Shankar of SRI provided valuable criticism.

\newpage

This material is based upon work supported by the Air Force Research
Laboratory (AFRL) and DARPA under Contract No. FA8750-20-C-0512.  Any
opinions, findings and conclusions or recommendations expressed in
this material are those of the author(s) and do not necessarily
reflect the views of the Air Force Research Laboratory (AFRL) and
DARPA.




\newpage

\addcontentsline{toc}{section}{References}
\bibliographystyle{modplain}
