Yassir Idmessaoud

Didier Dubois

Jérémie Guiochet

Belief functions for safety arguments confidence estimation : A comparative study

Keywords: Confidence Assessment, Goal Structuring Notation (GSN), Dempster-Shafer theory (DST), Evidence fusion, Safety cases

Structured safety arguments are widely applied in critical systems to demonstrate their safety and other attributes. Graphical formalisms such as Goal Structuring Notation (GSN) are used to represent these argument structures. However, they do not take into account the uncertainty that may exist in parts of these arguments. To address this issue, several frameworks for confidence assessment have been proposed. In this paper, a comparative study is carried out on three approaches based on Dempster-Shafer theory. We extract and compare the implicit logic at work in these works, and show that, to some extent, these current approaches fail to provide a consistent relationship between the informal statement of arguments, their logical model and the use of belief functions. We also propose recommendations to improve this consistency.

Introduction

The deployment of autonomous systems in the highly uncertain human environment raises the issue of safety. Argument structures are widely used to evaluate and prove the safety of these systems. They are a clearly represented collection of rational pieces of evidence like test or simulation results, expert judgments, analysis reports, etc. They aim to demonstrate that a certain property of the system is satisfied. Many studies and standards define safety arguments as "Safety cases" (e.g, in the automotive [START_REF]Software considerations in airborne systems and equipment certification[END_REF] or railway [START_REF]Railway applications -Safety related electronic systems for signaling[END_REF] industries), but it is now extended to more general domains like dependability, assurance or trust cases. These cases are presented in the form of texts, tables or, more interestingly, graphically. Using graphical tools to represent arguments structures is more relevant because graphs are simpler to review, offer a clear overlook, help to understand the connection between pieces of evidence, and moreover they are easier to use and manage. Formalisms such as Goal Structuring Notation (GSN) [START_REF] Kelly | Arguing Safety -A Systematic Approach to Safety Case Management[END_REF] and Claims-Arguments-Evidence (CAE) [START_REF] Bloomfield | Building blocks for assurance cases[END_REF] are commonly used in this field. However, even with all these benefits, these tools do not take into account the uncertainties pervading this sort of arguments. Especially since autonomous systems, and critical systems in general, are becoming much more complex, they are affected by many sources of uncertainty like any decision support system, AI based system and the like. As a response to this issue many research projects are conducted to find a solution.

Several works have proposed methods based on Bayesian Networks (BN) to model uncertainty in a safety argument [START_REF] Hobbs | The application of bayesian belief networks to assurance case preparation[END_REF][START_REF] Denney | Towards measurement of confidence in safety cases[END_REF][START_REF] Guiochet | A model for safety case confidence assessment[END_REF]. Nevertheless, these approaches have a major impediment, which is the need for data. As a matter of fact, using BN requires statistical information that is often not available. Moreover, the use of subjective probabilities is questionable in the presence of partial ignorance. Dempster-Shafer theory (DST) (aka Theory of Evidence) was developed to address the issue of imprecise evidence [START_REF] Sentz | Combination of evidence in dempster-shafer theory[END_REF]. It represents a form of generalized probability theory where probability masses are assigned to sets of possible values, instead of singletons. In some works on safety argumentation, aggregation rules stemming from DST are used to merge confidence degrees in pieces of evidence (represented by mass functions) and calculate an overall mass function, in order to estimate an overall confidence in the top statement of a safety argument (e.g.,"the system is acceptably safe"). In our problem, the connection between pieces of evidence is represented by various types of arguments. In the literature, they strongly influence the choice of an aggregation rule. However, no real consensus emerges in current research works to relate argument types, their logical modeling, and aggregation rules based on DST.

In this paper, three approaches to uncertain safety cases using DST are compared as to the different definitions of types of arguments they propose and we review and discuss the aggregation methods they use. Section 2 presents the background on safety cases and introduces the existing selected approaches. Section 3 extracts the formal definitions of arguments from the selected articles [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF][START_REF] Cyra | Support for argument structures review and assessment[END_REF][START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF]. Then, we compare and analyze the aggregation rules used to compute belief degrees of the top statement of an argument. Section 4 suggests the existence of two basic types of arguments and proposes a rigorous methodology.

Baseline and related work

This section introduces a safety case formalism (GSN), some works on confidence quantification, and basic concepts of DST.

Background

