Laurent Stainier
email: l.stainier@ulg.ac.be

Eduardo A Fancello
email: fancello@grante.ufsc.br

Jean-Philippe Ponthot

A VARIATIONAL FRAMEWORK FOR NONLINEAR VISCOELASTIC AND VISCOPLASTIC MODELS IN FINITE DEFORMATION REGIME

Keywords: Constitutive Updates, Finite Viscoelasticity, Finite Viscoplasticity, Variational Formulation

The goal of this work is to provide a general framework for constitutive viscoelastic and viscoplastic models based on the theoretical background proposed in Ortiz and Stainier, Comput. Meth. App. Mech. Engng., Vol. 171, 419-444 (1999). Thus, the approach is qualified as variational since the constitutive updates obey a minimum principle within each load increment. The set of internal variables is strain-based and thus employs, according to the specific model chosen, multiplicative decomposition of strain in elastic and irreversible components. Inserted in the same theoretical framework, the present approach for viscoelasticity shares the same technical procedures used for analogous models of plasticity or viscoplasticity, say, the solution of a minimization problem to identify inelastic updates and the use of exponential mapping for time integration. Spectral decomposition is explored in order to accommodate, into analytically tractable expressions, a wide set of specific models. Moreover, it is shown that, through appropriate choices of the constitutive potentials, the proposed formulation is able to reproduce results obtained elsewhere in the literature. Finally, different numerical examples are included to show the characteristics of the present approach and to compare results with others found in literature when possible.

INTRODUCTION

Many different models for viscoelastic materials in finite deformation regime are found in literature. However, in contrast with what we see in small deformation models, the choice of convenient internal variables and evolution laws is not trivial nor unique, leading to different formulations. From one side, we recall the the work of Simo [START_REF] Simo | On a fully three dimensional finite-strain viscoelastic damage model: formulation and computational aspects[END_REF] in which an additive decomposition of stresses in equilibrium and non equilibrium contributions is stated and, more relevant, the evolution law is defined as a linear differential equation on the non-equilibrium stresses. This approach was later followed, among many others, by Holzapfel and Simo, [START_REF] Holzapfel | A new viscoelastic constitutitve model for continuous media at finite thermomechanical changes[END_REF] Holzapfel [START_REF] Holzapfel | On large viscoelasticity: continuum formulation and finite element applications to elastomeric structures[END_REF] or, more recently, Holzapfel and Gasser, [START_REF] Holzapfel | A viscoelastic model for fiber-reinforced composites at finite strains: Continuum basis, computational aspects and applications[END_REF] and Bonet. [START_REF] Bonet | Large viscoelastic constitutive models[END_REF] Multiplicative decomposition of strains applied to viscoelastic constitutive equations goes back to the work of Sidoroff [START_REF] Sidoroff | Un modèle viscoelástique non linèaire avec configuration intermédiaire[END_REF] and later to several others. [START_REF] Lubliner | A model of rubber viscoelasticity[END_REF][START_REF] Kaiss | Three-dimensional incompressible viscoelasticity in large strains: formulation and numerical approximation[END_REF][START_REF] Lion | A constitutive model for carbon filled rubber. experimental investigation and mathematical representations[END_REF] In particular Reese and Govindjee 10 discussed the ability of different models to reproduce nonlinear viscous behavior and they proposed a model which is not restricted to small perturbations away from thermodynamic equilibrium.

The goal of this work is to provide a general framework for constitutive viscoelastic models based on the mathematical background proposed in Ortiz and Stainier, [START_REF] Ortiz | The variational formulation of viscoplastic constitutive updates[END_REF] and Stainier. [START_REF] Stainier | Une formulation variationelle des algorithmes de calcul des constraintes pour les modèles élastoviscoplastiques et viscoélastiques en grandes transformations[END_REF] The approach is qualified as variational since the constitutive updates obey a minimum principle within each load increment. The set of internal variables is strain-based and thus employs, according to the specific model chosen, multiplicative decomposition of strain in elastic and viscous components.

Inserted in the same theoretical framework, this particularization and that for plasticity or viscoplasticity, share the same technical procedures to deal with the local nonlinear constitutive problem, i.e. the solution of a minimization problem to identify inelastic updates and the use of exponential mapping for time integration. [START_REF] Anand | Finite deformations constitutive equations and a time integration procedure for isotropic hyperelastic-viscoplastic solids[END_REF][START_REF] Miehe | Exponential map algorithm for stress updates in anisotropic multiplicative elastoplasticity for single crystals[END_REF] However, instead of using the classic decomposition of inelastic strains into "size" and "direction", we take profit of a spectral decomposition that provides additional facilities to accommodate, into simple analytical expressions, a wide set of viscous models. It is also possible to show that an appropriate choice of constitutive potentials allows to retrieve other models in literature.

VARIATIONAL FORM OF CONSTITUTIVE EQUATIONS

Using conventional notation, let us call F = ∇ 0 x the gradient of deformations, and C = F T F the Cauchy strain tensor, respectively. These values may be decomposed in volumetric and isochoric parts. The isochoric tensors are defined as follows:

F = 1 J 1/3 F, J = det(F), Ĉ = FT F = 1 J 2/3 F T F, (1)
We will work in the framework of irreversible thermodynamics, with internal variables. Thus, we define a general set E = {F, F i , Q} of external and internal variables, where F i is the inelastic part of the (total) deformation, and Q contains all the remaining internal variables of the model. In addition, a multiplicative decomposition F = F e F i of the gradient of deformations is considered. We assume the existence of a free energy potential W (E) and a dissipative potential φ( Ḟ; E), such that the Piola-Kirchhoff stress tensor, comprised of an equilibrium (elastic) and a dissipative (viscous) components, is derived as follows:

P = ∂W ∂F (E) + ∂φ ∂ Ḟ ( Ḟ; E). (2)
In addition, another dissipative potential ψ( Ḟi , Q; E) is included to characterize the irreversible behavior related to the inelastic tensor F i , such that

T = - ∂W ∂F i (E) = ∂ψ ∂ Ḟi ( Ḟi , Q; E), A = - ∂W ∂Q (E) = ∂ψ ∂ Qi ( Ḟi , Q; E). (3)
It was shown [START_REF] Ortiz | The variational formulation of viscoplastic constitutive updates[END_REF][START_REF] Stainier | Une formulation variationelle des algorithmes de calcul des constraintes pour les modèles élastoviscoplastiques et viscoélastiques en grandes transformations[END_REF] that an incremental version of the above equations, constituting an incremental update method for the material state, can be obtained from the following incremental potential:

W(F n+1 ; E n ) = ∆tφ F, E n + min F i n+1 Q n+1 W (E n+1 ) -W (E n ) + ∆tψ Fi , Q; E n , (4)
where

F (F n+1 , E n ) , Fi F i n+1 , E n and Q (Q n+1 , E n )
are suitable incremental approximations of the rate variables Ḟ, Ḟi and Q respectively.

VISCOPLASTICITY MODELS

We start by recalling the variational formulation of visoplasticity, as proposed in previous work. [START_REF] Ortiz | The variational formulation of viscoplastic constitutive updates[END_REF][START_REF] Stainier | Une formulation variationelle des algorithmes de calcul des constraintes pour les modèles élastoviscoplastiques et viscoélastiques en grandes transformations[END_REF] This will provide a background against which differences and similarities between viscoplasticity and viscoelasticity can be contrasted.

Viscoplastic solids are characterized by the existence of a certain class of deformations F p , or plastic deformations, which leave the crystal lattice undistorted and unrotated, and, consequently, induce no long-range stresses. In addition to the plastic deformation F p , some degree of lattice distortion F e , or elastic deformation, may also be expected in general. One therefore has, locally,

F = F e F p (5)
This multiplicative elastic-plastic kinematics was first suggested by Lee, [START_REF] Lee | Elastic-plastic deformation at finite strains[END_REF] and further developped and used by many others. We postulate the existence of a Helmholtz free energy density of the form

W = W (F e , F p , Q) = W (FF p-1 , F p , Q) ≡ W (F, F p , Q) (6)
where Q ∈ R N denotes some suitable collection of internal variables. The complete set of internal variables is, therefore {F p , Q}. The local state of the material is then described by the variables {F, F p , Q}. In materials such as metals, the elastic response is ostensibly independent of the internal processes and the free energy (6) decomposes additively as

W = W e (FF p-1 ) + W p (F p , Q) (7)
The function W e determines the elastic response of the metal, e. g., upon unloading, whereas the function W p describes the hardening of the material. Physically, W p represents the stored energy due to the plastic working of the material. In the case where the state of hardening if fully described by a single internal variable, i. e., N = 1, Q = {¯ p }, the material is said to undergo isotropic hardening.

A possible extension of von Mises' theory of plasticity to the finite deformation range is obtained by postulating a flow rule of the form:

Ḟp F p-1 = ˙ p M (8)
where ¯ p is the effective plastic strain and the symmetric matrix M is required to satisfy the incompressibility constraint: trace(M) = 0

and the normalization condition:

M • M = 3 2 (10)
but is otherwise unspecified. The normalization condition ( 10) is chosen so that ˙ p coincides with the rate of axial stretching in the uniaxial test. The flow rule ( 8) is a constraint relating the internal variables F p and ¯ p , which must be accounted for in the minimization (4) (the minimization is then also carried over M).

Plastic deformations are incrementally updated by the exponential mapping

F p n+1 = exp [∆¯ p M] F p n ( 11
)
The exponential mapping has the convenient property of preserving the isochoric character of plastic deformations. [START_REF] Anand | Finite deformations constitutive equations and a time integration procedure for isotropic hyperelastic-viscoplastic solids[END_REF][START_REF] Miehe | Exponential map algorithm for stress updates in anisotropic multiplicative elastoplasticity for single crystals[END_REF] 4 A GROUP OF VISCO-HYPERELASTIC MODELS

