- Robin Bloomfield, Bev Littlewood, Xingyu Zhao
Adelard and City University UK
Probability Of Perfection - A Practicable Approach?
Abstract
Many of the analyses and tasks that are required in the development of
critical software involve the elimination, with some degree of
confidence, of behaviours or features that are not wanted or judged to
be detrimental. An engineer, deploying a static analysis tool does not
normally think about the increased reliability that is achieved but
rather the confidence in, for example, the absence of run time errors
such as divide by zero. The link between reliability and such claims
is problematic although there is earlier research on conservative
bounds on mttft that be derived from beliefs in the total number of
defects left in a product. More recently the work of Littlewood,
Rushby and Povyakalo has shown how certain diversified architectures
probability of not perfect (pnp) for one subsystem and a probability
of failure on demand (pfd) for another can be combined to gain a
figure of the overall reliability that can be deployed in risk
analyses. This motivates the development of approaches to judge pnp.
In this talk/paper we explore whether in practice we might be able to
derive a figure for pnp and how that might be presented in a
"case". In this attempt we illustrate some of the differences between
a "proof" and a "case" and how, if we are successful we are left with
judgement about coincidental failures and other uncertainties that
seem challenging to quantify. (The work is immature, speculative and
entirely suitable for a workshop).
- Valentin Cassano, Tom Maibaum, Silvia Grigorova
McMaster University
A Reassessment of Toulmin's Argument Scheme in the Context of Assurance Cases
Abstract
Bloomfield and McDermid proposed the use of Toulmin's argumentation
ideas in the construction of safety cases, in particular, in safety
arguments. Although a promising beginning, this seminal standpoint
seems to have lost its pre-eminent position in more current approaches for
constructing safety cases. More precisely, while interesting in their
own right, e.g., as design notations for representing a goal
structured safety design decomposition for some artifact, notations
such as the GSN have no proper place or mechanism for representing the
main elements of Toulmin's celebrated notion of an argument
pattern.
Aiming at reinstating a full Toulmin style basis for safety argument,
we examine the logical status of Toulmin's argument pattern. Our
position is that, if we wish to give a formal account of a
Toulmin-like type of reasoning, we need to provide some rules of
inference characterising what we mean by proof. Toulmin's notion of an
argument pattern is not that. Instead, it is a scheme for a rule of
inference of a general kind. To further complicate matters, this
scheme is not an actual rule of inference as this concept is usually
recognized in logical studies, but a meta-scheme which has to be
properly instantiated. In that respect, the first thing to do is to
underpin the reasoning underlying safety cases. This will allow us to
instantiate Toulmin's notion of an argument pattern to either proper
rules of inference for an appropriate logic or a proper scheme for
such rules.
In the presentation we will explore the nature of such rules and
schemes and define some requirements for their definition. We also
explore the defeasible nature of such reasoning and the impact of this
defeasibility on the nature of the logic and the reasoning this logic
is intended to capture.
- Ewen Denney and Ganesh Pai
NASA Ames
The Role of Formalization and Argumentation in Assurance Cases
Abstract
Central to modern safety/assurance cases in many safety-critical
domains is a notion of structured argument marshaling heterogeneous
evidence, a significant portion of which can include formal
engineering artifacts.
However, in both civil aviation and when regulating civil operations
with unmanned aircraft, there is a distinct preference for using
normative regulations, and performance-based standards. When safety
cases are used, little to no importance is given to argumentation, at
least in the form of graphical argument structures.
Clearly, arguments can sometimes be formalized and there are times
when this is worth doing, at least for part of the argument. Equally,
however, there are times when an argument is best left informal. We
believe that despite this mixed formality, assurance arguments can
still be usefully given formal underpinnings.
In practice, safety/assurance cases themselves remain, largely, as
informal artifacts. Additionally, creating, evolving and evaluating
safety cases and their underlying arguments, continues to be a
manually-driven process, with the available set of tools providing
limited support for automation.
We believe that (i) a more formal foundation for safety cases will
affirm their role as essential, first-class, safety engineering
artifacts, and (ii) given a formal basis, that much can be
intelligently automated.
Though other researchers have explored the pros and cons of a formal
assurance case language, we instead consider formalization primarily
as the means of achieving greater automation in the creation and
evaluation of arguments.
In this talk, we present some of the issues involved in moving towards
a more formal, automated approach for safety case development, and how
some of these have been addressed in our toolset for assurance case
automation, AdvoCATE. We illustrate this with several examples as
applied to safety assurance of unmanned aircraft systems.
- Lian Duan, Mats Heimdahl
Department of Computer Science and Engineering, University of Minnesota.
Representing Confidence in Assurance Case Evidence
Abstract
When evaluating assurance cases, being able to capture the confidence
one has in the individual evidence nodes is crucial, as these values
form the foundation for determining the confidence one has in the
assurance case as a whole. Human opinions are subjective and
uncertain; it is difficult to capture an opinion with a single
probability value. Thus, we believe that a distribution is best
suited to captures human opinion such as confidence. Previous work has
used a doubly-truncated normal distribution or Dempster Shafer theory
to represent confidence in the evidence nodes.
In this talk, we will argue that that a beta distribution is more
appropriate. The beta distribution models a variety of shapes and we
believe it provides an intuitive way to represent confidence.
Furthermore, there exists a duality between the beta distribution and
subjective logic, a duality can be exploited both in the calculation
of confidence and the presentation of the results.
- Lu Feng, Andrew King, Insup Lee, Oleg Sokolsky
PRECISE Center,
Department of Computer and Information Science,
University of Pennsylvania
Towards a Logical Foundation for Assurance Arguments for Plug & Play Systems
Abstract
There is a growing interest in plug & play systems in domains such as
healthcare, where multiple medical devices are assembled at the
bedside to coordinate with each other. Such plug & play medical device
cyber-physical systems (MCPS) would help to provide better medical
treatment to patients. For example, they can provide better
physiologic alarms (by combining data streams from multiple medical
devices) and closed loop control (by using physiologic sensors to
drive actuators). MCPS are safety-critical systems, and thus they need
to be evaluated for safety by regulators before they can be used. The
state of the art in safety assessment is to consider the complete
system. However, unlike other safety-critical systems such as
aircrafts and nuclear plants, plug & play MCPS are constructed at
bedside, based on the needs of an individual patient and from
available devices. The challenge is how to assess the safety of plug &
play MCPS a priori if we don't know precisely what medical devices
(i.e., make, model, brand, etc.) will be used in the instantiation?
We consider the development of safety assurance arguments for such
plug & play systems. Specifically, we propose an assurance argument
pattern to assist the safety analysis of plug & play MCPS, each of
which consists of a set of medical devices, an App (i.e., a software
component that coordinates the medical devices for a specific clinical
scenario), and a platform that runs the App. Each App defines a set of
possible systems: one for each allowed combination of devices and
platform. We assume that the App vendor will need to devise an
assurance argument that explains why all these possible combinations
are safe. The core of our assurance argument pattern is a
platform-oriented argument strategy, which relies on the model-based
analysis at design time and the validation of modeling assumptions
during assembly. The proposed argument pattern also leverage the
safety evidences provided by device vendors. We present an
assume-guarantee compositional proof rule for plug & play MCPS and
show how it can be used to as a logical basis for the proposed
pattern.
- John B. Goodenough, Charles B. Weinstock
Software Engineering Institute
Using a Perfect Argument in an Imperfect World
Abstract
In this talk, we consider how the structure of a deductive argument
can be combined with uncertainties in real-world evidence (and
inference) to justify why one should have a certain degree of
"confidence" in a claim. We consider whether there is a practical
difference (from an assurance perspective) between strong confidence
in a weak claim and weak confidence in a strong claim. Although the
exploration of confidence issues is first developed in light of a
simple, abstract example, we then show connections to more realistic
examples.
- Silvia Grigorova, Tom Maibaum
McMaster University
On the Necessity of Evaluating Safety Evidence Weight and the Use of Baconian Reasoning
Abstract
When we reason about the safety properties of a system we are faced
with both epistemic and aleatoric uncertainty. Because of various
practical constraints it is never possible to eliminate uncertainty
completely. It is characteristic of all the elements of the safety
case argument – evidence, including assumptions and context, and
argument, including the rules of inference that allow us to "jump to
conclusions" and the backing that increases our confidence in the
applicability of these rules. Thus, we are faced with the problem of
how to model and evaluate this uncertainty. In some cases, we might
use a frequentist or Bayesian approach to model the extent to which
evidence supports (or refutes) the truth of a claim. However, there is
an additional aspect of evidence that needs to be considered and
modeled. The concept of evidence weight is critical in the evaluation
of the safety argument, as the amount and comparative relevance of the
evidence that has been collected (versus all the relevant evidence
that exists) greatly influences the confidence that we may place in
the argument's claims. Thus, a proper safety argument evaluation
approach necessarily needs to consider this aspect characterizing
evidence, and we suggest a way of modeling it. In the talk we argue
that Baconian reasoning is better suited to that end than Bayesian
reasoning. This is also the view held by a number of proponents of
Baconian probability, including J.M.Keynes, R. Carnap and L.J. Cohen.
- Paul Joannou
McMaster Centre for Software Certification
Acceptance Criteria for Systems Supported by an Assurance Case
Abstract
An assurance case is a reasoned, auditable artefact created to support
the contention that a claim or set of claims about an engineered
system are satisfied. It contains the following and their
relationships:
- one or more claims about properties of the system;
- arguments that logically link a body of evidence and any assumptions to the claim(s);
- a body of evidence supporting these arguments for the claim(s).
One of the primary users of the assurance case is an entity with the
authority to decide that the assurance case and the level of
confidence it provides are acceptable. This approval authority may be
held by a governmental organization in the case of a regulatory
situation, or may be held by an acquirer in a two-party situation.
The acceptance criteria for an assurance case will differ depending on
the level of confidence that is required that the claims are
satisfied. The required level of confidence is typically dependent on
the level of risk associated with the claims not being satisfied.
There are four key aspects of the system for which the approval authority must have acceptable confidence.
- Confidence that the claims are correct and complete,
- Confidence that the system has been implemented consistent with the claims,
- Confidence that the system will be operated and maintained consistent with design assumptions, and
- Confidence that 1, 2 and 3 are sustained during the lifetime of the system.
The acceptance criteria for providing adequate confidence is typically based on:
- Qualifications of the individuals involved,
- Use of due process in a planned and systematic manner,
- Clear documentation that is third party reviewable, and
- Objective evidence that the system meets its quality objectives.
Definition of the acceptance criteria for all four key aspects prior
to system development provides guidance to the developer as to how
acceptability of the system will be assessed, and provides consistency
to the assessments done by different approval authorities.
The talk will provide this overall context of assurance and emphasize
the role that verification plays in achieving acceptable assurance
along with the many other criteria.
- John Knight
University of Virginia
Assurance Cases - The Home for Verification
Abstract
Formal verification provides a high level of assurance that a
statement in logic, such as a software specification or a software
implementation, possesses a logical property. The high level of
assurance derives from the basis of the assurance, namely a proof.
Valuable though a proof is, any proof comes with two limitations:
1. The proof could be wrong in some way.
2. The value of the property established by the proof is not inherent in the exi
stence of the proof.
Both of these limitations are addressed with an assurance case. The
first limitation is addressed by the requirement to develop an
inductive argument that the proof is believed to be correct. This
argument is inductive, because it relies on assurance of items such as
the correct use of the tools used to develop the proof.
The second limitation is addressed by the use of the property that the
proof establishes as evidence. The evidence is a solution in the
assurance case, and thus the exact role of proof in the context of a
system of some sort is defined. We conclude, therefore, that an
assurance case provides an ideal structure within which to use the
notion of formal verification.
- Yutaka Matsuno
Department of Computer Engineering, College of Science and Technology,
Nihon University
Toward Practical Use of Assurance Cases: Definitions, Methods, and Tools.
Abstract
The simple concepts of Assurance cases: claim, argument, and evidence
have been getting attention in safety industry and also formal methods
and argumentation communities. However, despite the simple concepts,
when applying assurance cases into system development in practice,
there arises many questions and challenges. One of the fundamental
question is "What is An Assurance Case?"; also, a basic challenge is
how to introduce assurance cases into system lifecycle where other
methods such as FTA, FMEA, and UML have been already used. Started
from 2010, we have been introducing assurance cases to Japanese
industires (please
see http://www.dcase.jp). Also, we
have developed an assurance case (GSN) editor called "D-Case
Editor". For the design and implementation, we have exploited
functional programming techniques (see our DSN2014 paper). This paper
presents our definitions, methods, and tools for assurance cases which
were made during our activities.
- Harald Ruess, Sebastian Voss, and Carmen Carlan
Fortiss, Munich
Towards Meaningful Assurance Cases
Abstract
Safety cases are a tried and tested method for arguing about and
documenting the safety of software-intensive systems. However,
assurance cases are usually not well-integrated with system models and
the consequences are profound. Therefore, we are proposing a tight
integration and co-development of component and system models with
safety case arguments. In this way, one may automatically guide the
construction of the system architecture w.r.t. the claims given in the
safety claim. We illustrate first ideas on using model-to-model
transformations for guiding the construction of safe system
architectures and on building up convincing assurance cases from
results of formal verification or statistical testing.
- Kevin Sullivan
University of Virginia Department of Computer Science
Continuous Systems Value Assurance
Abstract
Project and system value arise from a diversity of system and
meta-system properties, stakeholder preferences, and evolving external
conditions. Maintaining acceptable levels of value assurance across
the systems engineering life-cycle is a hard, important, unsolved
problem. We are working to develop, evaluate, and promulgate improved
concepts, models, methods, and tools to address this problem. Our work
combines formal theories of system value, experimentation, assessment
of evidence, and ongoing evolution of systems, theories, and
evidence. We express our formal theories using the languages of the
Coq proof assistant, for its mathematical expressiveness, constructive
proofs, and automation. A combination of code synthesis and web-based
code deployment helps enable practical experimental evaluation and
evolution of our theories and tools while largely hiding arcane
formalism. Our overall perspective is that value assurance cases take
the form of domain-specific instances of generalized scientific
theories of system and project value along with evidence and analysis
supporting assessments of degrees of theory confirmation, epistemic
gaps and risks, and value assurance. Such assessments in turn support
determination of appropriate next steps in theory or system test and
evolution. Key open questions include the viability of generalized
theories of system properties that can be productively specialized to
particular systems and projects, and how to reason effectively from
evolving evidence to confidence in system and project value.
- Alan Wassyng
McMaster University
A Template for an Assurance Case Shall Be Known as an Assurance Case Template
Abstract
With thanks to Groucho and Chico.
An assurance case is almost universally described as a structured
argument that uses evidence to support a claim (or claims) about
properties of a system. Over the years it has become apparent that
the concept is powerful, and can be practical and effective. It has
also become apparent that there are deep issues involved in developing
assurance cases so that they are:
- useful;
- sound;
- tractable for developers of the system;
- reviewable by regulators or other certifiers.
In order to cope with these issues we have to deal with concepts such
as argument, evidence, acceptance criteria, and confidence. The
concepts are vital to the development of assurance cases, but may
require a level of very specialized knowledge that is not commonly
available. A technique that has been used for many years to alleviate
this problem is one of argument patterns (also called safety case
patterns, or assurance case patterns).
What I mean by an assurance case template is somewhat different from
the usual argument patterns -- it is a more "complete" pattern for a
particular class of assurance cases. We should be able to do this if
there are classes of systems for which a set of high quality assurance
cases can be developed, and the assurance cases within this set are
"almost" identical with respect to the argument structure, evidence
and acceptance criteria. The important conjecture here is that there
are domain specific classes of systems for which this technique will
work, and work well.
This approach could have a number of advantages, including: the
template can be used to drive development of systems in a way that
they are designed to be safe, secure and dependable right from the
outset; a community developed template can perform the function of a
standard, but provide better guidance in that expectations would be
clearer; and valid arguments can be built into the template without
everyone involved having to be an expert in argument structure.
This talk will explore what the essential characteristics of such a
template should be.