Cyrille Comar
email: comar@adacore.com

Jérome Guitton
email: guitton@adacore.com

Olivier Hainque
email: hainque@adacore.com

Thomas Quinot
email: quinot@adacore.com

J Ér Ôme Guitton

Structural Coverage Criteria for Executable Assertions

Keywords: Structural coverage, Functional coverage, Coverage criteria, DO-178, Certification, Formal verification, Assertions, Contract Based Programming

published or not. The documents may come

L'archive ouverte

Introduction

A few programming languages promote the notion of contract based programming and offer specialized constructs to support this paradigm. A seminal representative of such languages is Eiffel with its Design by Contract principle [START_REF]ECMA-367: Eiffel analysis, design and programming language[END_REF], [START_REF] Meyer | Applying "design by contract[END_REF]. Ada, and more specifically the Ada 2012 revision of the language, is another example, featuring pre and postcondition aspects, type invariants, as well as new syntactic constructs allowing conditional control within expressions [START_REF]Information Technology -Programming Languages -Ada[END_REF]. Programming with contracts is essentially based on assertions, Boolean expressions expected to always yield True, embedded in dedicated constructs at various spots of the program. Subprogram pre and postconditions, for instance, embed assertions on properties expected to hold when entering or exiting the subprogram, respectively. Type invariants are assertions that should hold for each object of the type at any time, except potentially while it is being updated. Such assertions can be viewed in different ways: They can first be considered as a debugging aid, since they help reduce the distance between the place in the code where an error initially occurs, and the point where it causes an externally noticeable effect and can be detected. They can also be viewed as a way of clarifying responsibilities: a subprogram precondition expresses the constraints on the kind of situations the routine is able to deal with: it is the responsibility of the caller to ensure that the constraints are respected. Conversely, a postcondition expresses the properties that the routine is guaranteeing, and on which the caller can rely after the call. Finally, an emerging way of viewing assertions, and in particular pre-and postconditions, is to consider them as a formalization of the requirements of the associated subprogram. For instance, we can express informally the requirements for a square root routine to be: the routine behavior is only defined for positive or null floating point inputs, the square root is the inverse of the square (square(sqrt(x)) = x), and we expect a maximum error of 10 -2 on the result. This can be expressed formally with pre-and postcondition assertions on the subprogram, as in the Ada 2012 example declaration below: function SQRT ( X : F l o a t ) r e t u r n F l o a t with Pre => X >= 0 , Post => abs (SQRT' R e s u l t * SQRT' R e s u l t -X ) <= 0 . 0 1 ;

As can be expected, standards for developing critical software such as DO-178C for civil avionics, or EN-50128 for railway, require a fair amount of verification and testing during development cycles. They also require activities showing the coverage and completeness of those verifications. DO-178C defines two families of such coverage objectives:

• Functional coverage, which consists in checking that the system behaves as it should, or in other words that all the functional requirements have been verified, and that each of them has been sufficiently exercise to take all aspects of the requirement into consideration;

• Structural coverage, which consists in verifying that the program code has been exercised with sufficient exhaustiveness during the testing campaign. Specific structural criteria such as DECISION COVERAGE or MCDC provide an exhaustiveness metrci based on a close observation of the Boolean expressions that have an influence on program control flow.

This paper explores the implications of conducting coverage analysis on code that uses assertions, starting from the following questions:

• Are the standard structural coverage criteria adapted to code containing assertions?

• Can the structural coverage of assertions help assess functional coverage?

Before discussing these questions, we first need to understand why it can be useful or necessary to keep assertions in the final executable. As a matter of fact, tools usually let the user choose whether assertions will be part of the executable code or not, and it is common practice to enable assertions and other checks of various kinds for testing purposes only, and then to disable them for the final executable to be put in production, in which case pure structural coverage analysis of assertions is less of an issue. Enabling assertions during testing is a good idea because it makes the testing campaign more efficient: potentially elusive problems such as uninitialized variables or improper aliasing have better chance to get detected. On the other hand, keeping assertions enabled in the final executable is not always the best choice, especially when no recovery mechanism is in place: innocuous errors might cause the program to stop, whereas they would have remained unnoticed in the absence of assertions. Nevertheless, assertions can be used to provide the guarantee that the program is doing what it is supposed to do, and in some situations it is preferable to stop execution rather than continuing executing a program turned wild. In other words, keeping assertions live in the final system is a legitimate option, and is even necessary in some circumstances, when error recovery is taken care of and it is essential for the program to do only what it was designed for and nothing else.

Coverage criteria that make sense for assertions are therefore needed in situations where assertions remain in the executable code, or if they are used to help functional coverage assessment. As a result, in the majority of cases, DECISION COVER-AGE, and MCDC even more so, are not adequate criteria for assertions. This is actually unsurprising since, in essence, assertions aren't decisions by our definition, as they are expected never to evaluate False, whereas decisions are assumed to be legitimately allowed to take both values True and False.

Ignoring assertions for coverage purposes is not a viable option either: even a single assertion might check a wide spectrum of possible cases, and having a means of measuring how extensively this spectrum was exercised by a testing campaign is a necessity.

In addition, we believe that some structural coverage on assertions can help functional coverage analysis, when assertions are used to capture subprogram requirements.

We therefore observe that specific coverage criteria to be applied for the coverage analysis of assertions need to be defined. The remainder of this paper identifies possible tracks and illustrates how functional coverage can be helped in the process. The discussion is organized as follows:

In section 2, we propose definitions for three increasingly exhaustive criteria for the coverage of assertions, which could correspond to the three certification level of DO-178C that require coverage analysis. In section 3, we present examples of assertions, and introduce tri-state truth tables that we will use in the following sections for illustration purposes. Sections 4, 5 and 6 provide insights on the way to interpret the definitions on an example assertion, and comment on the sets of tests that can be used to achieve the respective criteria. Section 7 then shows how the definitions allow the nesting of decisions within assertions.

We then examine a few notesworthy aspects of the proposed criteria: section 8 provides a quantitative complexity analysis, giving a notion of the cost associated with achieving each criterion in terms of amount of testing it requires. Section 9 discusses situations where it may be impossible to satisfy some of the criteria, in particular for assertions which contain coupled operands. Finally, section 10 relates our tracks of thought to existing work, before moving to a conclusion where we summarize the most important points and discuss possible perspectives of further investigations.

Proposal of specific coverage criteria for assertions

We propose three levels of coverage criteria for assertions. These three levels are intended as companions to the three criteria defined for regular application code in the DO-178C standard (namely Statement, Decision, and MCDC coverage, depending on the certification level).

DO-178C defines the notion of condition to designate operands within decisions. We will reuse this term to designate operands within assertions as well.

For reasons exposed later on, when we need to distinguish conditions within a Boolean expression, the only operators we consider are those with short-circuit semantics such as the && and || in C, or and then and or else in Ada, as well as Boolean-valued IF-expressions (equivalent to the C ternary operator ?:). Logical negations have no influence on expression decompositions for our purposes.

A Boolean expression built from elementary Boolean conditions combined with these operators can be modeled as a Binary Decision Diagram (BDD), and an evaluation of such an expression can then be understood as a traversal of this BDD.

Note that Boolean subexpressions may appear within the considered elementary conditions, for example as formal parameters in subprogram calls, or as the expression that conditions a non-Boolean-valued IFexpressions. Such nested Boolean subexpressions do not directly determine the traversal of the BDD, and are therefore out the the scope of the coverage analysis for the outer assertion (of course they are subject to a separate coverage discussion in terms of the usual structural coverage criteria, as detailed in section 7).

On this ground, here are the three levels of criteria we propose:

Assertion True Coverage (ATC)

The expression as a whole has been evaluated True at least once.

Assertion True Condition Coverage (ATCC)

All the expression conditions have been evaluated at least once as part of a complete expression evaluation to True. Different conditions may have been evaluated as part of different outer expression evaluation instances.

Assertion True Path Coverage (ATPC)

All the paths leading to a True outcome within the expression's BDD were taken.

The following sections provide more detailed insights on what satisfying the criteria mean, then explore a few properties of interest regarding the criteria. We will be relying on a simple use-case example to illustrate most of the points.