General formulation

A quite general group of viscoelastic materials can be modelled within the present variational framework. Due to the possibility of obtaining analytical or semi-analytical expression for the constitutive updates, only isotropic models will be considered now. However, no theoretical constraints to include more general behaviors are found. The rheological mechanism shown in Figure 1 is taken as a basis to include different potentials expressions in (4). The model is based on the following assumptions:

• The elastic part of the Kelvin branch is split in isochoric and volumetric energies. The isochoric part is an isotropic function of Ĉ = FT F : where c j are the eigenvalues of Ĉ. The volumetric part may be defined using the usual expression

ϕ( Ĉ) = ϕ(c 1 , c 2 , c 3 ), (12)
U (J) = K 2 [ln J] 2 ,
The viscous part of the Kelvin branch is an isotropic function of the symmetric part of the rate of deformation:

φ(D) = φ(d 1 , d 2 , d 3 ) with D = dev sym ḞF -1 , (13)
where d j are the eigenvalues of D.

• The Maxwell branch, connected in parallel, is based on a multiplicative split of strains in an elastic and an isochoric inelastic (viscous) part:

F = Fe F v =⇒ Fe = FF v-1 , det F v = 1. (14)
A flow rule for the internal variable F v can be written as:

Ḟv = D v F v = d v j M v j F v , (15)
in which the spectral decomposition of D v = sym( Ḟv F v-1 ) in eigenvalues d v j and eigenprojections M v j , j = 1, 2, 3, was used. The scalars d j are chosen to be the internal variables contained in the set Q = {d 1 , d 2 , d 3 }. In this case, it is important to note that ( 15) is a constraint relating the internal variables F v and Q . The elastic and viscous potentials associated to this branch are assumed to be isotropic functions of the elastic deformation and viscous stretching, and thus depend on their eigenvalues:

ϕ e ( Ĉe ) = ϕ e (c e 1 , c e 2 , c e 3 ) and ψ(D v ) = ψ(d v 1 , d v 2 , d v 3 ), (16)
where c e j are the eigenvalues of Ĉe .

• Viscous deformations are incrementally updated by exponential mappings:

∆ F = Fn+1 F-1 n = exp[∆tD] ⇒ D = ∆q j ∆t M j = 1 2∆t ln ∆ Ĉ . ( 17
) ∆F v = F v n+1 F v-1 n = exp[∆tD v ] ⇒ D v = ∆q v j ∆t M v j = 1 2∆t ln (∆C v ) . (18)
Expressions ( 17) and (18) show that D and D v are approximated by incremental expressions of ∆ Ĉ and ∆C v respectively. The exponential mapping has the particular convenient property of providing an isochoric tensor for any traceless argument. [START_REF] Anand | Finite deformations constitutive equations and a time integration procedure for isotropic hyperelastic-viscoplastic solids[END_REF][START_REF] Miehe | Exponential map algorithm for stress updates in anisotropic multiplicative elastoplasticity for single crystals[END_REF] Taking into account (17) and ( 18), the minimizing variables Q n+1 , F v n+1 in (4) are replaced by the new incremental variables ∆q v j , M v j .:

W(F n+1 ; E n ) = W(C n+1 ; E n ) = ∆ϕ( Ĉn+1 ) + ∆tφ ∆q v j ∆t + ∆U (θ n+1 ) + min M v j ,∆q v j ∆ϕ e ( Ĉe n+1 ) + ∆tψ ∆q v j ∆t , (19)
such that

∆q v j ∈ K Q = {p j ∈ R : p 1 + p 2 + p 3 = 0}, (20)
M v j ∈ K M = {N j ∈ Sym : N j • N j = 1, N i • N j = 0, i = j}. (21)
The set K Q enforces the traceless form of D v , while the set K M accounts for usual properties of eigenprojections. Moreover, it is easy to verify that both sets are convex on their respective variables. Given isotropic expressions for energy functions, the minimization in ( 19) can be performed analytically. A simple extension to this model can be obtained by considering a set of P Maxwell branches, as seen in Figure 1. More details on the practical implementation of this formulation, including the derivation of a consistent tangent operator can be found elsewhere. [START_REF] Fancello | A variational formulation of constitutive models and updates in non-linear finite viscoelasticity[END_REF]

Hencky and Ogden models

Hencky models are based on quadratic forms of logarithmic strain tensors:

ϕ = µ 3 j=1 ( j ) 2 , φ = η 3 j=1 (d j ) 2 , ( 22
)
ϕ e = µ e 3 j=1 e j 2 , ψ = η v 3 j=1 d v j 2 . ( 23
)
In this case, it is particularly convenient to obtain simple uncoupled linear expressions for the minimizing argument ∆q v j . In spite of the facility offered by Hencky models in terms of analytical treatment, it is well known that these type of hyperelastic potentials do not fit well the behavior of rubber-like materials. For that case, a more adequate choice may be the Ogden model which has also the capability of generalizing other models like neo-Hookean and Mooney-Rivlin. Ogden models are based on the following potentials:

ϕ = 3 j=1 N p=1 µ p α p ([exp( j )] αp -1) , φ = 3 j=1 N p=1 η p α p ([exp(d j )] αp -1) , (24)
ϕ e = 3 j=1 N p=1 µ e p α p exp( e j ) αp -1 , ψ = 3 j=1 N p=1 η v p α p exp(d v j ) αp -1 . (25)
5 NUMERICAL EXAMPLES

Shear test

This example presents a pure shear tests of a single 3D element (Figure 2). Material parameters and load characteristics were taken from an equivalent example in Reese and Govindjee, [START_REF] Reese | A theory for finite viscoelasticity and numerical aspects[END_REF] in order to perform some useful comparisons. The lateral displacement u x follows a sinusoidal law . The material was assumed to be almost incompressible through the choice of a high value for the bulk modulus K. Two different models for ϕ were used: Ogden model and Hencky model. In the case of Ogden, we used the following sixparameter fitting:

µ 1 = 20, µ 2 = -7, µ 3 = 1.5, α 1 = 1.8, α 2 = -2, α 3 = 7.
For the Hencky model, the value µ = i 1 2 µ i α i = 30.25 was used, which is the consistent equivalent shear modulus for small deformations. The Maxwell branch uses Hencky model for both potentials with µ e = 77.77 and viscous coefficient η v such that τ = η v µ e = 17.5 . The time evolution of Cauchy stresses σ xy as a function of shear strain C xy , for different shear amplitudes, is shown in Figure 3. In the case of small strains both models (Ogden or Hencky main spring) give identical results, and match quite well equivalent results in the reference work. [START_REF] Reese | A theory for finite viscoelasticity and numerical aspects[END_REF] As expected, the behavior of the main spring is determinant on the behavior of the whole system for deformations higher than unity. Comparing the results of the Ogden-based model with those of Reese and Govindjee 10 it is possible to see a close correlation of maximum values of stress for all four cases. However, hysteresis loops clearly look "thinner" as the deformation grows along the cycle. This behavior is in agreement with the fact that the Hencky model used in the Maxwell branch provides a contribution in stress much more lower than a corresponding Ogden model for high deformations.

Viscoelastic support

This example simulates a viscoelastic cylindrical support clamped on its exterior surface and with a rigid edge connected to a vibrating device (see Figure 4). The harmonic vibration u = U sin wt , with w = 10 s -1 occur along different directions. The first one is a lateral translation with maximum displacement U x = 3 8 (R e -R i ). The second one is composed by a axial translation (U y = R i ) and rotation (θ y = 45 • ). Dimensions of the viscoelastic support are R i = 15mm, R e = 30mm and L = 50mm. Figure 5(a) shows the maximum amplitude of deformations for a lateral motion while Figure 6(a) illustrates the case of axial (rotation plus translation) motion. The isochoric nature of the material shows up in Figure 5(a) where the compressed and tractioned sides of the cylinder deform accordingly to preserve this constraint. Two material models were run, both sharing the same constitutive characteristics in the small strain regime.

• Case 1: Ogden model for both springs potentials ϕ and ϕ e (µ e i = 4µ i ) : µ 1 = 3.5 ; µ 2 = 0.011 ; µ 3 = 0.0015 and α 1 = 0.1 ; α 2 = 2.0 ; α 3 = 9 (µ eq = i 1 2 µ i α i = 0.19275 MPa). The viscous potential ψ is of Hencky type with η v = 7.69 (τ = 0.4 s). Potential φ is null.

CONCLUSION

We presented in this article a general set of viscoelastic constitutive models based on a variational framework which provides appropriate mathematical structure for further applications like, for example, error estimation. The theoretical and numerical background is stated for general isotropic constitutive functions depending on eigenvalues of strains and strain-rates. As a consequence, most of the implementation effort, including stress updates and tangent matrix is done at generic level with no relation to a specific isotropic law (potential).

In the numerical examples we compared the capacity of Hencky and Ogden-type models to reproduce observed nonlinear viscous behaviour. As expected, Ogden models perform better for the case of large strains and rubber-like materials, leading to non-elliptic hysteretic loops. Moreover, this choice do not represent, in the present formulation, any additional complexity to the numerical implementation or additional cost on computations.

Figure 1 :

 1 Figure 1: Generalized Kelvin-Maxwell model.

Figure 2 :

 2 Figure 2: Cyclic shear test

5 Figure 3 :

 53 Figure 3: Stress-strain curves in cyclic shear test

Figure 4 :

 4 Figure 4: Support. Undeformed configuration.