Safety arguments or safety cases can be defined in multiple ways. In fact, the definition may vary slightly according to the field where it is used. For instance, in the automotive industry [START_REF]Software considerations in airborne systems and equipment certification[END_REF], it is defined as : argument that functional safety is achieved for items, or elements, and satisfied by evidence compiled from work products of activities during development. This concept has been generalized in the OMG (Object Management Group) standardized Assurance Case Metamodel [START_REF] De | An analysis of safety evidence management with the structured assurance case metamodel[END_REF] and an instance of it is the goal structuring notation (GSN), which is commonly used to represent safety cases [START_REF] Kelly | Arguing Safety -A Systematic Approach to Safety Case Management[END_REF]. As presented in Figure 1, it includes nine main elements. It breaks down the conclusion called a Goal (following a given Context and in accordance with a specific Strategy) into Sub-goals and

G2

{Hazard Hn} has been addressed

G1

{System X} is acceptably safe

S1 C1 Sn1

Fault tree for {Hazard H1}

Solution Goal

Undeveloped Goal (to be developed)

Strategy Context

Argument by that all identified hazards have been addressed

List of identified hazards for {System X} supports each of them by evidence items called Solutions. The choice of strategies and sub-goals is supported by the use of so-called Justifications. Figure 2 presents an example of a GSN pattern.

SupportedBy

C1

List of identified hazards for {System X}

G1

{System X} is acceptably safe

S1

Argumentation by claiming addressed all identified plausible hazards A given prevention risk control is implemented.

A given protection risk control is implemented.

G2 {Hazard H1} has been addressed

G3 {Hazard H2} has been addressed

Gn {Hazard Hn} has been addressed … {Hazard H1} has been removed.

Sn1 Sn2 Sn3

Fig. 2. GSN example adapted from Hazard Avoidance Pattern [START_REF] Kelly | Safety case construction and reuse using patterns[END_REF].

GSN is categorised as a qualitative method to justify safety. However, in this example, many uncertainties may exist. For instance, what is the uncertainty linked to the element "C1: List of identified hazards" or what is the confidence in the solutions Sn (also called pieces of evidence). In order to estimate the confidence in the top goal G1, all these uncertainties should be assessed. Some quantitative approaches have been proposed to assess uncertainties in such arguments [START_REF] Graydon | An investigation of proposed techniques for quantifying confidence in assurance arguments[END_REF]. In [START_REF] Hobbs | The application of bayesian belief networks to assurance case preparation[END_REF][START_REF] Denney | Towards measurement of confidence in safety cases[END_REF][START_REF] Guiochet | A model for safety case confidence assessment[END_REF], Belief Bayesian Networks (BBN) are used to assess confidence in safety case structure and pieces of evidence. They measure confidence by computing probabilities from evidence to conclusion. Due to the huge amount of data required to apply BBN, other works based on subjective logic [START_REF] Jøsang | Subjective logic[END_REF][START_REF] Yuan | A subjective logic-based approach for assessing confidence in assurance case[END_REF] or on DST are proposed to define and estimate uncertainties. These works are presented in Section 2.2.

Dempster-Shafer Theory offers a powerful setting to combine pieces of evidence. A mass function, or basic belief assignment (BBA), assigns probabilities over the power set of the universe of possibilities (Ω), known as the frame of discernment. Formally, a mass function m Ω : 2 Ω → [0, 1] is such that E⊆Ω m(E) = 1, and m(∅) = 0. Any subset E of Ω such as m(E) > 0 is called a focal set of m. Mass assignment induces the concept of belief function (bel : 2 Ω → [0, 1]). It represents the summation of all the masses supporting the same statement and is defined by : bel(A) = E⊆Ω,E =∅ m(E). Belief in the denial or uncertainty of the statement A are respectively represented by : disb(A) = bel(¬A) and uncer(A) = 1 -bel(A) -disb(A).

In our case, we use propositional variables for which the frame of discernment has two states: Ω = {T rue(T ), F alse(F )}. As a consequence, in such frames, mass function and belief function for T and F are equal. For example, consider a statement A saying that a clock provides the right time. The mass function m Ω such that m Ω ({T }) = 0.5, m Ω ({F }) = 0.2 and m Ω ({T, F }) = 0.3 quantifies respectively the degrees of belief (0.5), of disbelief (0.2) and of uncertainty (0.3) in A. In this case, due to the Boolean form of the frame of discernment, we have bel(A) = m Ω ({T }), disb(A) = m Ω ({F }) = 0.2 and uncer(A) = m Ω ({T, F }) = 1 -m Ω ({T }) -m Ω ({F }). They represent respectively our belief that the time read is correct, not correct, and the probability that we don't know the time by reading the watch (Tautology).