Example assertions and tri-state truth tables

To help illustrate various points in the following sections, we will use the following example use-case for assertions: the doors of an elevator are controlled by a simple Ada program, and we focus on the subprograms responsible for locking/unlocking the doors.

An elevator door can be in three possible states:

• Locked: the door cannot be opened;

• Closed: the door is closed but not locked, i.e. it can be opened by a user;

• Opened: the door is opened. It cannot be locked; only a closed door can be locked.

Only two transitions between these states are invalid: going directly from Locked to Opened, and the other way around.

To enforce this constraint, the operations to lock the door is effective only if the door is Closed; in the other cases, it does nothing. A natural Nb Errors indicates the number of errors that have been generated in the operation ; a failure to lock a closed door is one of the possible errors, so at least one error is returned if the final state is not Locked when the original state was Closed. In Ada 2012, this could be expressed by a postcondition: For the sake of the example, the unlock operation is not quite symmetrical: trying to unlock a door that is not locked also results in an error, which allows a simpler postcondition:

procedure In both cases, postconditions express the invariants that the corresponding procedure bodies enforce. Forcing them to False during the test campaign would mean deliberately introduce bugs in the procedure code, which would be purely artificial. Keeping them in the deployed application would still be useful: the violation of any of these assertions means that the program cannot guarantee the safe use of the elevator anymore and the system would stop it and switch to a safe recovery mode: e.g. stop the elevator where it is and call for manual maintenance.

To help illustrate our criteria on this example, we will resort to tri-state truth tables to synthesize the way expressions get valued. The True and False possible values of the conditions or of the expression outcome will respectively be denoted with "T" and "F", and condition columns have an extra "x" possible state for situations where the condition evaluation is short-circuited. Each line of the table is called an evaluation vector and is assigned a unique number that can be used to designate it later on.

For the Unlock Door postcondition, using abbreviations like Pre Locked to denote "the door state on entry was Locked", Closed to denote "the door state on exit is Closed", and Error to denote "At least one error has been returned", we have an expression with three conditions of the following form and its associated tri-state truth table :   ( Pre Locked and then Closed )

or else E r r o r # Pre Locked Closed Error Outcome 1 F x T T 2 T F T T 3 T T x T 4 F x F F 5 T F F F

ATC user level characterization

From the truth table of our example assertion, any of the vectors #1, #2 or #3 is enough to satisfy ATC on its own, as they all yield a True outcome for the expression as a whole. This is pretty weak on the functional coverage front.

The other two criteria are stronger and deserve each a more elaborate discussion:

ATCC user level characterization

ATCC is explicitly referring to complete expression evaluations as those contributing to the criterion fulfillment. This denotes evaluations that terminate without unexpected interruptions, typically by possible exception occurrences during the tests. Indeed, evaluations that don't terminate yield no value for the expression as a whole, so we can't tell whether the assertion was satisfied. These are implicitly excluded by ATC already. The important extra point about ATCC that deserves being explicit is that we consider the incomplete set of valued conditions as not contributing to the criterion.