Figure 5 :

 5 Figure 5: (a) Deformed configuration for lateral edge motion. (b)Lateral force F x versus displacement u x .

Figure 6 :

 6 Figure 6: (a) Deformed configuration for axial edge motion. (b) Axial force F y versus displacement u y .


Julien Brunel

David Chemouil

Vincent Ibanez

Nicolas Meledo

Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy

We propose an approach based on Alloy to formally model and assess a system architecture with respect to system-level safety requirements. The system on which we instantiate our approach is a specific Required Navigation Performance system from a Thalès Avionics named Localizer Performance with Vertical guidance Approach (LPV). In this article, we describe how to define such a system architecture and how to verify safety objectives.

Introduction

This work has been produced in the context of the Artemis European project CESAR, ended in 2012. The aim of CESAR was to boost cost efficiency of embedded systems development and safety and certification processes in the different domains: automotive, aerospace, rail and automation. To achieve this goal, CESAR promoted model-based techniques and formal methods.

In this context, Thales Avionics and Onera collaborated on applying formal methods in order to assess avionic architectures. Indeed, in the avionic domain, the definition of the architecture is one of the main activities in the development phase. The architecture must be defined very early and must validate different constraints such as physical reuse, safety, security, etc. . .

To help avionics architects to define the final architecture, modelling facilities are currently deployed and linked to early validation capabilities. The aim of this work is to study the benefit of a formal method in order to assess models of avionic architectures with respect to some specific high-level safety requirements. We will use the formal language (and its associated tool) Alloy and apply our approach on a specific RNP approach called Localizer Performance with Vertical guidance Approach (LPV approach).

LPV case study

An approach with vertical guidance (APV) uses lateral and vertical guidance, and does not meet the requirements established for precision approach and landing operations. Depending on the type of APV procedure, lateral guidance can be provided from either stand-alone Global Navigation Satellite Systems (GNSS), or by RNAV derived positioning using multi-sensor positioning capability. Vertical guidance can be provided from GNSS augmentation system such as SBAS (or possibly Galileo in the future) or a barometric reference. APV procedures are based on two different concepts, which allow to reduce minimums compared to conventional Non-Precision Approaches. On the one hand, the APV-BARO (highly developed in the mainline segment) relies on navigation systems with high integrity baroaltimeter equipment with temperature compensation. On the other hand, the second concept called APV-SBAS relies on a satellite based augmentation system that improves the navigation system localization through the enhancement of GNSS localization precision and error correction.

LPV approach is characterized by a Final Approach Segment (FAS). FAS is the approach path which is defined laterally by the Flight Path Alignment Point (FPAP) and landing Threshold Point/Fictitious Threshold Point (LTP/FTP), and defined vertically by the Threshold Crossing Height(TCH) and Glide Path Angle (GPA).

In this article, we consider the functional architecture of the LPV system and assess the two following safety objectives:

• Loss of LPV capability. The architecture must have two independent ways to provide LPV data.

• Misleading information integrity. The architecture must control the value of the LPV data provided by each calculator and between each screen and find mitigation in case of erroneous data.

Evaluation of the case study with Alloy

Alloy [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] is a formal system-modelling language amenable to automatic analyses. Alloy is implemented as a cost-less free-software tool, the Alloy Analyzer, which is programmed in Java and hence runnable on the majority of platforms. With respect to the safety objectives we are going to assess, the AltaRica [1] language would have been another possible choice. However, we decided to take benefit from the model-based aspect of Alloy and its expressiveness for the specification of the properties to check. Indeed, Alloy allows to define easily the metamodel of the avionic architectures we will analyze instead of encoding them in terms of AltaRica concepts. Moreover, the specification of the properties we want to check are expressed in (a relational extension of) first-order logic with many features adapted to model-based reasoning.

To represent the functional architecture of LPV (see Fig 1) in Alloy, we identified the major concepts at stake and defined an Alloy signature for each of them: Function, Port, IPort (input port), OPort (output port). Each Function has a set input of IPorts and a set output of OPort as attributes. An OPort of a function is related to a set of IPort of other functions through a flow and to a set of IPorts of the very function through the relation dependsOn in order to express which input ports can influence an output port (in term of failure propagation). Each function and each port hold a dysfunctional status (OK, Lost, or Err). Moreover, each port has a value. Notice that, in our model, the value will only be useful for certain ports, representing the pilot selection, the discrepancy between both LPV processing, and the reset of displays. Concerning the other ports, we only deal with their status and the value is just ignored (a finer modelling would have been possible here but it would have led to a worthless, more complex model). The following Alloy code corresponds to these concepts definitions (see also Fig. 2 We then define instances of these concepts corresponding to the LPV functional architecture. The function instances take into account the selection of the source by the crew (SelectSource), two occurrences of SBAS positioning (ComputeSBAS1, ComputeSBAS2), two occurrences of LPV processing (ComputeLPV1, ComputeLPV2), three occurrences of displays (Acquirei, i ∈ {1..3}), three occurrences of display resetters (Crosschecki, i ∈ {1..3}) and of monitors in order to launch an alarm, (Monitori, i ∈ {1..3}). We also define the different ports of each function, and the way ports are related to each other via flows. For instance, the following Alloy code is an excerpt of the flow definition, expressing that the output port oSBAS1 is related to the input port iSBAS1 via a flow (idem for oSBAS2 and iSBAS2). flow = oSBAS1→iSBAS1 +oSBAS2→iSBAS2 +...

We also define some global constraints the architecture must satisfy, such as the fact two ports related by a flow share the same status and the same value: The following code defines the status of the output port oSelected1 of function Aquire1. If this function is OK, oSelected1 the status is either equal to the status of its first input or to the status of its second input, depending on the selection made by the pilot. If the function Aquire1 is lost, then the status of output oSelected1 is lost. Otherwise, it is erroneous.

let st = Acquire1.status | let v = iSelection1.value | oSelected1.status = {
st = OK and v = v0 implies iDeviation11.status else st = OK and v = v1 implies iDeviation21.status else st = Lost implies Lost else Err } Similarly, we define, for each function, output ports status (and value in the case of pilot selection, discrepancy, and display reset) from input ports status (and value). Then, Alloy Analyzer proposes, with the command run to produce automatically an instance that satisfies all the definitions we expressed, and the global constraints. Of course, this is only possible if there is no inconsistency in the definitions. We can customize the way the instance is graphically displayed. Fig. 3 shows an excerpt of an instance produced by the Analyzer, where functions are represented by blue rectangles, output ports by red "inversed houses", and output ports by green inversed trapezoids. The status and values are not displayed.

We are now able to check formally various properties expressed in Alloy. A first kind of properties we can check consists of structural properties about the model. For instance, the fact that a port can only belong to one function, the fact that flows correspond to one-to-many communication, and the fact that ports that are related by the dependsOn relation belongs to the same function, is expressed by the following properties:

op).input }

The command check model_structure verifies that, up to a certain bound, all possible instances of the model satisfy these properties. If it is not the case, it yields a counter-example instance.

Now we want to validate the safety objectives expressed in Sect. 2. Concerning the Loss of LPV capability constraint, we express the following property:

• If one (and only one) LPV processing is lost, and if the pilot does a correct selection, then the data sent by the three displays are still correct. This corresponds to the following Alloy code (for the loss of LPV1):

Figure 1 :

 1 Figure 1: LPV architecture

Figure 2 :

 2 Figure 2: Case study metamodel (simplified)