Another important tool from DST is the Dempster rule of combination. It is used to merge various pieces of evidence coming from independent sources of information, and is represented by mass functions m i , i = 1, . . . , n. It proceeds in two steps. For two mass functions:

1. a conjunction of random sets:

m ∩ = m 1 ⊗ m 2 such that m ∩ (A) = E1,E2:E1∩E2=A m 1 (E 1 ) • m 2 (E 2 ); 2. a renormalization step if m ∩ (∅) > 0: m(A) = m ∩ (A)/(1 -m ∩ (∅)). The value m ∩ (∅) represents the degree of conflict between m 1 and m 2 .
This combination rule is commutative and associative.

Some DST-based approaches to safety cases

In this subsection, we discuss three uncertainty management methods in safety cases proposed in the literature. All such methods are DST-based. Two of them use Goal Structuring Notation (GSN) for structuring arguments. Our objective is to extract, in each paper, definitions of argument types, and to evaluate their consistency with the proposed aggregation rule that computes degrees of belief of conclusions. Cyra and Gorski [START_REF] Cyra | Support for argument structures review and assessment[END_REF] present an argument model called VAA inspired by Toulmin [START_REF] Toulmin | The Uses of Argument[END_REF] to graphically represent all pieces of evidence that support a conclusion (e.g., "The system is safe"). It proposes a method that, in a first step, transforms qualitative expert opinions expressed in natural language, about pieces of evidence (forming premises), into belief and plausibility functions, using [START_REF] Jøsang | Subjective logic[END_REF]. In a second step, the authors define five argument patterns and associate to each of them an appropriate belief aggregation rule. These rules use as inputs the values obtained at the first step, to calculate the overall confidence in the conclusion.

Anaheed et al. [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF] define four basic types of arguments. Each argument type is composed of at least two premises that support a conclusion. Premises are assessed by two parameters (sufficiency and insufficiency) and every argument type is associated to an aggregation rule. In this paper, they propose an algorithm based on a bottom-up approach that computes the degree of confidence in each premise to calculate the overall confidence in the system.

Wang et al. [START_REF] Wang | D-S Theory for Argument Confidence Assessment[END_REF][START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF][START_REF] Wang | Modelling Confidence in Railway Safety Case[END_REF][START_REF] Wang | Safety Case Confidence Propagation Based on Dempster-Shafer theory[END_REF] propose a confidence assessment method by converting qualitative expert opinions, on their confidence in pieces of evidence appearing in a GSN, into mass functions. These values are then merged by Dempster rule of combination to obtain the overall confidence in the studied system. The paper also defines two parameters to assess confidence: Trustworthiness to quantify confidence in the evidence; Appropriateness to quantify the confidence in the claim that the evidence supports the conclusion.

Comparative study

In this section, we introduce a framework for confidence assessment. Then, we compare argument types given in the studied papers and the propagation rules used to calculate the overall confidence.

General framework for BF-based confidence estimation

In order to estimate the overall confidence of the argument structure, our main issue is how to propagate the quantitative values coming from the confidence in premises in accordance with the characteristics of its structure. In this regard, it is important to propose a general method to compute degrees of belief in conclusions of safety cases. Most works omit to provide this general method putting together logic and belief functions. Such a methodology was described more than 30 years ago [START_REF] Chatalic | An approach to approximate reasoning based on Dempster rule of combination[END_REF] and is recalled here.

The first step is to define the nature of the relationship between premises in their support of the conclusion, known as argument types. These types should be firstly expressed informally in a natural language (e.g, if premises P 1 and P 2 are true, then the conclusion (C) is true) because it is more understandable for the human expert. Then this verbal relation should be transformed into a formal logical sentence (e.g., P 1 ∧ P 2 ⇒ C). The importance of these definitions lies in the fact that they significantly affect the logical expression of the links between pieces of evidence and the conclusion. The second step is mass assignment. This task consists in defining masses assigned to the focal sets deduced from the logical expressions obtained from argument definitions.