To illustrate what sets of test may be used to achieve ATCC, let's consider the Unlock Door postcondition and the associated truth table again. We can see that evaluation #2 yields True and evaluates all the conditions, so is sufficient to achieve the criterion on its own. #1 alone is not enough since the evaluation of Closed is short-circuited, and #3 alone is not enough either since the evaluation of Error is short-circuited. The definition allows the combination of #1 and #3 to fulfill the criterion, still, as they both yield True and evaluate all the conditions overall. This is immediately stronger than ATC from the functional standpoint: Indeed, a single test vector allows satisfying the criterion alone: vector #2 which corresponds to Pre Locked True, Closed False and Error True. This is a very interesting case, which checks that Error is correctly set on a failed legitimate attempt to unlock a door. If testing doesn't check this specific case, it has to check two cases as a counterpart; one verifying that Error is correctly set on invalid attempts to unlock a door that was not locked on entry (vector #1), and one verifying a situation where the door state transitions from Locked to Closed as expected in nominal conditions (vector #3).

ATPC user level characterization

The use of the expression BDD for ATPC makes it potentially hard to understand from a user point of view. This is where focusing on operands combined by short-circuit operators helps. Indeed, in this case the set of BDD paths leading to a True outcome correspond to the set of lines with a True outcome in the tri-state truth table, so figuring out which tests need to be exercised to fulfill the criteria is straightforward from the table.

For our example postcondition on Unlock Door, we can immediately see from the associated truth table that achieving ATPC requires 3 tests, going through all of the first three vectors, which are the ones for which the expression evaluates True. The gain in strength of functional coverage compared to ATCC is significant, as the criterion requires exercising all the cases of relevance.

Incidentally, however, we notice that Error is not evaluated as part of vector #3. It might seem surprising not to evaluate a possible error condition in a vector that contributes to a structural coverage criteria, and here could be an indication that the postcondition might be imprecise in conveying all the functional requirements and might need to be improved.

This last observation, together with the previous comments, illustrates that thinking in functional terms as part of a structural analysis process can be meaningful and of real interest. It so appears that structural coverage analysis on contracts can be of significant potential value for functional coverage discussions.

Decisions within assertions and the influence of coding styles

While assertions aren't decisions by definition (an assertion is assumed to only ever evaluate to True throughout testing, whereas a decision can be expected to evaluate True and False over successive tests), assertions can embed nested decisions that might need to be analyzed on their own. This influences the amount and kind of testing required, so is useful to keep in mind when reasoning about the meaning and characteristics of criteria. Here, we present an example to illustrate the point and show how differences in coding style can influence the testing requirements as well.

Consider the postcondition of the Lock Door subprogram in our example. The assertion is of the form: On the other hand, the inner IF-expression is not Boolean-valued, and so the corresponding two cases do not directly appear as nodes in that BDD.

Complexity assessment

An interesting question is how many evaluations (tests) are needed to satisfy our criteria. The regular MCDC criterion, for example, is known to require no more than N+1 tests for a decision with N conditions. What would be an upper bound for assertions? For ATCC, the complexity is also linear: no more than N tests are required for an assertion with N conditions. Indeed, for any well-formed assertion, each condition is reachable and from this condition there exists a path to outcome True in the BDD. So for each condition we can provide a test that evaluates the considered assertion and exits on outcome True. Taking one such test per condition gives N tests. However, for ATPC, the complexity can be exponential, depending on the topology of the BDD. In the study of equivalence between object branch coverage and MCDC that [START_REF] Comar | Formalization and Comparison of MCDC and Object Branch Coverage Criteria[END_REF] provides, a pathological case was presented where three evaluations were enough to cover an arbitrarily complex decision for object branch coverage; the same case also shows an exponential complexity for ATPC. Consider the following set {E n } n∈N of Boolean expressions:

• let E 0 be a simple condition expression, with its condition denoted C 0 ; then define:

• ∀ n > 0, E n = (E n-
C 0 C 1 C 1 T T F T F T F T F (a) C 0 C 1 C 1 C 2 C 2 T T F T F T F T F T F T F (b)
Figure 2: Exponential complexity for ATPC This example illustrates that exponential complexity comes from multi-path nodes (nodes with more than on predecessor in the BDD). On the contrary, when the BDD is a tree, the complexity is linear: the number of tests needed to cover it for ATPC is at most equal to the number of conditions. This is also the exact amount of tests needed in the case of an assertion that contains only or else operators.

[7] provides a case study on two industrial projects showing that multi-path nodes in BDDs are quite rare (less than 1% of decisions). A similar case study would be needed for assertions, but this suggests that assertions where the complexity of ATPC would explode are likely quite rare. In other words, we expect BDDs to be trees in the vast majority of cases, and ATPC is comparable to MCDC in this configuration as covering an expression for ATPC is exactly the same as taking only the True valuations of a MCDC coverage.

Achievability considerations

A known issue with coverage criteria on Boolean expressions is the potential inability to achieve coverage in the presence of coupled conditions. This is in particular what lead to the refinement of Unique Cause MCDC into Masking MCDC. The same question holds for coverage criteria on assertions. Amongst the criteria that we defined in this paper, only ATPC can be impacted by coupled conditions. In the general case, it is possible to build assertions with coupled conditions on which ATPC would not be achievable. The question is whether these cases could be found in a real industrial system. First, it must be noticed that such cases do not make sense in the absence of multi-path nodes. Indeed, with a tree BDD, not being able to cover a particular path to True means that one of the conditions cannot be changed, which would mean that it is useless and that the assertion is ill-formed.

On the other hand, as seen in the previous section, multi-path nodes in decisions seem to be quite rare in industrial application. To have an impact on achievability, these rare expressions also have to contain coupled conditions, and these coupled conditions have to forbid a path to outcome True. This makes this problematic cases even less likely to appear in real-life applications. It would therefore be manageable to handle these with justified exemptions without increasing too much the workload of the tester.

In that context, we have identified one recurring pattern that requires specific attention. It consists in the elaboration of an assertion that distinguishes different subsets or states, for each of which a separate expression must evaluate True, such as:

Case 1 : expression B must be True;

Case 2 : expression C must be True.

An example of this pattern is the postcondition of operation Lock Door in the elevator example. In this postcondition, Case 1 is when the door is closed before hand and Case 2 is the other cases. Depending on the way the assertion is expressed, some of the paths may be impossible to exercise in which case ATPC would be unachievable. The problem lies in an implicit coupling between the predicates denoting each case. Indeed, in general the cases distinguished in such a requirement are mutually exclusive.

If the above requirement is formally expressed in disjunctive normal form (DNF):

( Case 1 and then B ) or else ( Case 2 and then C) then ATPC cannot be achieved, because the implicit coupling makes it impossible to exercise some paths in the expression (which involve Case 1 and Case 2 both being True). In this example, the expression's truth table contains:

Case 1 B Case 2 C Outcome T F T T T and ATPC cannot be achieved because there's no way to get both Case 1 and Case 2 true as part of the same evaluation. In BDD terms, the path outlined in figure 3 can never be taken. For MCDC, the issue of coupled condition has been handled by refining the coverage criterion into the Masking MCDC variant; in the case of assertions, something like a masking ATPC could be defined formally but this criterion would be harder to understand by testers. Here, we would consider an alternative solution: rewrite the assertion to eliminate multi-path nodes. Indeed, note that in the context of formalizing the discussion of two mutually exclusive states, the unreachable path does not make any sense, as it first takes a branch denoting the first case, and then falls through to examining the second case. This is a consequence of the DNF formalization failing to capture the notion that Case 1 and Case 2 form a partition of the state space. Conversely, using a notation that does capture this fact yields a BDD where this nonsense path does not exist. For example, using Ada 2012 conditional expressions, the discussion of two cases can be denoted as: This notation retains the semantics that the two cases discussed are mutually exclusive: if Case 1 is examined, there is no point in examining Case 2. With this additional semantic information retained, ATCC and ATPC become equivalent in this case, and are reached using two tests:

Case 1 B Case 2 C Outcome T T x x T F x T T T
In addition, when the discussion of cases is thus expressed as a chain of conditional expressions, ATPC can be simply understood as exercising each of the distinct cases, or states. In other words, when a requirement consists in a partition of input space, and the requirement is expressed with a notation such as the above that preserves the notion of that partitioning, then ATPC essentially consists in separately covering each subset in the partition.

Note that this is precisely the form that has been presented for the postcondition of Lock Door. The SPARK 2014 language also introduces a specific notation for this pattern in the form of the Contract Cases aspect, that could have been used as follows: In addition to expressing a postcondition equivalent to the above chained conditional expressions, this also states that the set of cases are both disjoint or complete.

Related work

As the coverage level required on Boolean expressions is a typical key differentiator between assurance levels in various certification standards, there are lots of publications treating of Boolean expressions in coverage analysis contexts.

The certification standards themselves, such as [START_REF] Rtca | Software considerations in airborne systems and equipment certification[END_REF], [START_REF] Rtca | Software considerations in airborne systems and equipment certification[END_REF] for civil avionics, or [START_REF]Railway applications -Communication, signalling and processing systems -Software for railway control and protection systems[END_REF] for railway, are of course a primary reference. A very large number of related papers and documents were written over the years as the experience of using the criteria in real projects built up. Here are just a few examples: [START_REF]What is a Decision in Application of Modified Condition/Decision Coverage (MC/DC) and Decision Coverage (DC)? Position Paper 10[END_REF] clarifies some aspects regarding possible interpretations of the DO-178CB standard, specifically on the notion of "decision". [START_REF] Chilenski | An Investigation of Three Forms of the Modified Condition/Decision Coverage (MCDC) Criterion[END_REF] defines possible variants of the MCDC criterion, amongst which masking MCDC was eventually accepted as valid alternative in avionics projects to handle issues with coupled conditions [START_REF]Rationale for accepting Masking MCDC in certification projects[END_REF]. [START_REF] Hayhurst | A Practical Tutorial on Modified Condition/Decision Coverage[END_REF], [START_REF]Software Verification Tools Assessment Study[END_REF] illustrate what the various criteria can mean in practice from a user or tool qualification perspective. [START_REF] Chilenski | Applicability of modified condition/decision coverage to software testing[END_REF] performs a thorough study of MCDC's main characteristics and relationships with other criteria. [START_REF] Sergiy | Formalization of software testing criteria using the z notation[END_REF] proposes a formalization of coverage criteria in Z, and other authors proposed improvements to the traditional decision related criteria, improving their problem detection strength while remaining linear with the complexity of decisions [START_REF] Sergiy | Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing[END_REF], [START_REF] Sergiy | From MC/DC to RC/DC: Formalization and Analysis of Control-Flow Testing Criteria[END_REF].

All these revolve around the notion of decision in DO-178C parlance, however. To our knowledge there is no prior publication on the specific set of issues that this paper proposes to explore, with a focus on assertions and their possible connection with functional coverage. Parallels of interest are nevertheless possible with some connected topics.

In particular, if we consider coverage analysis as a mean to determine if a testing campaign exercised enough of a program logic, a parallel is possible between the concerns we address here and research on the testing complements to formal methods. Indeed, there is an strong duality between aiming at the definition of a useful subset of tests needed to exercise a component correctly, based on formal representations, and verifying that enough testing was achieved thanks to assertion coverage analysis on the implementation code.

[1] and [START_REF] Stocks | A framework for specification-based testing[END_REF], for example, introduce a framework where a formal representation of a component in Z is used to derive partitions of its Valid Input Space (VIS) so a single test within a given partition is representative of the entire partition. If one translates the VIS partitioning rules as preconditions, then a set of tests derived from the partitioning process should in principle match or at least encompass the set of tests required to achieve ATPC. As another example [START_REF] Dick | Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods[END_REF] presents techniques based on expression DNF to automate the partitioning and test sequencing processes.

Conclusion and perspectives

In this paper, we discussed the structural coverage analysis of assertions (Boolean expressions expected to always yield True at various points of a program), and the necessity for specific coverage criteria. We explained why we believe such an analysis is of use in an application certification context, and proposed the definition of three coverage criteria as a basis for further discussion.

One aspect of interest is the idea that some categories of assertions can be understood as a formalization of a program's functional requirements. We have provided examples that show how structural analysis on contracts can be interpreted in a meaningful way in functional terms, and thus provide a valuable basis for a functional coverage analysis.

We believe there is a lot of room for further work on this topic, in particular to refine the definition of relevant coverage criteria. Gathering more data from real use cases on industrial projects would help assessing their actual usefulness, and would certainly foster improvements. It is also quite possible that defining several families of criteria could be relevant to address different categories of assertions, within the context of contract based programming. For instance, we can perceive that preconditions are very different from postconditions, and might thus warrant distinct criteria.

Finally, assertion coverage turns out to be a common notion in the hardware design verification area, in association with so-called Assertion Based Verification (ABV) systems [START_REF] Dahan | Combining system level modeling with assertion based verification[END_REF]. It might be interesting to investigate if some of the ideas that led to the definition of an entire methodology in the hardware domain could apply to the software area. This would be kind of a symmetrical idea of the one used in [START_REF] Sreekumar | A Probabilistic Analysis For Fault Detectability of Code Coverage Metrics[END_REF], where the authors note that a categorization of software faults works pretty well in the microprocessor validation domain as well, and leverage this similitude.

procedure

  Lock Door ( E : i n out E l e v a t o r T y p e ; N b E r r o r s : out N a t u r a l ) with Post => ( i f D o o r S t a t e ( E ' Old ) = Closed then N b E r r o r s >= ( i f D o o r S t a t e ( E ) = Locked then 0 else 1 ) else ( D o o r S t a t e ( E ) = D o o r S t a t e ( E ' Old ) ) and then N b E r r o r s = 0 ) ;

  Unlock Door ( E : i n out E l e v a t o r T y p e ; N b E r r o r s : out N a t u r a l ) with Post => ( ( D o o r S t a t e ( E ' Old ) = Locked and then D o o r S t a t e ( E ) = Closed ) or else N b E r r o r s > 0 ) ;

(Figure 1 :

 1 Figure 1: BDD for Lock Door postcondition

Figure 3 :

 3 Figure 3: BDD for (Case 1 and then B) or else (Case 2 and then C)

ifFigure 4 :

 4 Figure 4: BDD for if Case 1 then B elsif Case 2 then C

  Note that short-circuit Boolean operators and then and or else are really but a specific cases of the more general Boolean-valued IF-expression construct: A and then B is equivalent to (if A then B else False), and A or else B is equivalent to (if A then True else B). This construct exactly captures the elementary building block in BDDs, which model the way decisions actually are evaluated in generated code: the condition at each step selects a path ultimately leading to a True or False outcome. In assertion contexts, paths leading to False are irrelevant, and do not play a role in the coverage analysis. Conversely, a non-Boolean-valued IF-expression just selects a value that will intervene in some other outer expression such as a relational operator or function call: either direction of the condition might yield a True or False outcome; neither direction can be eliminated in an assertion context on the basis that only True outcomes are relevant. Consequently, the relevant coverage criteria for an expression that controls a non-Boolean IF-expression are the usual DECISION COV-ERAGE and MCDC.

  [START_REF] Carrington | A tale of two paradigms: Formal methods and software testing[END_REF] and then C n ) or else C n , with C n , C n independent from each other and from any condition in E n-1 .

	Figures 2(a) and 2(b) show the BDD of E

1 and E 2 . For n > 1 it can be seen there that the two True outcomes of E n-1 both reach C n in E n and have then two different paths to True; so the number of paths to True in E n is more than twice the number of paths to True in E n-1 . This means that one would need at least 2 n tests to cover E n for ATPC.


Thierry Le Sergent

François-Xavier Dormoy

Benefits of Model Based System Engineering for Avionics Systems 1 Benefits of Model Based System Engineering for Avionics Systems

Keywords: Model Based System Engineering, Software Engineering, SysML, Domain Specific Language, SCADE, Avionics System, Aircraft Braking System

Introduction

Avionic system design is an extremely complex activity due to:

-Different concerns from different teams:

o Complexity of functions to realize o Hardware and software redundancies to manage safety considerations o Communication protocols o Complex hardware network with configuration switches, o Etc. -Amount of data to manage: 1,000s of data -Resource sharing principle (CPU, network, …) Current methods to manage system engineering complexity rely on refinement levels and view-points. Industries promote ICDs (Interface Control Documents) as a contractual means to assign the development of system components. These are basically large databases that gather the result of system architecture design.

In the domain of safety critical software, the benefits of a model based approach are well established. Now, using an example of avionics architecture, we will show how Model Based System Engineering (MBSE) brings many benefits when the tools are suited for system designers and applied to solve industrial challenges.

Proponents of MBSE provide strong arguments for improving the efficiency of complex system development, promising to achieve at least the same level of quality in a shorter time. However, this gain in efficiency must be proven. This paper details the way a realistic complex avionics system can be designed efficiently using a MBSE tool, with hundreds of data passed through ARINC 429 and ARINC 664-P7 messages. A classical methodology is followed to manage the different levels of concern:

-Functional architecture o Functional data flow communications -Software architecture o Function organization into software components o Software message definition and propagation between the components -Platform hardware architecture o Definition of buses, switches, and computing units o Software to hardware mapping o Virtual link definition for the ARINC 664-P7 communication -Software design, code generation and verification with SCADE Suite [START_REF]Esterel technologies SCADE products[END_REF] In order to sustain industrial deployment as a cost-effective MBSE tool, the following must be addressed:

-Interoperability -By conforming to a standard, such as SysML [START_REF]OMG Systems Modeling Language (OMG SysML)[END_REF], users avoid the risk of vendor lock-in and can integrate with other technologies. -Usability -In order to overcome reluctance to change, the tool should speak the language of system engineers rather than forcing engineers to force their design into an awkward formalism.

Avionics system case study

For this case study, Dassault Aviation provided a simplified representative example of a Braking System, based on a COM-MON architecture. Principles of the COM-MON design are not detailed but focus is made on the ARINC 664-P7 and ARINC 429 communications between the COM, MON and other systems.

-At the functional level, COM and MON interact with 9 sub-systems. 175 functional data are considered.

-At the software level, COM and MON partitions are respectively interacting with 12 partitions. 14 ARINC 664-P7 messages and 48 A429 messages are defined. -The platform level contains 4 Processing cores (CPU), 4 Switches, a dual A/B ARINC 664-P7 network, and 30 Virtual Links (VL).

Based on this example, we realized a complete retro-fit in SCADE System through the following steps:

-Description of the entire architecture (Functional, Software and Platform) -Production of the application ICDs -Management of data consistency checks across the complete application -Management of Virtual Link paths to facilitate switch configurations -Analysis of message allocation with respect to network bandwidth -Synchronization of the system architecture with the software design Screen shots and details of the complete example are provided after we have introduced all the tool features that enable efficient support of the design method.

Proposed Model Based Engineering Method and Tool Support

As introduced in the first section, a traditional system design approach is used, relying on several abstraction layers: functional, software (sometimes called "logical"), and platform. Our approach is unique in how it defines and manages the relations between these levels of abstraction.

The following technical means are hereafter detailed:

-Allocation and interface specification, relying on data management -Customization of SysML objects -Analysis of the model, in particular to produce the Interface Control Documents (ICD).

Allocation and interface specification

When designing a system in several abstracting layers, consistency and completeness of each layer must be ensured. The difficulty comes from the fact that the abstraction levels are not a simple hierarchical decomposition. The functional, software, and hardware views are all hierarchical, but with a different hierarchy.

The relationship between the different layers is called projection. SysML comes with a dedicated construct, allocations, to support this. Projections provide a straightforward way to show the realization of a function by a software component, and show how a software component is run by a hardware component.

Before focusing on the interface allocations themselves, it should be noted that the intention of a projection is to specify precisely which item shall be supported by which item. The projection must take into account that blocks may be instantiated several times. The difficulty arising from the hierarchical instantiation is solved in SCADE System though a block replica mechanism detailed in [START_REF]Data Based System Engineering: ICDs management with SysML[END_REF]. The result of the replication mechanism is that each object from the real world is represented with a dedicated object in the model. This replication mechanism is reused for the data objects presented below.

Projection of the component interfaces can be realized in the same simple way as for block components. But this does not lighten the burden of making all interfaces consistent with each other. Let's consider the following case:

-A function F produces data D, for several other functions defined in the functional decomposition.

-Each function is allocated to a software component, some sharing the same component, others not.

ERTS 2 2016 Benefits of Model Based System Engineering for Avionics Systems 3

-The software components exchange messages in order to transmit the functional data.

It is easy to specify that the software component S supporting F shall produce a message M carrying D. But what about the other sides of the communication? The message M must be sent to all software components that support a function receiving data D. This rule must be maintained whatever the data propagation and function allocations, something that may evolve during the design process.

Another consideration is that ARINC 429 and ARINC 664-P7 messages can carry several data elements. The designer may define either one message carrying several data to other software components, even if some data are not required by all the message recipients, or to define several messages. All these challenges are supported by a concept of data.

Data management

SCADE System comes with an original and powerful means to specify the interface allocations efficiently. It relies on data objects that can be structured and propagated.

The data propagation mechanism first published in [START_REF]Data Based System Engineering: ICDs management with SysML[END_REF] is summarized here:

-Data are implemented as SysML blocks, allowing SCADE System to conform to the SysML meta-model, but managed as data in the tool. -Data are propagated along block ports and connectors thanks to a dedicated feature of the tool -Propagation of a data D out of a block B through one of its ports consists in the creation of a data proxy in the parent blocks instantiating B. -All proxies are connected as a chain; the tool allows managing the data attributes (feature detailed in section 3.3) whatever the selection of one proxy of the chain.

This mechanism brings two important benefits. First, it allows handling a complete "path" through a block hierarchy and connections from a single data element. Second, it allows managing thousands of data, each broadcasted or multi-casted in a straightforward way by the designer, without graphical scalability issues by avoiding the creation of numerous ports and connectors (the proxies are automatically created from path selection).

Individual data are structured thanks to an internal model transformation:

-Data structures are defined with classical structured types -Applying a structured type to data replicates the structure inside of the data definition. This allows for each data to have its own individual fields.

Structured data is an ideal means to model messages; the message fields represent place-holders for the functional data. Simple allocations of functional data (defined at the functional abstraction layer) to a field of a structured data message represents the fact the message carry the functional at a certain place in the message. This would not be possible without the internal replication of the message type because the field of type would be shared by all the messages sharing the same type.

Allocating a propagated functional data to a propagated message data implements the interface allocations between the abstraction layers.

An additional feature allows managing the user interface scalability: There may be several thousand of functional data, and data messages in a model. Managing the allocation between the different levels of abstraction is challenging for the usability perspective of a graphical tool. Even a traditional list of objects can be cumbersome for the users. SCADE System IDE comes with a customizable filtering mechanism that restricts possible candidates to correct allocations and propagation. The principle is the following:

-A checking rule verifies that a functional data FD propagated from function FA, allocated to Component CA, to function FB, allocated to component CB, is allocated to message data MD that goes from CA to CB. This check takes into account both the possible multiple propagation target of a data, and possible multiple allocations to messages to handle redundancies. -In addition to automated verification and report generation at the end of the design, the checking rule is used dynamically by the UI to filter out the allocation and propagation possibilities that would lead to a violation of the rule. That way, the UI exposes a much shorter list of possible selections, and correct designs are realized much faster.

This mechanism extends very easily: users can program their own verification rules from the model API, and use them both for final batch verifications, and as filters in the allocation and the data propagation interfaces.

ERTS 2 2016 Benefits of Model Based System Engineering for Avionics Systems 4

DSL vs. SysML: Configuration of the SCADE System tool

The method presented above only requires blocks, ports, connectors, data, and structured type objects. However, these constructs fall short of easily addressing a specific domain. The ability of a tool to meet the needs of domain expert engineers is a key success deployment factor, which must go beyond these few generic SysML objects.

There are traditionally two competing approaches when it comes to domain-specific system modeling:

 "Pure" Domain-Specific Languages (DSLs)  Customizations of generic modeling solutions, e.g. UML with profiles such as SysML Proponents of the first approach appreciate the total freedom that DSLs provide in order to best fit actual domain concerns, without incurring the cost of supporting legacy UML peculiarities. Proponents of the second approach claim that reliance on standards such as UML provide better long term sustainability and interoperability.

SCADE System stands out with an original hybrid approach that combines the best of both worlds: While the internals of SCADE System rely on UML/SysML and profiling (therefore providing full standard support and interoperability), SCADE System still presents itself as a domain-agnostic system modeling language and toolset, via a pure DSL "virtual layer" implemented transparently on top of UML and SysML. This layer is naturally extended to accommodate domain-specific needs without starting from scratch: The domain specialist simply designs a domain-specific language as a meta-model that specializes SCADE System's domain-agnostic metamodel. Additional information is conveyed by appropriate attributes in specializing meta-classes and relationships among them; additional constraints imposed by the domain are enforced by redefinitions of existing relationships.

SCADE System transparently handles the intricacies of UML profile management and dynamically adjusts its interface to the domain-specific "configuration", offering new modeling constructs (in toolbars, property pages, etc.) while forbidding others according to constraints of the domain. Moreover, models based on a domain configuration can be manipulated via a "pure" API derived from the domain meta-model, not UML concepts and stereotypes.

Figure 1 below shows the tool workflow in practice: the domain specialist designs the domain meta-model; from it, a "configuration plug-in" is automatically generated. By loading this plug-in file, SCADE System is transformed into a Domain Specific tool with the customized "creation palette" and object properties. Similar meta-models are provided for ARINC 664-P7 and CAN messages. The same technique is used to define all meta-classes needed at the platform definition layer, with the physical ports, switches, etc.

ICD production

Now that we have described the data management process, Interface Control Documents can be generated from the model. These Excel sheets are needed by many different development teams, each requiring different information, presented in the way they expect. For example:

-Partition table -Messages definition with their parameters -Messages source and targets with ARINC 664-P7 ports, transmission rate, length, etc.

-ARINC 664-P7 Virtual Links definition Each table being specialized for a specific usage, the tool should not rely on dedicated built-in tables, but offer a means for each user to customize their own view. SCADE System comes with a simple but powerful means:

-A dedicated dialog allows defining the hierarchy of objects to display in a table: the list of possible children, references, or even arbitrary queries is proposed for selection. -For each line in this tree, the list of possible attributes, references, or arbitrary queries is proposed to create columns in the table.

These lists of possible children, references and attributes are directly exposed from the model API. This includes the domain meta-model API specified. So, in a few clicks one can for example set-up the table of all ARINC 429 messages, with their target and with the parameters from data allocated from the functional design.

All table examples listed below have been produced for the designed aircraft braking system. They comply with the original MS Excel tables that were given at the start of the project. Of course the displayed tables can be exported in a click to MS Excel files.

Application to an Avionics system case study

We will now apply the methodology and tools to the avionics system case study described at the beginning of the paper. As explained in section 3 we proceed in layers focusing on data management (producing and consuming). As a result of this stage, Functional Data with producer/consumer tables are available for each Function as illustrated in Figure 4 below for the ADIRU and a global table with all functional data produced and consumed by the Braking System application. Automated checks allows immediate detection of functional data that are not produced or functional data that are not consumed (useless data).

Functional architecture

Software architecture

The software architecture defines the software components of the Braking System and the messages produced and consumed (required) by each software component. Again the messages are propagated in the software architecture by the data propagation mechanism.

In the example illustrated below, the BCS_COM software component of the Braking System requires one message (MSG_ADIRU_COM_C10: ARINC 667-P7 message) produced by the ADIRU component.

The Software architect may use several diagrams to focus on ARINC 664-P7 or ARINC 429 communication as illustrated in figures 5 and 6 below. At the software level we also describe all messages (ARINC 664-P7 and ARINC 429). Figure 7 illustrates the MSG_ADIRU_COM_C10 (ARINC 664-P7) message, with its three data set containing the functional data AC_GND_SPEED, AC_ACCEL and AC_PITCH_ANGLE.

Functional to Software mapping

Now that we have defined the functional and the software architecture, the functional to software mapping consists in the allocations of functions to the software components (illustrated in figure 9), and the functional data mapping to software messages (illustrated in figure 10). Allocation tables are used for that purpose.

ERTS 2 2016 Benefits of Model Based System Engineering for Avionics Systems 8 Automated consistency checks confirm that these allocations are consistent with the data and message propagation: the message to which a functional data element is allocated to must be produced by a software component to which the producer function is allocated to, and must be propagated to the software components to which the consumer function is allocated to. Inefficiencies are also detected, for example when a message carries a data not needed by all recipients of the message. One can now analyze in detail the design tradeoff for message definitions.

Platform architecture

At this stage we capture the platform components (CPUs, switches, buses, external devices, etc) describing the possible resources (CPU, memory, bandwidth, etc) available to the architect to deploy the application. The BCS platform consists of 4 CPUs, 4 Switches, an external device (RDC) and several buses as described in Figure 11. At this platform level, we allocate software components to the CPUs and define message paths between them. For ARINC 664-P7, these paths are known as Virtual Links. Again, these paths are implemented as dedicated data propagated in this architecture. For example, with the ADIRU software being hosted in CPU4 and the COM being hosted in CPU1, the VL associated to MSG_ADIRU_COM_C10 are defined for channel A and channel B, following the classical redundancy means in ARINC 664-P7 communication.

Virtual Links routing are automatically produced in Tables enabling configuration of switches.

Software to Platform mapping

One of the important tasks for the integrator is to allocate the software components onto the platform and optimize usage of available resources. This is one of the main challenges for IMA (Integrated Modular Avionics).

Allocation of the software components (Partition) to CPUs is illustrated in Figure 12 below.

Braking System ICD (Interface Communication Document)

Thanks to this final allocation step we have a complete description of data communication from the functional level down to platform integration from which ICD tables are automatically produced as illustrated in Figure 15 below.

Comparison with other approaches

The NASA handbook [START_REF]NASA Systems Engineering Handbook[END_REF] states that a clean process must be set up to "identify and resolve interface incompatibilities and to determine the impact of interface design changes". Management of Interface Control Documents (ICDs) [START_REF] Vincent | Training Manual for Elements of Interface Definition and Control[END_REF] is indeed at the center of most industries' system engineering processes, but most often supported by tedious manual processes based on MS Excel files cross analysed and reviewed by the different engineering teams involved.

More robust processes rely on databases. They provide scalability, and the database schema enforces some design rules. However, this is not as powerful as the meta-modelling capability provided by UML-based tools, and does not support a graphical representation which is an essential communication means between engineers.

SysML [START_REF]OMG Systems Modeling Language (OMG SysML)[END_REF] is the most known standard in system engineering, but it does not come with specific constructs to model software messages that are exhanged between "blocks". SCADE System Avionics is compliant with SysML, and provides such constructs. Other standards have been set-up which focus on the component interfaces. We now compare our approch with three of them that have been deployed in the industry.

EAST-ADL [7], initially defined in the European ITEA EAST-EEA project that has been then aligned with the AUTOSAR automotive standard was a good source of inspiration. In the same way as the method presented here, the central features of EAST-ADL, is its multi-layer approach, which defines multiple abstraction levels and distributes all development information across these levels. Just like the SCADE System Avionics package, EAST-ADL is supported by a UML Profile. The main difference is in the focus we have put on the detailed definition of the component interfaces that gather information from the different levels of abstraction. On the other hand EAST-ADL provides a focus on timing information that has not been yet considered in the SCADE System Avionics Package.

The SAE "Architecture and Analysis Description Language" (AADL) [START_REF]Architecture Analysis & Design Language (AADL)[END_REF], has its roots in the avionics domain. AADL allows for the description of both software and hardware parts of a system. In contrast to SysML's limited generic components of "block", "port", etc., AADL provides precise modeling concepts to describe the runtime architecture of application systems in terms of concurrent tasks, their interactions, and their mapping onto an execution platform. It also separates the definition of block interfaces from their implementation, but does not make the links between functional, software and platform interfaces in the way presented in this paper.

The more recent FACE standard [START_REF]Future Airborn Capability Environmennt (FACE)[END_REF] also focuses on the non-ambiguous specification of interfaces for "Unit Of Portability" (UoP). It describes the component interfaces at three different layers, conceptual (e.g. mass, length …), logical units (e.g. Kg, millimeters …), and platform implementation (e.g. uint8, float64 …). This complements very well our approach. Indeed it allows setting a "meaning" to the functional data used at the top level of the process we have presented, while FACE itself does not detail the way this information shall be carried into software messages.

It is perfectly possible to define with SCADE System Configurator the EAST-ADL, the AADL, and the FACE metamodels. On-going work to support the FACE standard as a complement of the Avionics package presented here will be published in the coming months.

Conclusion

This paper presents a model based development approach and tooling enabling efficient and agile process development focusing on data. Applied to a case study based on a braking system example, we have demonstrated a complete flow from functional architecture capture down to platform deployment showing the main benefits of a model based approach: Starting from the provided ICD files of the braking system example, the complete retro-fit in SCADE System has been achieved in a couple of months. Thanks to the model based solution, with a user interface that speaks the language of the avionics system designer, design modification and regeneration of consistent ICDs is now mature. This demonstrates a large efficiency and the capability to significantly accelerate the development cycle in handling design changes.


Well supported by tools with features detailed in this paper, we believe the system design methodology can reach the maturity level the software component design has achieved since several years.

Figure 1 :Figure 1

 11 Figure 1: System Configuration Workflow Figure 1 also shows an extract of the ARINC 429 meta-model. -At the top of the diagram, Data, Struct and Field refer to SCADE System meta model; -Below, Message, MessageDefinition, MessageField and MessageData are defined in the "generic" Avionics configuration. They all inherit from SCADE System meta classes -Finally at the bottom of the diagram, the ARINC 429 meta-classes refine the Avionics meta-classes, providing all information needed for the definition of ARINC 429 messages.

Figure 2 :

 2 Figure 2: Functional architecture

Figure 3 :

 3 Figure 3: ADIRU functional data table

Figure 4 :

 4 Figure 4: Software architecture focusing on ARINC 664-P7 Communication

Figure 5 :

 5 Figure 5: Software architecture focusing on ARINC 429 Communication

Figure 6 :

 6 Figure 6: ARINC 664-P7 Message definitionTable Data Set information are gathered in another Table as illustrated below in figure 8.

Figure 7 :

 7 Figure 7: ARINC 664-P7 Data Set Table

Figure 8 :Figure 9 :

 89 Figure 8: Function to Software allocation Table

Figure 10 :

 10 Figure 10: Platform architecture illustrating Chanel A, Chanel B Virtual link routes

Figure 11 :

 11 Figure 11: Software (Partition) to Platform projectionIn the same way software messages allocated to Virtual Links are illustrated in table 13 below.

Figure 12 :

 12 Figure 12: Extract of Message to Virtual Link allocationWe can then perform resource usage checks, such as bandwidth checks, as illustrated in Figure14below.

Figure 13 :

 13 Figure 13: ARINC 664-P7 bandwidth checks results

Figure 14 :

 14 Figure 14: Extract of Braking System ICD

11 

 11 Automated checks ensuring that the functional, software, and platform architecture are consistent with each other  Data flow checks ensuring proper usage and production of data all along the process  Platform resource and usage domain checks enabling design tradeoff in platform definition  Automatic generation of ICD (Interface Communication Document)  Automatic generation of configuration files (for OS and switches)  Full description of communication (CAN, ARINC 429, ARINC 664-P7, discrete)  Full description of Software architecture Other important topics covered at tool and methodology level are not addressed in this paper:  Requirement traceability all along the process  PLM/ALM (Product or Application Lifecycle Management) linkage  Product Line Engineering and Variant Management ERTS 2 2016 Benefits of Model Based System Engineering for Avionics Systems Synchronization of System and Software engineers work

  Fully customizable interface driven by Domain Specific Languages -Clean separation and consistent relationships of the Functional, Software and Hardware layers -Templates for standard avionics protocols (ARINC 429, ARINC 664-P7, CAN provided) -Intuitive hierarchical data modeling and automated ICD generation These means are detailed in this paper; the design of the industrial case study that is first introduced has demonstrated the efficiency of the tool support.

-Efficiency -Tools and methodology should bring savings in design, analysis, and document generation The SCADE System Avionics Package delivers the following answers: ERTS 2 2016 Benefits of Model Based System Engineering for Avionics Systems 2 -

Acknowledgment

We want to thank Mickael Lafaye and Jean-Pascal Rotteleur from Dassault Aviation for their help and the fruitful inputs they provided during the Avionics Case Study


R H J Fick

M Pizzolato

D Wassermann

M Zucchelli

G Menegaz

R Deriche

A SENSITIVITY ANALYSIS OF Q-SPACE INDICES WITH RESPECT TO CHANGES IN AXONAL DIAMETER, DISPERSION AND TISSUE COMPOSITION

Keywords: Diffusion MRI, MAP-MRI, q-space Indices, NODDI, Axonal Dispersion, Axonal Diameter

In Diffusion MRI, q-space indices are scalar quantities that describe properties of the ensemble average propagator (EAP). Their values are often linked to the axonal diameter -assuming that the diffusion signal originates from inside an ensemble of parallel cylinders. However, histological studies show that these assumptions are incorrect, and axonal tissue is often dispersed with various tissue compositions. Direct interpretation of these q-space indices in terms of tissue change is therefore impossible, and we must treat them as scalars that only give non-specific contrast -just as DTI indices. In this work, we analyze the sensitivity of q-space indices to tissue structure changes by simulating axonal tissue with changing axonal diameter, dispersion and tissue compositions. Using human connectome project data, we then predict which indices are most sensitive to tissue changes in the brain. We show that, in both multi-shell and single-shell (DTI) data, q-space indices have higher sensitivity to tissue changes than DTI indices in large parts of the brain. Based on these results, it may be interesting to revisit older DTI studies using q-space indices as markers for pathology.

INTRODUCTION

An important application in diffusion MRI (dMRI) is to infer pathology-related tissue changes from properties of the ensemble average propagator (EAP) [START_REF] Stejskal | Use of Spin Echoes in a Pulsed Magnetic-Field Gradient Study Anisotropic Restricted Diffusion Flow[END_REF]. Recently, functional basis approaches have allowed for the estimation of so-called q-space indices that describe various properties of the threedimensional EAP [START_REF] Hosseinbor | Bessel fourier orientation reconstruction (BFOR): An analytical diffusion propagator reconstruction for hybrid diffusion imaging and computation of q-space indices[END_REF][START_REF] Özarslan | Mean Apparent Propagator (MAP) MRI: A novel Diffusion Imaging Method for Mapping Tissue Microstructure[END_REF]. In contrast to Diffusion Tensor (DT) indices [START_REF] Basser | Estimation of the Effective Self-Diffusion Tensor from the NMR Spin Echo[END_REF], q-space indices also describe the restricted, i.e., non-Gaussian aspects of the EAP. Because of this, q-space indices allow us to relate the EAP to microstructural properties such as the axon diameter, but only when we assume that the tissue consists of parallel cylinders with no extra-axonal space [START_REF] Fick | Laplacian-Regularized MAP-MRI: Improving Axonal Caliber Estimation[END_REF]. However, from histological studies, we know that both these assumptions are incorrect and even in the Corpus † The author expresses his thanks to Olea Medical and to the Provence-Alpes-Côte d'Azur Regional Council for providing grant and support.

Callosum we must account for axonal dispersion [START_REF]Microstructural organization of axons in the human corpus callosum quantified by diffusion-weighted magnetic resonance spectroscopy of N-acetylaspartate and post-mortem histology[END_REF]. This means that q-space indices cannot directly be linked to tissue microstructure, and must be treated as values that only provide non-specific tissue contrast, just as DT indices.

In this work, we analyze the sensitivity of q-space indices to microstructural changes in the presence of axonal dispersion. Inspired by [START_REF] Drobnjak | PGSE, OGSE, and sensitivity to axon diameter in diffusion MRI: Insight from a simulation study[END_REF], we measure the sensitivity of a q-space index as its partial derivative with respect to changes in axonal diameter, dispersion, and volume fractions of intraaxonal and isotropic signal contributions (Figs. 1 and2). We also compare with the sensitivity of classical DT-indices to the same microstructure changes. Finally, we show on highquality data of the Human Connectome Project (HCP) [START_REF] Setsompop | Pushing the limits of in vivo diffusion MRI for the Human Connectome Project[END_REF] which index would be most sensitive to a particular change in microstructure (Fig. 3).

MATERIALS AND METHODS

In this section, we explain our processing pipeline from data generation to q-space index sensitivity analysis. We first provide our dMRI acquisition scheme and our simulation model. We then briefly explain our method of estimating q-space indices. Lastly, we explain the sensitivity analysis.

Acquisition Parameters: We use the multi-shell acquisition scheme of the MGH-HCP database [START_REF] Setsompop | Pushing the limits of in vivo diffusion MRI for the Human Connectome Project[END_REF] in our experiments. This data has particularly high b-values {0, 1000, 3000, 5000, 10000} s/mm 2 with {40, 64, 64, 128, 256} directions and 1.5 mm 3 isotropic voxels. The pulse length and separation time are δ/∆ = 12.9/21.8 ms. Assuming rectangular pulses the q-space positions are defined as q = (γδG)/2π. When comparing with DT-indices, we fit DTI tensors to a single-shell b max = 1000 s/mm 2 acquisition by cutting the outer three shells of the multi-shell acquisition.

Signal Generation: We generate diffusion data corresponding to dispersed cylinders using the orientationdispersed white matter model [START_REF] Zhang | Axon diameter mapping in the presence of orientation dispersion with diffusion MRI[END_REF]

E = (1 -ν iso )(ν ic E ic + (1 -ν ic ) * E ec ) + ν iso E iso (1)
with E ic (a, ODI) the intra-axonal signal with cylinder diameter a and Orientation Dispersion Index (ODI). The signal inside the cylinders is given by the Gaussian Phase Approximation and the dispersion is given by the Watson model, where ODI goes from 0 (no dispersion) to 1 (completely dispersed). The free water signal E iso is an isotropic tensor with free water diffusivity 3•10 -9 m 2 /s and the extra-axonal signal E ec (κ) is a dispersed anisotropic tensor with perpendicular diffusivity 1.2 • 10 -9 m 2 /s, with ν ic and ν iso the intra-axonal and isotropic volume fractions.

Signal Fitting and EAP Reconstruction: We use the Laplacian-regularized Mean Apparent Propagator (MAP)-MRI basis [START_REF] Özarslan | Mean Apparent Propagator (MAP) MRI: A novel Diffusion Imaging Method for Mapping Tissue Microstructure[END_REF][START_REF] Fick | Laplacian-Regularized MAP-MRI: Improving Axonal Caliber Estimation[END_REF] to reconstruct the EAP. In short, MAP-MRI fits the signal with a set of orthogonal basis functions as E(q) = Nmax i c i Φ Ni (q) where every basis function Φ Ni is given as a product of three 1D functions

Φ Ni (A, q) =φ n x(i) (u x , q x )φ n y(i) (u y , q y )φ n z(i) (u z , q z ) (2) with φ n (u, q) = i -n √ 2 n n! e -2π 2 q 2 u 2 H n (2πuq) A = Diag(u 2 x , u 2 y , u 2 z )
with basis order N i = (n x(i) , n y(i) , n z(i) ). We find the diagonalized scaling factors A = RA R T by fitting a tensor A , where R contains the tensor eigenvectors. We then rotate the data into the frame of reference using R and scale the basis functions using A along each direction. In essence, MAP-MRI's first basis function is a DTI tensor [START_REF] Basser | Estimation of the Effective Self-Diffusion Tensor from the NMR Spin Echo[END_REF] and higher order basis functions include Hermite polynomials H n that 'correct' the original DTI approximation. More importantly, in MAP-MRI the EAP P (r) can be directly and analytically reconstructed once the coefficients c are known. Estimation of q-space indices: Using MAP-MRI, we estimate the q-space indices as analytic integrals of the signal and EAP. We estimate the Return-To-Origin, Return-To-Axis and Return-To-Plane Probability (RTOP, RTAP and RTPP), which under several hypotheses are related to the mean pore volume, mean cross-sectional area and mean length [START_REF] Özarslan | Mean Apparent Propagator (MAP) MRI: A novel Diffusion Imaging Method for Mapping Tissue Microstructure[END_REF].

RTOP P (0) (3)
RTAP R P (R r |r ⊥ = 0)dR (4)
RTP P

R 2 P (R r ⊥ |r = 0)dR (5)
We also consider quantities related to the variance of the signal and EAP: The classical Mean Squared Displacement (MSD) and the Q-space Inverse Variance (QIV) [START_REF] Hosseinbor | Bessel fourier orientation reconstruction (BFOR): An analytical diffusion propagator reconstruction for hybrid diffusion imaging and computation of q-space indices[END_REF].

M SD R 3 P (r)R 2 d 3 r = - 1 4π 2 ∆E(q)| q=0 (6)
QIV -1

R 3 E(q)q 2 d 3 q = - 1 4π 2 ∆P (r)| r=0 (7)
Sensitivity Analysis: We determine the sensitivity of qspace indices by computing the partial derivative of an index value over a microstructure change, i.e., a change in axonal diameter, dispersion or volume fractions. In our experiments we perform the analysis between the following values separately: Axonal diameter a = [1 . . . 10] µm, dispersion index ODI = [0 . . . 1], restricted volume fraction ν ic = [0 . . . 1] and isotropic volume fraction ν iso = [0 . . . 1]. When one value is varied in our synthetic experiments, the rest is set to a = 1 µm, ODI = 0.05, ν ic = 0.9, ν iso = 0. We calculate q-space and DT indices for both the multi-shell and singleshell case, where we use MAP-MRI with a radial order of 4 and 0, respectively. We repeat the experiment 200 times with a signal-to-noise ratio of 30 and average the results. We then generate the normalized index values by estimating all indices over a microstructure change and by dividing each by its maximum over the curve. In this way, we normalize for the magnitude differences between different indices (e.g. 10 10 for RT OP and 10 -9 for QIV ). We then calculate the derivative of the normalized index curves by fitting a spline and computing its derivative analytically.

EXPERIMENTS AND RESULTS

Synthetic Experiments: Figs. 1 and2 show the normalized values and absolute derivatives of q-space and DT indices over changes in microstructure. The normalized values provide an intuition on how indices change (positively or negatively) when a particular tissue parameter is changed. We then see the amplitude of the absolute derivative as the index's sensitivity to that tissue change. The left and right columns show results on the multi-shell (MS) b max = 10, 000 s/mm 2 and single-shell (SS) b max = 1, 000 s/mm 2 data, respectively. The solid lines represent q-space indices and the dashed lines DT indices. In the axonal diameter figures (first row) we also mark the largest in-vivo axon diameter with a star at 4µm [START_REF] Aboitiz | Fiber composition of the human corpus callosum[END_REF]. Diameters up to 10µm were included to be consistent with [START_REF] Drobnjak | PGSE, OGSE, and sensitivity to axon diameter in diffusion MRI: Insight from a simulation study[END_REF]. Overall, it can be seen that the normalized values for SS curves behave more monotonic than the MS curves.

Starting with axonal diameter (first row), it can be seen that their indices change little below 4µm. This corresponds to the sensitivities in Fig. 2, where the index derivative is nearly zero below 4µm. We also find that the sensitivity of RTOP and RTAP (blue and green) increases close to linearly and QIV (pink) and D ⊥ become more sensitive after 7µm. Lastly, the multi-shell q-space indices are more sensitive than the single-shell ones, and the DT indices are least sensitive.

Considering axonal dispersion (second row), we find that the multi-shell RTOP and RTAP show a small value increase at ODI lower than 0.05. This is likely caused by the nearly constant diffusion signal perpendicular to the cylinder axis with the preset volume fractions and low axonal dispersion, causing unstable MAP-MRI signal extrapolation. Then, as ODI increases, we find that MS and SS q-space indices have similar profiles, indicating that higher b-values do not clearly improve index sensitivity to dispersion. At ODI between 0.3 and 0.6 the FA (dashed brown) is the most sensitive parameter, after which all indices are similarly sensitive.

Showing changes over restricted volume fraction (third row), we find that multi-shell RTOP and RTAP are more sen- From top to bottom we show results over axon diameter, dispersion index, and restricted and isotropic volume fractions. The stars in the axonal diameter figures indicate the largest axon diameter found in-vivo [START_REF] Aboitiz | Fiber composition of the human corpus callosum[END_REF].

sitivity than their single-shell versions below volume fractions of 0.8. In MS, we see that QIV (pink) and FA (dashed brown) are more sensitive at lower volume fractions while multi-shell RTOP and RTAP sensitivity dominates at volume fractions beyond 0.3. In SS RTOP and RTAP are only most sensitive beyond 0.8, while QIV dominates the curve below 0.2. Lastly, when varying the isotropic volume fraction (fourth row) we see a similar profile as with the restricted volume fraction -only reversed. This makes sense as decreasing the restricted volume fraction and increasing the isotropic volume fraction both replace the restricted signal contribution with either an anisotropic or isotropic tensor. In MS, we see a high sensitivity for FA above 0.7, RTOP and RTAP dominate between 0.3 and 0.7, and QIV is sensitive below 0.3.

To make these results more tangible, in the next experi- HCP Experiment: We select a coronal slice of a subject of the human connectome project and use NODDI [START_REF] Zhang | NODDI: practical in vivo neurite orientation dispersion and density imaging of the human brain[END_REF] to estimate the axonal dispersion and intra-axonal and isotropic volume fractions. The result can be seen in the top row of Fig. 3. For every pixel in this image we determine which qspace or DT index is most sensitive to a microstructure change given the axonal dispersion and volume fractions found in that pixel. The results are given separately for single-shell and multi-shell in the second and third row of Fig. 3.

To find this most sensitive index we first generate a 3dimensional volume of synthetic dMRI voxels, varying ODI, ν ic or ν iso along each axis from 0 to 1, to be used as a lookup table. We do not include axonal diameter as we found its sensitivity is negligible (top row Fig. 2). We compute the same scalar indices as in the previous section. Then, for every voxel within the brain mask, we retrieve the partial derivatives in our synthetic volume at the position of the found NODDI Most Sensitive Single-Shell Index Fig. 3: A coronal slice of a subject of the HCP data. The top row shows the parameters that NODDI estimates. The bottom row shows the expected index that is most sensitive when that parameter changes. parameters (i.e., ODI, ν ic or ν iso ). We then find the index with the highest sensitivity and label the voxel accordingly. The first column of Fig. 3 shows that when ODI changes, FA (brown) is most sensitive in most of the brain for both MS and SS. Only in MS is RTAP (green) more sensitive in coherent white matter (e.g. Corpus Callosum). When the restricted volume fraction is changed (second column) we find a different result between SS and MS. In SS, RTOP (blue) is most sensitive in coherent white matter, QIV (red) in the cortex and FA in the rest of the brain. In MS, RTOP is most sensitive in the bulk of the brain, and RTAP and MSD (light-blue) in the cortex. Lastly, when isotropic volume fractions change (third column) RTOP is most sensitive in most of the brain and QIV in the CSF. MD is never the most sensitive index.

DISCUSSION AND CONCLUSION

In this work we clarified and illustrated the sensitivity of qspace indices to changes in axonal diameter, axonal dispersion and tissue composition, for both single-shell and multishell acquisitions on both synthetic and real data. In Fig. 2 we showed that multi-shell q-space indices improve the sensitivity to changes in volume fraction in the range between 0.3 and 0.8, which are often found in the brain (middle column Fig. 3). Furthermore, Fig. 3 shows that RTAP is the most sensitive parameter w.r.t. dispersion in anisotropic white matter. This means that a small change in dispersion has a large effect the estimated 'apparent axon diameter' [START_REF] Özarslan | Mean Apparent Propagator (MAP) MRI: A novel Diffusion Imaging Method for Mapping Tissue Microstructure[END_REF] -an effect which is typically ignored. Finally, and perhaps most interestingly, the single-shell results in Fig. 3 show that, when a change is expected in tissue composition, it may be more sensible to look for changes in QIV and RTOP, rather the classical FA and MD. Based on these results, it may be interesting to revisit older DT studies using QIV and RTOP as a marker for pathology.

Fig. 1 :

 1 Fig.1: Normalized q-space and DT index values over simulated microstructure change. The left and right columns show results on the multi-shell (MS) b max = 10, 000 s/mm 2 and single-shell (SS) b max = 1, 000 s/mm 2 data, respectively. From top to bottom we show results over axon diameter, dispersion index, and restricted and isotropic volume fractions. The stars in the axonal diameter figures indicate the largest axon diameter found in-vivo[START_REF] Aboitiz | Fiber composition of the human corpus callosum[END_REF].

Fig. 2 :

 2 Fig.2: The first order derivatives of q-space and DT index values over simulated microstructure change. The layout is the same as in Fig.1.

Acknowledgments

This work was partly supported by the French ANR "MOSI-FAH" under ANR-13-MONU-0009-01. Data used in the preparation of this work were obtained from the Human Connectome Project (HCP) database.