Figure 3 :

 3 Figure 3: Visualization of LPV functional architecture in the Alloy Analyzer (excerpt)

  assert model_structure { input in Function one →IPort output in Function one →OPort flow in OPort one →IPort all op : OPort, ip : op.dependsOn | ip in (output.

  ).

	enum Status { OK, Err, Lost }
	abstract sig Port {
	status : Status,
	value : Value
	}
	abstract sig Port {
	status : Status,
	value : Value
	}
	abstract sig IPort extends Port {}
	abstract sig OPort extends Port {
	flow : set IPort,
	dependsOn : set IPort
	}
	abstract sig Function {
	input : set IPort,
	output : set OPort,
	status : Status
	}

assert one_computer_lost { (all f: Function | (f =ComputeLPV1 implies f.status=OK) and ComputeLPV1.status=Lost and oSelection.value=v1) implies oSelected1.status = OK and oSelected2.status = OK and oSelected3.status = OK } The command check one_computer_lost verifies that the model satisfies this property.

Concerning the Misleading information integrity constraint, we expressed two properties to be satisfied by the functional architecture:

• If one LPV processing produces erroneous data, then an alarm (modeled by the variables oDiscrepancy) is launched on the three displays. This corresponds to the following Alloy code (for the LPV1 in erroneous failure mode): assert one_computer_erroneous { (all f: Function | (f =ComputeLPV1 implies f.status=OK) and ComputeLPV1.status=Err) implies oDiscrepancy1.value=v1 and oDiscrepancy2.value=v1 and oDiscrepancy3.value=v1 }

• If one display returns an erroneous data, it resets itself. This corresponds to the following Alloy code (for display 1 (Acquire1) in erroneous failure mode: assert one_display_erroneous { (all f: Function | (f =Acquire1 implies f.status=OK) and Acquire1.status=Err) implies oReset1.value=v1 } All the properties we have expressed in this section are validated by Alloy Analyzer.

A last aspect we verified concern the "functional chains", used by Thales to support safety analyses. A functional chain is sequence of functions and ports linked by flows that lead to a given output port. If we know all the functional chains leading to a given output port viewed as a target data, it gives information about all the functions whose failure could have an impact on the integrity of the target data. It turns out from discussions that these functional chains are specified by engineers by hand. We propose here a way to generate all the functional chains leading to a given output port (this set of functional chains defines what we call a functional tree). The following Alloy code defines what a functional tree is. It is defined by an inductive relation next and a given output port target satisfying the following constraint: So that Alloy Analyzer generates a functional tree whose target is the output port oSelected1 (output of function Aquire from display 1), we have to specify a simple predicate expressing that there is a functional tree whose target is oSelected1, and then to ask for an instance satisfying this predicate, with the command run.

Conclusion

In this article, we modeled the LPV functional architecture in the Alloy language. We then expressed different properties from the safety objectives in Alloy language. We checked with Alloy analyzer that these properties are fulfilled by the model. We also proposed a definition that allows to generate all the functional chains leading to a given data, in order to support some safety analyses.


Marc Boyer

Loïc Fejoz

Stephan Merz

Proof-by-Instance for Embedded Network Design

published or not. The documents may come

Introduction

Embedded systems are often safety-critical, and their development therefore calls for techniques ensuring high quality. In particular, domains such as avionics (fly-by-wire, control) and medicine (infusion pumps, pacemakers) are subject to regulation requiring certification, and similar quality levels are justified for domains such as transportation (automotive, train control) or for systems where loss or malfunctioning has high costs, e.g. satellites. Traditionally, quality is ensured by applying rigorous development processes, testing of components and systems, and the use of formal methods. The verification tools used in such an approach are themselves critical and therefore subject to certification. In particular, some regulatory standards (e.g. DO178-C) require the same level of confidence in verification tools as in the systems in whose development they are used, adding to the overall cost of development and complicating the maintenance and improvement of such tools.

For instance, the PEGASE project [START_REF] Boyer | The pegase project: Precise and scalable temporal analysis for aerospace communication systems with network calculus[END_REF] focused on determining bounds on message delays and dimensioning buffers in the design of networks for embedded systems such as AFDX backbones used in avionics. The formal underpinnings of the project were provided by Network Calculus (NC) [START_REF] Boudec | Network Calculus[END_REF], a domain-specific formal method, and as explained above, its use for certifying the design requires high confidence in the results computed by the tools. Although the underlying theory is generally well understood, implementation errors may result in faulty network designs, with unpredictable consequences.

Although the use of formal methods is encouraged in certified developments, formally verifying a complex tool such as an NC analyzer, for any possible network design, looks like a daunting task. Proof-by-instance (also known as result certification) addresses the simpler problem of checking that the result computed for a specific input is correct. In our application, the NC analyzer only needs to record the computations that led to the result that it produced, and their correctness can be established by checking the applicability of the computation rules and the accuracy of the numerical computations themselves.

We studied the feasibility of developing a proof-by-instance method for NC. In order to have high assurances about correctness, checking is performed within the kernel of the Isabelle proof assistant, based on a library for NC that we developed in Isabelle/HOL [START_REF] Nipkow | A Proof Assistant for Higher-Order Logic[END_REF]. As a side effect, this also increases our confidence in the version of NC underlying the PEGASE verifier.

We have produced a proof-of-concept implementation of this technique for the timing verification tool from the PEGASE project [START_REF] Boyer | The pegase project: Precise and scalable temporal analysis for aerospace communication systems with network calculus[END_REF], and have successfully applied this prototype to an industrial-size case study. Based on this experience we lay out a road-map of how a fullfledged result verifier could be developed that could play a valuable role in certifying network designs for embedded systems.

Product-based assurance for verification tools

Whereas formal methods promise high assurances for correctness, the cost of full-fledged proof remains prohibitively high in many cases, and the ability to scale up formal verification for usage in industrial applications has been questioned. Nevertheless, advances in formal methods research have resulted in techniques that have proved practical and effective for specific problems.

Our contribution is based on a technique that ensures the correctness of the results computed by the tool, not the tool itself. This approach is called "proof by instance" or "certificatebased result checking". In a nutshell, the tool outputs not only the result, but also a certificate for why the result is correct, for example a trace of the computation. The validity of the certificate can be established offline by a trusted checker. For tools used at design time, we argue that this approach has several advantages over proving the calculator correct.

Instrumenting the calculator for generating a trace is much easier, and hence less expensive, than attempting a full-fledged correctness proof.

Certificates should be designed in such a way that checking their correctness is essentially trivial. This is usually the case for checking the validity of the trace of a computation. Certifying the checker is therefore much easier than certifying the original tool.

The calculator producing the certificate is treated as a black box: it can be implemented using any software development process, programming language, and hardware by a tool provider separate from the checker. It can be updated without having to be re-qualified, as long as it still produces certifiable computation traces.

Proof by instance is a good match for industrial processes based on testing.

Checking the trace of an NC analyzer is similar to checking a mathematical proof: its computation consists in applying theorems of NC whose hypotheses need to be established, as well as the accuracy of calculation. We implemented our checker within the proof assistant Isabelle/HOL [START_REF] Nipkow | A Proof Assistant for Higher-Order Logic[END_REF]. A companion paper [START_REF] Mabille | Towards certifying network calculus[END_REF] describes this work from the perspective of interactive theorem proving. The correctness of our checker therefore relies on the correctness of the proof assistant, which in turn is reduced to the correctness of a relatively small kernel (a few thousand lines of ML code) that is mature and widely used.

Proof-by-instance applied to timing verification

Chain of trust

Figure 1 sketches the overall approach. The designer provides a network topology for which he wants to establish some timing bounds. These are computed by the NC tool, which also provides a trace of its computation. In the case of PEGASE, a trace contains calculations over certain classes of functions, as explained in section 3.2, as well as reasoning steps similar to a mathematical proof, corresponding to the network topology as explained in section 3.3.

The checker, separate from the NC analyzer, then verifies that all reasoning steps are justified and that all calculations are carried out correctly. The confidence in the correctness of the result therefore depends only on the trustworthiness of the checker, not on the implementation of the NC tool.

In order to implement a checker in the proof assistant Isabelle/HOL, one must write an Isabelle "theory" that contains a library of theorems of NC applied by the analyzer. This work is done once and for all. As a side benefit, formal proofs of these theorems give us high confidence in the correctness of the theory that underlies the analyzer. Result checking amounts to verifying that only valid instances of theorems appear in the trace. The communication between the analyzer and the checker is explained in more detail in Section 3.3.

t γ r ,b β R,T h(γ r ,b , β R,T ) t γ r ,b δ D δ D h(γ r ,b , δ D ) h(δ D , δ D )
Figure 2: Common curves and delay.

Illustration of Network Calculus computation

Network calculus [START_REF] Boudec | Network Calculus[END_REF] is a theory for computing upper bounds in networks. Network elements that introduce delays are modeled by servers, and resources, e.g. messages, that can be delayed, by flows. A flow is represented by its cumulative function f , where f (t) is the total number of bits sent by this flow up to time t. Hence the mathematical background of NC is a theory of the set of functions

F = { f : R ≥0 → R ≥0 ∪ {∞} | x ≤ y ⇒ f (x ) ≤ f (y) } (1)
that form a dioid under the operations and + defined as point-wise minimum and addition.

The network calculus theory also uses two operators, the min-plus convolution (⊕) and deconvolution ( ), and the associated Kleene closure, aka sub-additive closure.

(f ⊕ g)(t) = inf 0≤u≤t (f (t -u) + g(u)) (2) (f g)(t) = sup 0≤u (f (t + u) -g(u)) (3)
f ⊕ = δ 0 f (f ⊕ f ) (f ⊕ f ⊕ f ) • • • (4)
For practical applications, four families of functions are particularly interesting, which are defined as

δ d (t) = 0 if t ≤ d , ∞ otherwise, β R,T (t) = 0 if t ≤ T and R • (t -T )
otherwise, and γ r ,b (t) = 0 if t ≤ 0 and r • t + b otherwise. These functions are illustrated in Figure 2. The horizontal deviation between two functions, h(f , g) is also an operator of interest: no formal definition is given here, but an illustration is given in Figure 2.

The network calculus theory models the flows and servers with arrival and service curves. A flow A is said to have an arrival curve α (denoted A α) iff the amount of data sent by NC theory contains fundamental results relating these concepts. The basic one states that if a flow with arrival curve α crosses a server with service curve β, then the crossing delay d (A, S ) is bounded by h(α, β) and the output flow has arrival curve α β.

Producer - 1 MBit/s Switch1 θ 1 = 1µs - 10 MBit/s Switch2 θ 2 = 20µs - 5 MBit/s Consumer in γ r ,b S 1 β R 1 ,θ 1 mid S 2 β R 2 ,θ 2 out
A α S β A S -→ D d (A, S ) ≤ h(α, β) D α β (5)
In order to illustrate the use of Network Calculus theories on a simple example, let us consider the producer-consumer setup shown in Fig. 3. The producer sends at most one frame every T = 20 ms. We assume that the payload is of maximal size 980 bytes. Assuming an overhead of 20 bytes per frame, the maximum frame size is MFS = 8000 bits. This flow is sent to a consumer via two switches with switching delays θ 1 = 1 µs and θ 2 = 20 µs. The physical links between the producer, the switches, and the consumer have bandwidths of 1, 10 and 5 MBit/s, respectively.

The NC model appears in the lower part of Fig. Applying NC rules, one may determine arrival curves for the streams mid and out, and compute delays incurred by the frames at the two servers. For the first server, the maximum delay is 801 µs, whereas the delay at the second server is bounded by h(α mid , β 5,20 ) = 42102 25 µs. Consequently, the overall delay incurred by frames is bounded by 801 µs + 42102 25 µs = 62127 25 µs.

For the result to be trusted, one must be able to certify the computations of the individual results, and also ensure that composing intermediate results in sequence is correct w.r.t. the network topology, based on appropriate Isabelle theorems.

Checking the above computation is quite simple since it uses only rule ( 5), but in practice, analyzing a real network requires the use of dozens of rules, and the accuracy of the result depends on the choices of the appropriate theorems that were applied.

Tool chain

As explained in Section 3.1, the analyzer tool is completely separated from the result verifier. The analyzer is considered as a black box: it implements the NC algorithms and produces a trace (or certificate) that can be checked by the verification tool. Currently, the analyzer is a Java prototype developed from scratch, but our intention is to merge it into the RTaW-PEGASE AFDX analyser.

The verification tool is based on the Isabelle/HOL proof assistant augmented with dedicated NC libraries. Isabelle is a generic logical framework that provides syntax for defining logics and a trusted kernel for applying proof rules. Isabelle/HOL refers to the encoding of higher-order logic in this framework; it is the best-developed object logic within Isabelle and provides many convenience features for modeling and proving, including a language close to that of standard functional programming languages and interfaces to efficient automatic theorem provers. Nevertheless, ultimately all theorems proved in Isabelle/HOL are certified by the generic kernel.

We have developed Isabelle/HOL theories for encoding the basic objects of NC (including flows and servers) and their properties. In particular, these theorems contain machine-checked theorems of network calculus.

For a given network configuration, the NC analyzer computes upper bound on network delays ( 62127 25 µs in the example from Section 3.2), and produces a trace that gives information about how the result was obtained. In particular, the trace contains references to theorems used to obtain intermediate results (e.g., the value of α mid in the example from section 3.2). The checker inputs the trace and verifies that this reasoning is correct.

Road-map

Current prototype

In our current proof-of-concept implementation, the analyzer generates traces in the form of Isabelle proof scripts that are processed by the proof assistant in the context of our NC theories.

Using this prototype, we have been able to compute upper bounds for traversal times for a network drawn from an industrial case study (involving 8 switches and more than 5000 flows), and to provide a correctness proof for the computation. We compare this implementation to state-of-the-art tools, along three axes.

Accuracy of bounds. The current prototype implements only simple results of network calculus, for restricted classes of functions. The computed bounds are pessimistic compared to up-to-date implementations of network calculus [START_REF] Boyer | PEGASE, a robust and efficient tool for worst case network traversal time[END_REF]. In our case study, the bounds are overestimated by a factor of about 2.

Computation time.

Computing the bounds on delay and generating the traces takes a few minutes. Checking the generated traces requires about 8 hours on a standard laptop. These first results demonstrate the scalability of the approach, and the ability to handle realistic problems. Note that checking time is not really critical, since the checker needs only to be run on the final design when the architecture is believed to be stable, whereas intermediate results only require running the analyzer without checking.

Development effort.

Once the feasibility of the approach demonstrated, the very good news is that the development effort of such a formal tool was quite reasonable. Although we have not precisely tracked the effort that went into producing this prototype, we claim that the cost of the formal part (developing Isabelle theories and generating traces) represents less than 3/4 of the global effort. In other words, the overhead for developing a trustworthy version of a Network Calculus analyzer does not exceed a factor of 2 or 3, while using state-of-the-art techniques (documentations, testing, peer-review, etc.) often require a factor of 5 to 10.

From this experiments, we can draw a road-map for transforming the prototype to an efficient tool.

An Isabelle theory for network calculus

So far, only basic objects and results of network calculus have been formalized in the NC Isabelle library, and some well-known theorems have not been formally proved. The remaining work can be separated into two parts:

1. The first step is to write more theorem statements, in order to be able to have more accurate models of the networks, and more accurate bounds. For example, it is known from [START_REF] Grieu | Analyse et évaluation de techniques de commutation Ethernet pour l'interconnexion des systèmes avioniques[END_REF] that modelling the shaping in the network can improve the bounds by a factor of 40%. Notice that even if NC theorems are left unproved, this framework still ensures that each trace conforms to the tool specification, since the NC theory is the specification of the tool. Providing proofs for NC theorems will increase our confidence in the specification of the tool and in the fact that the results are meaningful for the actual system. In the absence of formal proofs, the coherence of the specification must be ensured by careful rereading by domain specialists.

Checking ( , +) operations on functions within Isabelle

NC theory uses operations on functions, including simple sum and minimum, but also more complicated ones such as convolution or deconvolution. The network calculus theory relies on such operations, based on their mathematical properties, but does not address their implementation. A correct implementation of these operations is important for the overall result to be correct.

Our current prototype uses very simple affine functions, whose implementation and proofs are straightforward. It is quite obvious, for example, considering two functions f (x ) = 3x + 2, g(x ) = 4x + 10 to prove that (f + g)(x ) = 7x + 12, (f g)(x ) = 3x + 2.

But to provide more accurate timing result, more general classes of functions must be supported. For example, a periodic flow sending a message of size s every T time unit can be represented by a linear function f (x ) = x T +s or a stair-case function g(x ) = s x T (see Figure 4). The function g is more accurate, and can lead to better bounds. But while computing the sum of two flows of sizes s and s , and period T and T is straightforward with linear functions, it requires a more general function representation with stair-case functions.

The class of piecewise linear concave and convex functions (see Figure 5) can represent local bursts, shaping, and long term rate, while having a simple representation and implementation of operators.

A very generic class, the ultimately pseudo-periodic functions, has been defined in [START_REF] Bouillard | An algorithmic toolbox for network calculus[END_REF]. It can represent any functions made of a set of piecewise linear segments, with a finite prefix and a periodic suffix. All algorithms implementing the basic operators (sum, minimum, convolution, deconvolution, etc.) over this class of functions are described in research papers but some corner cases are left out, and the implementation of complex algorithms is error-prone.

Each tool implements one or several classes of functions (an overview is presented in [START_REF] Boyer | NC-maude: a rewriting tool to play with network calculus[END_REF]), and, as expected, the more generic functions allow for more accurate models, and give better (i.e. smaller) bounds.

One way will be to identify some simpler classes of functions, like the one of [START_REF] Boyer | An efficient and simple class of functions to model arrival curve of packetised flows[END_REF], combining concave piecewise linear functions and stair-cases functions, providing good accuracy in timing analysis but allowing for full and reasonable straightforward Isabelle proofs.

Another way could be to handle partial computations, over only a finite horizon. Instead of computing a function f : R + → R for all possible arguments, one may consider a function f T such that f (x ) = f T (x ) only for x ≤ T . In some cases, such approximations are sufficient for computing bounds (see Figure 2).

Intermediate proof format

The current prototype outputs traces directly in Isabelle's input language. In the future, we plan to define a dedicated proof format, independent of Isabelle, for the following reasons:

1. A dedicated format will allow us to represent traces at the appropriate level of abstraction, whereas current proofs mix main results of network calculus such as [START_REF] Boyer | The pegase project: Precise and scalable temporal analysis for aerospace communication systems with network calculus[END_REF] and simple reductions of (in)equations such as a + b ≤ c, b ≥ 0 =⇒ a ≤ c. A dedicated format can be independent of any particular checker, and will be able to interface different NC tools and checkers.

2. It can be more compact (current proofs are quite long-winded) and thus enable more efficient checking, in space (smaller proofs) and time (avoiding to redo the same proof with different values, by creation of local lemmas).

3. Higher-level proof formats could be used to generate human-readable proof, for example as justifications for certification authorities.

Conclusion

Network Calculus has proven to be a powerful formalism that is well suited to provide guarantees on the worst-case performances of networks for large critical embedded systems, in particular in the avionics domain. The work described here provides insight on how a proof-by-instance technique can contribute to ensure the correctness of the results, thus helping turn a proof-of-concept verification software into an industrial-grade design tool. It also exhibits by-products of the approach such as a more coherent and formally checked theory and a more precise specification of tools.

Based on the successful development of a prototype, it gives a road-map for the development of a full efficient and trustworthy tool.

Figure 1 :

 1 Figure 1: Proof by instance process

Figure 3 :

 3 Figure 3: A simple system and its Network Calculus representation.

3 .

 3 Flow in is constrained by the arrival curve α in = γ r ,b where b equals MFS and r = MFS T = 8000 20×10 3 = 2 5 .

Figure 4 :Figure 5 : A concave piecewise linear function 2 .

 452 Figure 4: Affine and stair-case approximations of periodic flow


Andreas Junghanns

Jakob Mauss

Michael Seibt

Faster Development of AUTOSAR compliant ECUs through simulation

come   L'archive ouverte pluridisciplinaire

in AUTOSAR Builder, selected software components or compositions can be exported including an AUTOSAR OS (Operating System) and RTE (Run-Time Environment) as an FMU (Functional Mockup Unit). FMU [START_REF] Tatar | Automated test of the AMG Speedshift DCT control software[END_REF] is a new exchange format for models that has been developed in the EU-funded MODELISAR project (2008 -2011) and since then gained considerable acceptance across multiple industries and tools. The FMU can then be imported into the virtual ECU tool Silver (QTronic), where it can be co-simulated with vehicle models originating from a wide range of simulation tools, including Dymola, SimulationX, MapleSim and AMESim. Vehicle models are again provided as FMUs, or via proprietary binary export formats, typically Windows DLLs. Tools for measurement and calibration such as CANape (Vector Informatik) or INCA (ETAS) can then be connected to the virtual ECU running on PC, to directly measure or tune its parameters, like an engineer would do in a real car. Virtual ECUs are also used to move testing activities from test rigs and HiLs to Windows PC.

1

Introduction

Software for automotive ECUs is jointly developed by OEMs and their suppliers as shown in Fig. 1. Typically, a team of function developers uses a modelbased tool chain to develop a model of the ECU and to generate C code from that. The resulting C code is then compiled for the target processor, and the resulting ECU is validated and tested using test rigs, HiL systems, and road tests. Test and validation results are fed back to the developers, which closes the development cycle. See [START_REF] Mauss | Chip simulation used to run automotive software on PC[END_REF] for details and typical numbers. This process, although standard in the automotive industry today, has two major drawbacks:

• a single iteration takes days or weeks, that is, feedback reaches developers late

• the process depends on prototype vehicles and test rigs. These are typically rare resources during development. Their limited availability causes additional delays during development. This paper presents a tool chain that supports an improved development process. The key idea is to provide development engineers with virtual ECUs, which enables them to move many development tasks from test rigs and HiLs to Windows PC. As experience shows,this helps to shorten development cycles (down to 5 minutes for an incremental build) and to reduce the critical dependency to real hardware. We focus here on AUTOSAR projects, although the method does not depend on the framework (hand coded, model-based, AUTOSAR) used to develop the ECU.

The remaining paper is structured as follows: In the next section, we summarize various benefits of a virtual ECU for automotive development, with references to real applications. Section 3 explains how to build a virtual ECU for development projects that use the emerging AUTOSAR framework and section 4 demonstrates how to use the resulting virtual ECU on Windows PC to speed up development.

Virtual ECUs in the development process

Simulation has great potential to improve the development process for ECUs. It helps to move development tasks to PC, where they can often be performed faster, cheaper or better in many respects. In general, the speed-up generated with virtual ECUs is the product of three independent factors • Faster feedback on system level: On a PC, a development engineer can rebuild the entire ECU within 5 minutes after modification of a software module, thanks to incremental build, and test drive the result in a simulated environment. This helps detecting problems early on the developer's PC, and decreases the number of problems that show up late, when integrating all modules. As experience shows, such early checks speed up development.

• Independence of real time simulation: A virtual ECU might run on PC many times faster than in real time. When used in combination with test automation, a simple PC gives a higher test throughput than a considerable more expensive HiL test system. S. Gloss et. al. [START_REF] Gloss | Systematic validation of over 200 transmission variants[END_REF] To exploit these and other benefits when developing an ECU, the ECU must first be ported to a PC. This is typically done based on the C code of the ECU, which is either hand-coded, or generated by tools such as Ascet (ETAS), TargetLink (dSPACE) or Embedded Coder (MathWorks). For example, QTronic's virtual ECU tool Silver [START_REF] Junghanns | Building Virtual ECUs Quickly and Economically[END_REF] provides a framework to

• Compile given ECU tasks for Windows PC,

• Emulate the underlying RTOS and other services (CAN, XCP),

• Execute the resulting virtual ECU in a closed-loop with a simulated vehicle.

Typical applications are [START_REF] Gloss | Systematic validation of over 200 transmission variants[END_REF][START_REF] Junghanns | Building Virtual ECUs Quickly and Economically[END_REF][START_REF] Brückmann | Model-based Development of a Dual-Clutch Transmission using Rapid Prototyping and SiL[END_REF][START_REF] Tatar | Automated test of the AMG Speedshift DCT control software[END_REF], where a virtual ECU is used to develop the controller for an automatic transmission. For closed-loop simulation, vehicle models can be imported from many simulation tools into Silver, including MATLAB/Simulink, Dymola, SimulationX and MapleSim, e.g. through the FMI (Functional Mockup Interface) format for model exchange [START_REF] Blochwitz | Functional Mockup Interface 2.0: The Standard for Tool independent Exchange of Simulation Models[END_REF]. C code is not always available for implementing a virtual ECU, for example when all or major parts of the ECU have been developed by a supplier and the OEM that is interested in building a virtual ECU has therefore no access to the C source code. Silver supports such cases with a chip simulator [START_REF] Simons | Using Chip Simulation to optimize Engine Control. 7th Conference on Design of Experiments (DoE) in Engine Development[END_REF][START_REF] Mauss | Chip simulation used to run automotive software on PC[END_REF]. The chip simulator takes the binary code for the target processor (currently TriCore or PowerPC) and simulates the execution of the instructions by the target processor on a Windows PC.

Designing and testing a Virtual ECU with AUTOSAR Builder

An AUTOSAR authoring tool such as AUTOSAR Builder allows the modeling of a single ECU or a distributed embedded system based on templates defined by the AUTOSAR standard. To ensure the validity and completeness of an AUTOSAR description, consistency or design rule checks have to be applied iteratively. Once this step has been passed, unit-testing can be performed by simulating single Software Components (SWCs) or even full compositions (CSWCs) that also take a real AUTOSAR OS and RTE into account. The application code (which can be manually coded or auto-generated) needs to be provided as source or compiled. In addition the test vectors need to be defined through a dedicated environment or can be imported. Everything else, including the OS and the RTE configuration and the Testbench is generated automatically. Once the SWCs or CSWCs have passed the tests in simulation, they can be exported as FMUs including the AUTOSAR OS and RTE. 3

Running a simulation in Silver

A virtual ECU exported from AUTOSAR Builder as FMU can be loaded into the Silver runtime environment, which runs on Windows. Fig. 2 shows a screen shot of Silver with the transmission controller EGS exported with AUTOSAR Builder loaded as virtual ECU. Besides the virtual ECU, also a vehicle model developed in Dymola / Modelica has been loaded into Silver, which enables closed-loop execution of the transmission controller. The tree shown on the left of the Silver window shows all loaded modules, and their input and output variables.

In real projects, this tree might contain hundred thousands of scalar variables. Silver has been optimized to efficiently deal with such large models. The top-right part of the Silver window contains the plotters, gauges, sliders, and push buttons configured by the development engineer to interact with the vehicle model. In the case shown here, the engineer can start the engine, switch the PRND lever to any position, accelerate and brake using sliders, and watch the temperatures of the transmission brakes and clutches, and other key variables of the vehicle.

Once loaded into Silver, the services shown in Fig. 4 are available to implement various engineering tasks.

Example uses cases are: • Drive the simulation using a Python script. Python scripting can be used to implement reactive tests (including e. g. 'do until' test steps) or an optimization loop that automatically calibrates ECU software parameters using mathematical optimization.

4

Conclusion

As demonstrated above, virtual ECUs help to move development tasks to a PC, which speeds up automotive embedded systems development tremendously. We have demonstrated a technical realization of virtual ECUs for the special case of AUTOSAR. Silver supports the same idea also for ECUs that run software generated with non-AUTOSAR tool chains. Use of virtual ECUs is increasing but not yet wide-spread in the automotive industry today. We expect to see significant growth of automotive applications in the coming years, mainly driven by the speed up of development that can be achieved as outlined in this paper.

Fig 1 :

 1 Fig 1: Development of automotive ECUs

Fig 3

 3 Fig 3 shows a screen shot of AUTOSAR Builder, with an AUTOSAR software component EGS1 (a simple controller for a 6-speed automatic transmission) loaded. AUTOSAR Builder provides means to export this controller as an FMU for Co-Simulation or Model Exchange [5].

Fig 2 :

 2 Fig 2: Simulation of an AUTOSAR Software Component in Silver

Fig 3 :

 3 Fig 3: AUTOSAR Builder in simulation mode

Fig 4 :

 4 Fig 4: The Silver runtime environment for virtual ECUs

•

  Parallelization: Virtual ECUs help to split development into parallel threads. With virtual ECUs, many development tasks can be moved from shared resources (vehicles, test rigs, HiL) to PC, where engineers can work in parallel, without blocking each other.

  reports how this effect is exploited to test 200 variants of a transmission controller.Other points that illustrate the benefit of virtual ECUs: • On a PC, an engineer can easily "freeze time", i. e.

	Exact reproduction of experiments is difficult or
	impossible on a HiL or test rig, due to non-
	deterministic effects. • Having a PC-based solution, a calibration tool like INCA (ETAS) or CANape (Vector) can be
	connected to a virtual ECU via XCP to measure
	into a running simulation and to tune
	characteristics online. In this way, many
	parameters of an ECU can be tuned using a
	relatively cheap and highly available PC platform,
	without blocking rare and more expensive
	resources like physical prototypes and test rigs.
	• A virtual ECU runs independent from real time and can hence also easily be coupled with very
	time consuming simulations, such as combustion
	simulation. This is impossible for test rigs or HiL
	systems, where all parts of the simulation must run
	in real-time.

stop simulation and inspect the call stack and all variables of a virtual (i. e. simulated) ECU without bandwidth limitation and repeat a simulation deterministically as often as needed. In contrast, a real ECU being used in a HiL environment or test rig must run in real time. Stopping and stepping is impossible then, or requires considerable extra effort, e. g. based on the JTAG debug interface.

  Drive the virtual vehicle interactively on PC to explore behaviour of the virtual ECU, without limitations of how much or what can be measured during simulation. • Drive the simulation using measured data, available as MDF, DAT or CSV file. This can be used to implement open-loop tests of the virtual ECU. In simple cases, this does not even require a vehicle model: the virtual ECU is then directly driven by measurements.

	parameters during simulation. This approach
	allows the expertise of calibration engineers with
	INCA or CANape to be also available in the PC
	environment.
	• Connect INCA (ETAS) or CANape (Vector) to the virtual ECU via the extended CAN calibration
	protocol (XCP, an ASAM standard) to diagnose a
	running simulation and to tune software

• Import a vehicle model from simulation tools such as Dymola, SimulationX, MapleSim, AMESim, Simulink, GT-Power, or axisuite.

• Connect a test automation solution to Silver, to test the ECU on a PC as shown in

[START_REF] Gloss | Systematic validation of over 200 transmission variants[END_REF]

and

[START_REF] Tatar | Systematic Test and Validation of Complex Embedded Systems[END_REF]

. • Connect Visual Studio Debugger to the virtual ECU, define code or data breakpoint and debug the virtual ECU at the code level, e.g. to fix problems found by test automation. Virtual ECUs running in a fully simulated environment on PC are particularly attractive here, because the corresponding step-debug functionality is much harder or impossible to achieve in a real-time environment. •


Thierry Le

Alain Le Guennec

Data-Based System Engineering: ICDs management with SysML

Keywords: Model Based System Engineering, Software Engineering, SysML, ICD

. These clearly define the development and verification processes including system requirements, functional decomposition, and architecture design.

 specifically to support the system engineering development processes through models. The benefits of models versus Documents-based processes has been highlighted in many papers; it allows in particular, automated verification of design consistency.

 that is at the center of most industries' system engineering processes, and that is not supported in a straightforward way by SysML.

.

Introduction

Interface Control Documents, know as ICDs, are widely used in all industries, at different levels of the system development and verification processes. One definition, independent from the standards, is given at http://www.chambers.com.au/glossary: "An Interface Control Document (ICD) describes the interworking of two elements of a system that share a common interface. For example, a communications interface is described in terms of data items and messages passed, protocols observed and timing and sequencing of events. An ICD may also describe the interaction between a user and the system, a software component and a hardware device or two software components. This class of document is typically used where complex interfaces exist between components that are being developed by different teams. It is jointly prepared by the interfacing groups."

As many teams are involved at different levels, different times, and different expertise, in the development of complex systems, the difficulty faced by industries is to manage the consistency of the interface of each individual component of the system, from the textual requirements to the detailed specification of the interfaces for the development of each component separately. 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".

The manner proposed in this paper is to rely on model-based technologies to manage all required information in a consistent model and generate the ICDs from the model.

That model shall:

 Handle "data" that is the information exchanged by each item of the system (as stated in [START_REF]NASA Systems Engineering Handbook[END_REF], it can be "cognitive, external, internal, functional, or physical")  Handle the system architecture topology(ies) (there may be different architectures; functional, logical, physical)  Handle fine grain traceability with textual requirements and allow impact analysis of requirements or design changes This paper details the development of ICDs from the tool point of view; it answers to the question "what features shall be supported by an integrated toolset to support a model-based development of ICDs that ensure efficiency of user work and consistency of the result. Other aspects, such as organizations, qualification w.r.t. standard such as DO-1178C are not elaborated here.

The paper is structured in the following way:

First, the principal item of ICDs, the data, is discussed. Second, a major issue with SysML is explained, and a solution is proposed. This allows the third section to show how data and system architecture topology specified in SysML can be reconciled. The last section can then cover the complete process development, from the textual requirements, to the generation of consistent ICDs, and the initialization of the development of software components.

Data dictionary

A common technique used for the development of complex software predominant systems relies on a set of "data" exchanged between the software components of the system.

These databases are used as detailed specifications exchanged between OEM and equipment manufacturers. Also, a set of in-house tools have been developed over the years for verification activities and code generation, so it is important for a new system engineering tool to be able to import and export data dictionaries saved in these databases.

The inconvenience of the management of these data with databases is that they are technically separated from the model defined in the system engineering tool. Keeping the information coherent, such as data names and topological information (source and target of each data), is a challenge.

The solution proposed is the following:

1. Data can be defined as SysML values of a block, with a name and a datatype, on which a set of properties can be defined (see more details below), 2. Data are managed in tables allowing easy find/sort/filtering and direct editing of their properties, 3. Tables of data can be exported/imported as .csv files, allowing inter-exchange with external databases, 4. Data can be allocated on SysML connectors or ports. These steps are detailed here.

Data properties

Data, functional or logical, shall carry information, such as value range, timing information, position in a message frame, etc. Defining this set of properties and the value for these properties must be supported in a friendly way by the engineering tool. The technical foundation of SCADE System, the Eclipse MDT Papyrus project [6], allows for defining such information through the standard profiling mechanism. This customization has the advantage of being an effective standard. But, the profiling mechanism is a rather low-level mechanism, not easily managed by system engineers who are experts in their domain but not necessarily in UML technology.

To provide the necessary means to system engineers, SCADE System comes with an annotation mechanism reused from the SCADE Suite® toolset [START_REF]Esterel technologies SCADE products[END_REF] that has been proven to be very effective in many complex industrial projects. A simple textual language allows defining structured information types (aka "annotation schema") associated to any model object, e.g. the SysML block values, that implement the data. Annotations are transparently implemented in terms of UML profiles, for interoperability's sake.

The data and allocations done as part of the model are, of course, traced with high-level requirements where appropriate, and reported in the documentation generated automatically.

Import/export data

As all model objects, data are presented in the object tree view of the IDE. A table representation is also available both to provide a comprehensive view of the data defined in a block, with customizable columns to display any data properties, are as the key pivot for import/export capability to common separated value (.csv) files or MS-Excel tool as presented in the following screenshot.

The column of SCADE System tables are not simple textual columns; they are associated to the data properties, as defined in the previous section, or predefined property, for example the datatype property inherited from the SysML definition. Exporting content of these tables to Excel or .csv files is a straightforward copy of the string contained in each cell. Importing is more challenging, as the textual information imported becomes model information. In particular the string "pasted" in the Type column is automatically bound to datatype with the same name available in the visibility scope of the block. If such datatype is not available in the model, a feedback is given to the user to enrich the model.

As the amount of data can be considerable in an industrial model, a specific caution has been taken in the development of Papyrus to support of tables of more than 10.000 lines.

Data allocation on topology

The key aspect of the methodology proposed is to "map" the data as defined in the previous section to the architecture topology defined as a SysML model.

The constructs used from SysML to define an architecture topology are only the Packages, Blocks, Flow Ports, and connectors. The mapping is realized by SysML allocations.

The following figures introduce, with a simple example, the proposed modeling style. More details are given in the remaining portion of the paper after a major SysML issue is detailed in the next section, as it must be solved beforehand. Note that SysML allocations are also supported in SCADE System tables, allowing a more scalable view than the nice, but limited to the size computer screen, graphical representation. This also allows for import/export capability.

Challenges with SysML

One main issue to deal with is the "multi-instantiation" of architecture components; it is indeed a great benefit of modeling language, such as SysML, to support the definition of "blocks", whatever they represent, that can be reused several times in the model through "part". This feature is naturally used to model the fact that, for example, an equipment is "duplicated" in the system.

Without entering the formal definition of SysML parts versus. blocks, the following example highlights the issue system engineers are faced with for the specification of information related to each individual component.

The model as specified with a SysML Block Definition Diagram on the left side of the following figure represents a Car with four Wheels, FLW (Front Left Wheel), FRW, RLW, RRW, each Wheel containing one tire.

Classical SysML modeling tools handle model objects, as pictured in the tree view in the center of the following figure: flat list of blocks, each containing parts. The problem arises on the second level of the "conceptual hierarchy": the tools handle only one object to represent the four conceptual tires. There is no direct mean to specify, e.g. the pressure of each of the four tires as there is only one "object handle". It is not possible to specify that the tires on the left side of the car are allocated to a worker on the left side of the manufacturing chain, while the tires on the right side of the car are allocated to a worker on the right side of the manufacturing chain. Trying to set such allocations leads to the allocation of all tires (in fact _the_ object tire) to both the LeftWorker and RightWorker, as pictured on the right side of the figure with the SysML Internal Block Diagram representing the car; all tire graphical representations are bound to the same object.

The straightforward means used in practice consists in copying the block Wheel as many times as needed, leading the system engineers to manage, manually, the consistency of the copies.

To allow system engineers to manage, in a straightforward manner, their architecture designs, SCADE System manages, automatically, the "replica" from the specification specified with blocks and parts as in the BDD shown above. All intermediate "blocks" and "inheritances" are automatically created internally to comply with the SysML standard, and are managed by the tool to remain consistent with the user design. A simple view, as shown in the following picture, is shown to the user; it abstracts the internal objects, but provides "handles" allowing setting property value and allocations to individual conceptual component.

Thanks to this management, data and architecture topology can now be assembled taking into account the replication of component defined once through block types.

Data and topology reconciliation

Managing a huge set of data in an industrial model is cumbersome. Two mechanisms facilitate this management:

1. Automatic replication of the data produced by component replica, 2. Propagation of the data along the hierarchical architecture,

Data in blocks

Data being implemented as SysML properties of the blocks, the replication of blocks detailed in the previous section is of great help to manage the data. Consider the example presented in the following figure .   Block2 contains two identical parts, Part1 and Part2, defined from the block Block1. The "internal interface" of these parts are the same; it is made of data Label_001, Label_002 and Label_003, defined in Block1 (for example imported from a .csv file), allocated to its port A429_Out. Now, in Block2, these data must represent different information. The replication of Block1 handled by the tool makes the data produced by the two parts indeed different information, accessed from Block2 through a single path. As shown in the next section, aliasing these names with names local to Block2 is also possible.

Data propagation

Independently of the multi-instantiation topic discussed in the previous sections, propagating data along a path of connectors through intermediate levels of blocks would be better supported by tools than requiring many manual, error prone, actions. An interactive IDE allows the system integrator to efficiently specify how the data are propagated in the model. Data is not necessarily defined in the block producer as shown in the previous section. It should also be possible to define all data in one upper block, for example allowing the import of a global data dictionary. Data could also be defined on the recipient side so that a block comes as a standalone component defining its complete interface independently from the way it is connected.

Data propagation consists of specifying, without ambiguities at any interface connected to several connectors, how each data is broadcasted or multi-casted through the connectors. For that purpose SCADE System offers an interactive window showing, for each connector selected, the list of data provided and required on both ends. Three actions are proposed:

 "Pushing" a data from source to target,  "Pushing" a data from target to source,  "Binding" data selected on the right and left side.

At the end, before generating ICDs, it is also important to verify globally on the model that the propagations have been kept consistent, in particular after model topology modification. To support that needed feature, SCADE System comes with a checker that automates the verification of rules that can be customized to adapt to the precise methodology defined. Typical rules would be:  All defined data is produced, i.e. allocated to an output port  No data is "lost" in intermediate connections

 No data arrive ex-nihilo on intermediate connections  Etc.
The technical means proposed for data propagation is detailed below. It enforces an important property: all allocations between data and block ports is local to block. This allows:

 The automated replication of the dependencies with block replica,  The capability to "export", and then re-integrate, standalone blocks for efficient collaborative work.

A data of a block is considered as produced by the block (a "provided data" of the block) if it is allocated to an output port of the block. Symmetrically, a data of a block is considered as consumed by the block (a "required data" of the block) if it is allocated to an input port of the block. Data of a block that are not allocated to any port are internal data of the block.

When a block is used as a part of another block, the provided and required data corresponding to that part are automatically transposed into the enclosing block to make them available there. Initially, those data are internal data of the enclosing block (until they are themselves allocated to ports of the enclosing block, possibly), and are bound to the corresponding data in the inner block; binding between two data means they represent the same data but possibly at different levels in the hierarchy and under possibly different names. The initial name of the transposed data is formed by the qualified name of the data being transposed (but that initial name can later be changed for readability), and so on recursively.

Example:

If a block 'B' contains two parts 'c1' and 'c2' typed by a block 'C' having one data 'd' connected to a port of 'C', then two data are automatically transposed in 'B':  'c1'.'d'  'c1.d' (can be later renamed by the user to 'd1' for example)  'c2'.'d'  'c2.d' (can be later renamed by the user to 'd2' for example)

The binding relation forms equivalence sets (the set of data bound together). There must be at most one producer in the set. For any consumed data, it is possible to retrieve the producer, if any.

The propagation consists simply in binding data. The tool helps in creating the missing data and its allocation to the port. On each connector end, the local data allocated to the end connector port (for a port of the block), or local data bound to a data allocated to the port of an inner part, is proposed for propagation through that connector. From the selection of one of these proposed data there are three propagation cases:

 A corresponding data already exists at the other connector end: a simple binding between the two data implements the propagation.  Upward propagation: the data to propagate is already allocated to the port of the inner part; so it has been transposed upwards in the block. Upward propagation consists of allocating the transposed data to the port of the block. Note that this leads automatically to the creation of a new transposed data in each block containing a part of that block, allowing further propagation of the data.  Downward propagation: the tool creates a new data in the nested block on the other side of the connector and allocates it to the connected port of the nested block. This data is therefore transposed upwards at the same level as the connector, where it will be bound to the initial data. An optimization in downward propagation consists in binding directly the outer data to the just created inner data. At the top of the picture, downward propagation is highlighted: OFV_SpeedCommand is allocated to the out port of Compute1A, so transposed data (renamed) y1 is created by the tool. User propagates it upward until block CPCS, then downward until OFC_Actuator, local data named y6. In OFV_AutoChannel1_Board1 a data SpeedCommand is defined and allocated to the port, so a transpose data z1 is automatically created. Propagating y6 to SpeedCommand is realized through the binding between y6 and z1.

Data grouping can also be defined within a block to aggregate other data (including other data group). When a data-group is allocated to a port or connector, all its data are considered to be allocated too. When a data-group is transposed upwards in the block hierarchy, it becomes the group of its transposed data. This allows propagating data more quickly, by grouping them when they are related.

ICDs system development process

System development and verification processes involve many steps that are out of the scope of this paper.

A comprehensive methodology handbook for the aeronautic domain can be found in [START_REF]Efficient Avionics Systems Engineering with ARP-4754A Objectives Using SCADE System[END_REF]. The focus of this paper is on the technical aspects of the production of ICDs. From the tool features detailed in the previous sections, an efficient tool supported development process for the ICDs can be set-up.

The tool itself does not impose a particular process; several ways can be followed. In particular, the System Engineering development process can rely of several refinement layers, e.g. functional, logical and physical, that are domain and company dependent.

The overall process can be applied in the same way at any system development level; it consists in:

1. Definition of the data in items of the system and use a traceability tool to establish a link between these model elements and the requirements defined in textual documents. 2. Specify the connections between the components, and propagate the data along this topology. 3. Verify the consistency of the model with automated rule checker such as SCADE System checker. 4. Extract information from the consistent model: ICDs tables, reports, and SCADE Suite operators interfaces for critical software components to be developed with SCADE Suite [START_REF] Halbwachs | The Synchronous Dataflow Programming Language LUSTRE[END_REF][START_REF]A Conservative Extension of Synchronous Dataflow with State Machines[END_REF]12].

Step 1 can be mainly manual in particular for a totally new system, or heavily rely on the SCADE System import feature when a large part of the data pre-exists from a previously developed similar system. Traceability is supported by the SCADE LifeCycle Requirements Management gateway tool. It allows straightforward impact analysis when requirements are modified.

Steps 2 and 3 are detailed in the previous section. The important thing is that the checking rules are customized to verify that the methodology defined by the method team has been followed by the designers.

Step 4 is now detailed in the two sections below. When the system development process is set-up in several refinement layers a possible usage of the technics presented is the following:

 As part of the functional analysis of the considered subsystem, the functional data exchanged between the functions are defined and allocated on the connectors representing the flow dependencies between the functions,  When the architecture of the system is defined and the functions are allocated to the architecture components, one has to define how the functional data shall be implemented. This is done by defining, using the same tool feature, logical data. The functional data are allocated on the logical data, which in turn are allocated on the architecture topological elements, connectors or ports,  In complex architectures where data are packed/unpacked at several architecture levels, the mechanism can be used again, modeling that several logical data can be transported by e.g. a message, itself defined as a data allocated to topological elements. This later step involving binary encoding and communication protocols has not been yet investigated; we consider for now in the paper the functional or logical architecture only.

Customizable ICDs tables

Once the data are properly managed in the model, generating ICDs becomes easy as all the required information is consistently managed in the tool. The tool offers an Applicative Programing Interface (API) to traverse, verify and extract any information for documentation generation from a program or script.

The SCADE System tool goes a bit further in providing customizable tables: in any block, table of its data can be displayed, showing in columns the properties set in annotations attached to the data. Query columns can also be specified: through simple user defined scripts interacting with the model API, these columns can be filled with e.g. any information extracted from the model. For example the table display below can be easy specified:

In addition to the name and datatype of the data, its user defined properties "Min", "Max", "SafetyLevel" and "Note" are displayed. The content of the user defined "Recipient" column is the result of a query providing the name of the final block owning a port onto which the data is allocated. The blocks can be defined as "final" with e.g. another annotation. In a similar way, the content of the "Communication" column is the result of a query providing the content of a specific annotation set to one of theconnectors through which the data "circulate" (i.e. data allocated to its two ends).

All the information required in ICDs tables can be customized with a few scripts, allowing an always up-todate representation of the ICDs. And as SCADE System tables can be exported in a click to .csv files, there' is no need to develop dedicated model reporter or gateway to external data bases.

Synchronization with SCADE Suite software development tool

Once the system description is complete and checked, the individual software blocks in the system can be refined in the form of models in SCADE Suite. Automatic and DO-178B Level A-qualified code generation can be applied to the SCADE Suite models.

A mapping between SysML block interface and SCADE Suite operator interface has been formally defined and implemented in SCADE System Synchronizer [START_REF]Esterel technologies SCADE products[END_REF].

The SCADE System Synchronizer tool has been extended to support this new way of specifying block interfaces. Instead of synchronizing the block ports with SCADE Suite operator inputs and outputs, it relies on the data allocated to these ports. The following figure shows the result of the synchronization between such SCADE System block and SCADE Suite. The datatype themselves are translated on user request as detailed in [START_REF] Le Guennec | Bridging UML and Safety-Critical Software Development Environments[END_REF].

Conclusion

Keeping ICDs consistent with architecture design drawn with Visio-like tools is not easy and not efficiently done with reviews. Managing models make things much more efficient.

The SCADE System tool proposes a method and tool features to manage Interface Control Document (ICDs) in a model based way that is compliant to the SysML standard.

It relies on block values and annotations transparently implemented in terms of UML profiles. Data dictionaries are managed with tables that can be customizable to show any information required with the various ICDs. The key feature for a friendly IDE is to manage in a proper way the multi-instantiation and propagation of data; these features are implemented in the SCADE System product.

Finally, the interface of software critical components can be generated automatically from the system model.

The solution reconciles the benefits of model based technology with the deployed system engineering processes based on ICDs. Evaluations are engaged in large aeronautic projects at the time this paper is released.

  The result of this propagation is shown in the following figure representing a realistic model of an aircraft Cabin Pressure Control System (CPCS). Allocations are represented as plain arrows, binding represented as dashed arrows.At the bottom of the picture: As data Pressure1 of PressureSensor1A is allocated to its port, a transpose data PressureSensor1A.Pressure1 (default name) is automatically created by the tool. Same for CabinePressure1 from parts Compute1A and Monitoring1A, transpose data renamed x1 and x2 to make the name fit in the picture. Upward propagation of x1 and x2 is realized with their allocation on the input port of CPU_1A; this creates transposed data x3 and x4. Propagating horizontally the data is realized through the binding between PressureSensor1A.Pressure1 and x3 and x4.