Consider a set of well-formed formulas K = {φ 1 , . . . φ n } in propositional logic, and a formula C such that K C. Assume each formula φ i is a piece of evidence that comes from a specific source independent of other ones. Uncertainty about the validity of each formula can be represented by a mass function m i assigning some probabilities to φ i , ¬φ i and the tautology . Take for example the case of a simple premise P and a rule in the form of an equivalence P ≡ C. One mass function will be assigned to the premise P in the form of three values m 1 (P ), m 1 (¬P ) and m 1 ( ) summing to 1, and another will be assigned to the rule (m

2 (P ≡ C) + m 2 ( ) = 1).
The third step is to choose the appropriate aggregation rule. This rule will be used to calculate the belief in the top goal (conclusion) based on beliefs about premises and rules. Extending classical logic inference to this uncertain environment can be done by means of Dempster rule of combination [START_REF] Chatalic | An approach to approximate reasoning based on Dempster rule of combination[END_REF], first computing an overall mass function, m = m 1 ⊗ • • • ⊗ m n and then computing the degree of belief in the conclusion C as Bel(C) = φi C m(φ i ). There are also several variants of this combination rule that could be used in evidence fusion. However, each method obeys certain assumptions and describes some kind of situation. That is why it is needed to make sure that every definition resulting from the first step verifies the assumptions and each fusion rule fits with the given situation. Here, pieces of evidence and rules are supposed to come from independent sources. If this assumption is not satisfied, idempotent combination rules can be used as discussed in [START_REF] Denoeux | Conjunctive and disjunctive combination of belief functions induced by nondistinct bodies of evidence[END_REF][START_REF] Destercke | Idempotent conjunctive combination of belief functions: Extending the minimum rule of possibility theory[END_REF].

The complete process includes an additional preliminary step, which consists in transforming expert opinions (qualitative values) expressed in natural language (safe, little safe, uncertain, etc.) into a numerical format that can be computed with (i.e. mass, belief or plausibility functions). This could be done in [START_REF] Cyra | Support for argument structures review and assessment[END_REF] using the triangle method of Josang [START_REF] Jøsang | Subjective logic[END_REF]. This is needed to compute the belief in the conclusion. The choice of this transformation has a profound impact on the results. However this aspect of the evaluation process will not be addressed in this paper.

Definition of argument types

The concept of argument type pertains to the logical relationship between the premises and the conclusion. In other words, it answers the question : In which format do the premises support the conclusion ? The terminology is not uniform. For instance, in [START_REF] Cyra | Support for argument structures review and assessment[END_REF] this relation is named a warrant, in [START_REF] Yuan | A subjective logic-based approach for assessing confidence in assurance case[END_REF] it is called an affection factor and in [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF] it is named appropriateness. Moreover, most papers only give an informal definition.

Table 1 presents formal definitions of argument types that we infer from the reviewed papers. We notice from the formal definitions given in Table 1 that the premises are related to the conclusion by either an equivalence or an

[pi ⇒ C] ≡ [∨ n i=1 pi] ⇒ C).
Formal definition Terminology for argument types Type 1 (∧ n i=1 pi) ≡ C NSC-Arg [START_REF] Cyra | Support for argument structures review and assessment[END_REF], Consensus [START_REF] Yuan | A subjective logic-based approach for assessing confidence in assurance case[END_REF], Full complementary

[24] Type 2 ∧ n i=1 (pi ≡ C) Disparate [24] Type 3 (∧ n i=1 pi) ⇒ C SC-Arg, C-Arg [4], Conjunctive argument [29] Type 4 ∧ n i=1 (pi ⇒ C) A-Arg [4], Alternative argument [1] Type 5 (∨ n i=1 pi) ⇒ C
Disjunctive argument [START_REF] Yuan | A subjective logic-based approach for assessing confidence in assurance case[END_REF], Full redundant [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF] Type 6

∧ n i=1 (pi ≡ C) (∧ n i=1 pi) ≡ C AC-Arg [4]
, Complementary [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF], Containment, Overlapping arguments [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF] Type 7

∧ n i=1 (pi ≡ C) (∨ n i=1 pi) ≡ C R-Arg [24]
implication connective. The choice could be justified by the intuitive perception of the relation between premises and conclusion (e.g. "The system is safe" is supported by "Hazard H1 has been addressed"). As already noticed, there are two types of arguments, one using implication, the other using equivalence. Using equivalence assumes that there is a symmetry between the conclusion and premises. Consider a small safety case where the statement "The system is safe" is supported by the premise "All tests are conclusive". Using equivalence means, on the one hand, that the system is safe because we are confident in our tests; on the other hand, that the actual safety of the system can only be ensured by the success of the tests, which is not necessary true. In addition to this, the use of equivalence generates cases for the denial of the conclusion (disbelief) which appears in the calculation as a conjunction of one or several premises with the negation of the conclusion (¬C). For instance, consider the case of a conclusion (C) supported by a single premise (p) with an equivalence relation between them (Type 1 or 2). Combining the masses of (p) and the rule (p ≡ C) with DS combination rule reveals two cases where the conclusion is not satisfied (¬p ∧ ¬C) and (p ∧ ¬C). Using implication can only indicates that, due to the tests, the system is safe; it cannot prove that it is faulty. Choosing between equivalence or implication could also be justified by the purpose of the safety case. Generally speaking, a safety case is used to demonstrate that a system is acceptably safe. Its purpose is to provide a structured argument in order to certify a critical system, and not to present statements that it could be faulty, i.e. that there is disbelief about safety greater than 0. This is actually guaranteed when using only implication. In contrast, if the goal is to use the safety case at the debugging phase, i.e. to consider that disbelief in the conclusion may be not null, the equivalence may be an appropriate choice between premises and conclusion. Since we are interested, in this study, in the certification aspect of safety cases, the remainder of the paper will be focusing on argument types modelled by implication from tests to a statement of safety.

We also notice from Table 1 that the premises are linked with each other by AND, OR logic gates or by a combination of the two. It depends on whether, for instance, tests justifying a conclusion are alternative or complementary. For example, type 3 represents the situation where the conjunction of all premises is needed to support the conclusion. In the contrary, type 4 represents the case of separate rules where each premise alone can support the whole conclusion.

Mass assignment

As seen in previous sections, masses are allocated to propositions of interest. Apart from the assignment of masses to logical expressions resulting from the definition types arguments (called appropriateness in [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF]), masses are also assigned to premises to assess their degree of confidence. This evaluation is used under the name trustworthiness in [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF] and affection factor in [START_REF] Yuan | A subjective logic-based approach for assessing confidence in assurance case[END_REF]. Normally, mass functions assigned to premises (P i ) have two parameters : belief (i.e. m p (P i )), disbelief (i.e. m p (¬P i )) and the remainder is their uncertainty (i.e m p ( ) = 1 -m p (P i ) -m p (¬P i )). In cases when the argument is an implication, not an equivalence, the disbelief in the premises will not affect the conclusion, and need not be taken into account in the uncertainty propagation. This remark reduces the number of useful focal sets and simplifies the calculation.

The choice of mass functions is a very important step in the assessment process. It has a huge impact on the form of the final result. We can either define several mass functions, one for each logical expression, to emphasize the fact that there are multiple independent sources of information. Or, one mass function is distributed over all the logical expressions to represent the situation where a single source supplies these pieces of information.

Belief Aggregation

As we saw in the previous Section 3.2 the informal definition of argument types is important for the belief assessment process. Since masses are also assigned to the logical formulas resulting from these definitions, many authors confuse logical and numerical aspects. But as explained in Section 3.1, the definition of argument type, especially the informal ones, conditions the choice of focal sets, on the one hand. On the other hand, it also affects the choice of the aggregation rule. For example, one may think of using the disjunctive consensus rule [START_REF] Dubois | A set-theoretic view of belief functions. Logical operations and approximation by fuzzy sets[END_REF], if disjunction is expressed in the definition. In this section, we are interested in choosing aggregation rules based on Dempster-Shafer Theory and observing the effect of mass functions assignment on the degree belief of the conclusion.

DST offers many aggregation rules (Dempster rule, disjunctive consensus, Yager's rule, etc. see [START_REF] Sentz | Combination of evidence in dempster-shafer theory[END_REF][START_REF] Smets | Analyzing the combination of conflicting belief functions[END_REF] for surveys). However, we are going to focus on the methods used in the studied papers listed in Table 2. In general, Dempster combination rule computes the intersection of focal sets. If some focal sets from one source are inconsistent with some from another source, a renormalization must take place. It also assumes that sources are independent and reliable. Other combination rules that express a conjunction exist (e.g. Yager's [START_REF] Yager | On the Dempster-Shafer framework and new combination rules[END_REF] and Inagaki's rules [START_REF] Inagaki | Interdependence between safety-control policy and multiple-sensor schemes via Dempster-Shafer theory[END_REF]). For instance, Yager's rule uses a renormalization scheme different from the one of Dempster, reallocating mass of the empty set to the whole frame. The disjunctive rule of combination is a union of random sets and does not need renormalization. Finally, the weighted average rule [START_REF] Sentz | Combination of evidence in dempster-shafer theory[END_REF] is used to make a trade-off between conjunctive and disjunctive methods.

So long as the focal propositions involved in a safety case are not conflicting, there is no need to renormalize the resulting mass function, nor to use the disjunctive rule. By taking into account the definition of a safety case and the underying assumptions, applying Dempster rule (without normalization) to aggregate evidences is well adapted. nation rule, presented earlier, to merge each premise with its appropriate rule (see Table 3), and secondly merge the two resulting mass functions m i (see Table 4). Notice that we could also merge premises and rules separately first, then fuse partial conclusions together. The result will be the same because Dempster rule is associative and commutative.

Table 3. Combination of a premise with its rule

m1 = mp 1 ⊗ mr 1 mr 1 (p1 ⇒ C) mr 1 ( ) mp 1 (p1) p1 ∧ C p1 mp 1 ( ) p1 ⇒ C
In the example given in Table 3, the focal formula p 1 ∧ C results from the conjunction between formulas p 1 and p 1 ⇒ C. Its mass is calculated by multiplying the masses values in the corresponding line and column. Since the frame of discernment (Ω) of elementary mass functions has two states, masses and belief functions of non-tautological inputs are equal. The calculation of the remaining masses follows the same logic. An example is given here, where, bel i ⇒ (p i ⇒ C) represents the degree of belief that the i th premise supports the conclusion and bel i p (p i ) represents the belief degree in the i th premise. For instance, m 1 (p

1 ∧ C) = m p1 (p 1 ) × m r1 (p 1 ⇒ C) = bel 1 p (p 1 ) × bel 1 ⇒ (p 1 ⇒ C).
Likewise the combination of m 1 and m 2 , yields mass function m 12 using Table 4.

Table 4. Combination of confidence in type 4 :

∧ n i=1 (pi ⇒ C) m12 = m1 ⊗ m2 m2(P2 ∧ C) m2(P2) m2(P 2 ⇒ C) m2( ) m1(P1 ∧ C) P1 ∧ P2 ∧ C P1 ∧ P2 ∧ C P1 ∧ C P1 ∧ C m1(P1) P1 ∧ P2 ∧ C P1 ∧ P2 P1 ∧ (P2 ⇒ C) P1 m1(P1 ⇒ C) P2 ∧ C P1 ∧ (P2 ⇒ C) (P1 ∨ P2) ⇒ C P1 ⇒ C m1( ) P2 ∧ C P2 P2 ⇒ C
The calculation of the degree of belief bel c (C) in the conclusion for type 4 arguments is as follows (in Table 4 cells in gray identify φ's that imply C):

bel 4 c (C) = φ:φ implies C m 12 (φ) = m 12 (P 1 ∧ P 2 ∧ C) + m 12 (P 1 ∧ C) + m 12 (P 2 ∧ C) = m 1 (P 1 ∧ C) φ2 m 2 (φ 2 ) + m 2 (P 2 ∧ C) φ1 m 1 (φ 1 ) -m 1 (P 1 ∧ C)m 2 (P 2 ∧ C) = m 1 (P 1 ∧ C) + m 2 (P 2 ∧ C) -m 1 (P 1 ∧ C)m 2 (P 2 ∧ C) = bel 1 p (P 1 )bel 1 ⇒ (P 1 ⇒ C) + bel 2 p (P 2 )bel 2 ⇒ (P 2 ⇒ C) -bel 1 p (P 1 )bel 1 ⇒ (P 1 ⇒ C)bel 2 p (P 2 )bel 2 ⇒ (P 2 ⇒ C) = 1 -[1 -bel 1 p (P 1 )bel 1 ⇒ (P 1 ⇒ C)][1 -bel 2 p (P 2 )bel 2 ⇒ (P 2 ⇒ C)]
In general, with n premises, the formula for type 4 arguments is as follows.

bel 4 c (C) = 1 - n i=1 [1 -bel i p (p i )bel i ⇒ (p i ⇒ C)] (1)
Letting bel i c (C) = bel i p (p i )bel i ⇒ (p i ⇒ C
) be the degree of belief in C due to premise p i , the expression in equation ( 1) is a many-valued disjunction connective aggregating the weights bel i c (C). So it is enough that bel i c (C) = 1 for some p i to get bel c (C) = 1, which is in agreement with the argument type.

It is important to mention that in equation ( 1), a mass function m ⇒ was assigned to each rule p i ⇒ C, assuming independence between them, according to type 4 in Table 1. In type 5 argument, we assign a single mass function m ⇒ to the complete rule with a disjunction of premises ([∨ n i=1 p i ] ⇒ C). The formula resulting from this new mass assignment is given in [START_REF] Bloomfield | Building blocks for assurance cases[END_REF]. In general, the belief in the conclusion for type 5 arguments is as follows, using Dempster rule of combination:

bel 5 c (C) = bel ⇒ ([∨ n i=1 p i ] ⇒ C)[1 - n i=1 (1 -bel i p (p i ))] (2)
where bel ⇒ ([∨ n i=1 p i ] ⇒ C) is the belief that the disjunction of all premises support the conclusion. We stress again that in equation ( 1), we assign one mass function to each simple rule, while in (2), we assign a single mass to a composite rule. So, even though types 4 and 5 are logically equivalent (

∧ n i=1 [p i ⇒ C]) ≡ ([∨ n i=1 p i ] ⇒ C)
, because the assignment of masses is different in types 4 and 5, they produce different results for the belief calculation. The same combination pattern applies to arguments of type 3 in Table 1. It requires all premises be true to justify the conclusion, and a simple support mass is assigned to the implication [∧ n i=1 p i ] ⇒ C. It yields for type 3 arguments:

bel 3 c (C) = bel ⇒ ([∧ n i=1 p i ] ⇒ C) n i=1 bel i p (p i ) (3)
In (2) a multivalued disjunction connective is applied to the degrees of belief in the premises while in (3), it is a multivalued conjunction. In contrast, equation ( 4) below for type 4 arguments supposes a single mass function m ⇒ with masses distributed over the elementary rules p i ⇒ C, assuming n i=1 m ⇒ (p i ⇒ C) + m ⇒ ( ) = 1. The resulting belief in the conclusion is then a weighted sum of the degrees of belief in the premises:

bel c (C) = n i=1 bel ⇒ (p i ⇒ C)bel i p (p i ) (4)
In front of these three expressions (equations ( 1), ( 2) and ( 4)) which result from the same logical form of the argument, a question arises. Which of them is the most appropriate for this argument type? The choices of the assignment of mass function in each equation do not model the same situation. Comparing the first and second formulas, on the one hand (1) suggests that each argument is based on one piece of evidence that could support the whole conclusion and is independent from the other ones. On the other hand, 2 supposes that all such arguments are provided at once by a single source. If we also compare equations ( 1) and ( 4), (1) represents the situation when the elementary arguments are independent, so that a mass is allocated each implication independently of the others. On the contrary, in (4) the belief mass assigned to in one implication affects those assigned to other ones, because, due to the use of a single mass function, the sum of all such masses must be one.

It is important to use each formula giving the belief in the conclusion in the appropriate situation, laying bare the underlying assumptions. For instance, the A-Arg presented in [START_REF] Cyra | Support for argument structures review and assessment[END_REF] is formally defined by ∧ n i=1 (p i ⇒ C), and uses Yager's combination rule to calculate the overall confidence in the conclusion. However, Yager's rule was developed to deal with highly conflicting sources in place of Dempster rule. But the authors of [START_REF] Cyra | Support for argument structures review and assessment[END_REF] do not explain the presence of a conflict between pieces of evidence. Conflicts occur in cases when the intersection between focal sets is empty, which could be the case if masses were assigned to expressions supporting the negation of the implication (e.g., p i ∧ ¬C), or in argument types involving equivalence. In the argument types discussed above, the focal sets resulting from handling argument of types 3, 4, 5 inspired by the selected articles do not generate such conflicts. In particular, the degree of disbelief in the conclusion is always 0 with these argument types.

Lessons learned

As shown in the previous sections, defining an "Argument Type" is a very delicate process. It depends on the assessor's understanding of the argument. Four important issues emerge from this paper:

Formal representation of the argument: The assessor should faithfully translate the informal definition of each argument into a formal one, by choosing the proper logical connectives relating premises to one another (conjunction, disjunction) or between them and the conclusion (equivalence, implication). In order to do so, it is necessary to avoid vagueness and imprecision in the formulation of (informal) verbal definitions and to describe the characteristics of each argument type as accurately as possible. In this paper, two basic types have been laid bare : Those using conjunction of premises (Type 3) and those using a disjunction (Type 4 and 5). Indeed, it is important to know if for instance the truth in one premise is sufficient to ensure the conclusion, or if all premises are necessary to ensure the conclusion.

Using equivalence vs. implication connectives: Implication is the commonly used logical operator for representing arguments supporting a conclusion. However, we have seen that some verbal descriptions used in the literature on safety arguments can be formally translated into equivalences. The equivalence operator should be used carefully because it involves several situations that we may not intentionally want to encounter. Consider for example a conclusion (C) supported by one premise (P). Using the rule (P ≡ C) implies that (P ⇒ C) and that (C ⇒ P ). We saw in Section 3.4 that the second implication is not necessary true. In addition to this, equivalence is also expressed as (¬P ≡ ¬C), in particular, ¬P ⇒ ¬C); this is why using equivalence, disbelief in the conclusion may be different from zero.

Assigning mass functions: It should be clear that the formal definition of the argument types is not enough determine the degree of belief in the conclusion. For instance, when we changed the mass functions definition in the 4 th and 5 th logically equivalent types in Table 1 while using the same combination rule (i.e., Dempster rule), we obtained three distinct formulas [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF][START_REF] Bloomfield | Building blocks for assurance cases[END_REF][START_REF] Cyra | Support for argument structures review and assessment[END_REF]. It is necessary to be sure that the choice of mass assignment reflects as well as possible the situation described in the arguments.

Choosing a combination rule : Changing the combination rule obviously affects the result of uncertainty propagation. So, it is important to choose the right one. However, as we saw in Section 3.4, applying Dempster combination rule is well adapted to computing the overall confidence, because no conflict is met during the combination step using arguments modelled by implication. In that case it is equivalent to Yager's rule. A possible use of this rule could be justified to cope with conflicts between the involved pieces of evidence, in place of Dempster rule. On the other hand, the disjunctive rule is too weak to be applied if one wants to jointly exploit the pieces of evidence in the safety case. A trade-off could be the rule in [START_REF] Dubois | Representation and combination of uncertainty with belief functions and possibility measures[END_REF] which combines focal sets conjunctively when they are consistent and disjunctively when they conflict.

Conclusion

In this paper, we propose a comparative study between some confidence propagation methods in safety cases. We highlight four important elements to be considered in the development of a safety case. First, arguments should be expressed in formal logic. Second, we advocate the use of the implication connective, rather than equivalence, to describe the relationship between premises and conclusion.

Then, we propose a simplified framework to define mass functions attached to premises and arguments. Finally, we argue that Dempster rule of combination should be preferred when the focal sets issued from independent mass functions to be combined do not conflict.

In future works, we plan to experiment an approach that exploits this methodology in an application pervaded with high uncertainties, such as autonomous vehicles. Another issue is the improvement of methods proposed for translating expert opinions into usable numerical values, such as those proposed in [START_REF] Jøsang | Subjective logic[END_REF] and applied in [START_REF] Cyra | Support for argument structures review and assessment[END_REF][START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF]. In this regard, it would also be interesting to develop non-quantitative approaches using qualitative counterparts of belief functions as suggested in [START_REF] Dubois | A possibilistic counterpart to shafer evidence theory[END_REF].

Fig. 1 .

 1 Fig. 1. GSN main components.

Table 1 .

 1 Formal definitions of arguments. Note that argument types 4 and 5 are logically equivalent (∧ n i=1

Table 2 .

 2 Consistency between argument types and combination rules.

Authors

Argument types Combination rules Consistency Cyra and Gorski [START_REF] Cyra | Support for argument structures review and assessment[END_REF] NSC As can be seen from Table 2, several combination rules are proposed to obtain the overall confidence in the conclusion. But, none of the reviewed papers clearly justifies its choice of the applied method, nor does it lay bare the underlying independence assumptions. Also, some of the proposed expressions are not consistent with the verbal definition. For instance, in [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF], the type Alternative argument is used when several independent premises support the conclusion. The formal definition induced is : ∧ n i=1 (p i ⇒ C) (Table 1). However, the authors only consider the confidence in the premises (also called trustworthiness, in [START_REF] Wang | Confidence in safety argument-An assessment framework based on belief function theory[END_REF]), but they did not consider the confidence in the relation between them and the conclusion (the rule). A possible formula that takes into consideration this definition could be equation [START_REF] Ayoub | Assessing the overall sufficiency of safety arguments[END_REF].

Consider the example of a conclusion (C) separately supported by two premises p 1 and p 2 , which refers to an argument of type 4 in Table 1, i.e., (p 1 ⇒ C)∧(p 2 ⇒ C). We develop this example below. For other argument types, the calculation follows the same method. The confidence assessment process is measured through two parameters. The confidence in premises is modelled by mass functions m pi and the confidence in the support of the the conclusion by each premise (the rules) is modelled by the mass function m ri . Then, we apply Dempster combi-