Michel Batteux
email: michel.batteux@irt-systemx.fr

Tatiana Prosvirnova
email: tatiana.prosvirnova@onera.fr

Antoine Rauzy
email: antoine.rauzy@ntnu.no

Model synchronization: a formal framework for the management of heterogeneous models

Keywords: Heterogeneous models, model synchronization, S2ML

In this article, we present the conceptual foundations and implementation principles of model synchronization, a formal framework for the management of heterogeneous models. The proposed approach relies on S2ML (System Structure Modeling Language) as a pivot language. We show, by means of a case study, that model synchronization can be used to ensure the consistency between system architecture models designed with Capella and safety models written in AltaRica 3.0.

Introduction

To face the increasing complexity of technical systems, systems engineers are designing models. These models serve different purposes: system architecture, control engineering, multi-physics simulation, safety analyses, performance assessments. They are designed at different levels of abstraction and by different teams. They may have also different levels of maturity. Ensuring that these models are consistent one another is one of today's major industrial challenges. As of today, their integration relies almost exclusively on organizational processes.

Collaborative data bases (PDM/PLM) and tools to set up traceability links between models provide a support to manage models in version and configuration, but not to ensure consistency between them. Different model transformation techniques have been proposed (e.g. [START_REF] Mauborgne | Operational and system hazard analysis in a safe systems requirement engineering process application to automotive industry[END_REF], [START_REF] Yakymets | Sophia framework for model-based safety analysis[END_REF]) but they often assume a master/slaves organization of models, which is not realistic in practice. As an interesting alternative, two-sided model transformation based on triple graph grammars has been proposed see e.g. [START_REF] Hermann | Model synchronization based on triple graph grammars: Correctness, completeness and invertibility[END_REF].

In this article, we present the conceptual foundations and implementation principles of model synchronization, a formal framework to ensure the consistency of heterogeneous models. Model synchronization relies on ideas stemmed from Cousot's abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints[END_REF], but its implementation is dedicated to the problem at stake. Namely, the overall approach relies on four theses: Thesis 1. The diversity of models is irreducible. Moreover, each model has its own life-cycle. In other words, attempts to derive models for one purpose (e.g. safety analyses) from models designed for another purpose (e.g. system architecture), are essentially vain and even counter-productive. Thesis 2. Heterogeneous models cannot be compared directly. Therefore, the synchronization process is made of three steps: first, models are abstracted in a common language; second, their abstractions are compared; third, actions are possibly taken to adjust original models according to findings of the comparison. Thesis 3. Systems engineering models are made of two types of constructs: behavioral descriptions and structuring constructs. Behavioral descriptions are specific to each engineering domain. It is thus in general impossible to perform crossdomain comparisons. On the contrary, the structures of models reflect to some extent the structure of the system under study. Therefore, model synchronization focuses on structural comparisons. Thesis 4. The overall objective of model synchronization is not to reach a perfect matching between (the structures of) original models. Rather, it is to agree on disagreements and to trace the possible discrepancies.

In a word, model synchronization is a pragmatic approach providing a formal framework and concrete tools to improve current processes. Its implementation relies on three basic constituents: first, one needs a pivot language in which models are abstracted. S2ML (System Structure Modeling Language) [START_REF] Batteux | From models of structures to structures of models[END_REF] is an excellent candidate for this purpose as it gathers in an organized and unified way most of the structuring constructs found in systems engineering modeling formalisms. Second, one needs tools to abstract original models into the pivot language. Ideally, the abstraction process should be fully automated. It is possible however to do this part of the work by hand or in a semi-automated way. Finally, one needs software tools to compare abstractions. The development of these tools is justified for at least two reasons: first, they depend only on the pivot language and are therefore reusable for the synchronization of any type of models; second, they ensure the soundness, the completeness and the traceability of the comparison process.

The contribution of this article is thus to present model synchronization and to discuss its conceptual foundations and its implementation into the SmartSync platform. We illustrate the discussion by applying the proposed approach on a case study -an electrical power supply system borrowed from [START_REF] Bouissou | A new formalism that combines advantages of fault-trees and Markov models: Boolean Logic Driven Markov Processes[END_REF]. We show how it can be used to maintain the consistency between system architecture models designed with Capella [START_REF] Roques | MBSE with the ARCADIA Method and the Capella Tool[END_REF] and safety models written in AltaRica 3.0 [START_REF] Batteux | Altarica 3.0 in 10 modeling patterns[END_REF].

The remainder of this article is organized as follows. Section 2 introduces the case study. Section 3 describes the model synchronization process. Section 4 discusses model comparison. Section 5 presents the SmartSync platform and gives some experimental results. Finally, section 6 concludes this article and discusses future works.

Illustrative Example

Description

As an illustrative example, we shall consider a power supply system borrowed from [START_REF] Bouissou | A new formalism that combines advantages of fault-trees and Markov models: Boolean Logic Driven Markov Processes[END_REF] and pictured Fig. 1. We shall use this case study to illustrate the different concepts of model synchronization, i.e. to show how to ensure consistency of heterogeneous models. Fig. 1. A power supply system

This system is in charge of supplying electrical power to the busbar BB. It is divided into a primary power supply or a backup power supply. The primary power supply receives the power from the grid and is itself made of two redundant lines. Each of lines is made of a transformer TRi and two circuit breakers CBUi and CBDi, i = 1, 2. Lines 1 and 2 are used in alternation. The passive one is in cold redundancy with the active one. The backup power supply part is made of the diesel generator DG and the circuit breaker CB3. It is in cold redundancy with the primary power supply.

Models

We consider this system from two engineering point of views: the point view of the system architect, supported by models designed in Capella [START_REF] Roques | MBSE with the ARCADIA Method and the Capella Tool[END_REF], and the point view of the safety analyst, supported by models written in AltaRica 3.0 [START_REF] Batteux | Altarica 3.0 in 10 modeling patterns[END_REF].

Fig. 2 shows the functional architecture diagram of the power supply system, while Fig. 3 presents its physical architecture diagram. The latter is quite similar to the process and instrumentation diagram showed Fig. 1. Fig. 4 on the left represents the life-cycle diagram of the operational architecture. Table 1 summarizes the allocation between functions and physical components depending on different operational phases of the system. Phase 1 corresponds to the mode Line1 of the diagram Fig. 4, Phase 2 corresponds to the mode Line2, and Emergency mode -to the mode Backup. Fig. 5 shows an excerpt of the AltaRica code for the power supply system. There are two failure conditions of interest: loss of electrical power delivered to the busbar and loss of isolation (of non-functioning parts). They are represented by two observers in the AltaRica model.The structure of the model is inspired by the phased-mission systems modeling pattern [START_REF] Batteux | Reliability assessment of phased-mission systems with AltaRica 3.0[END_REF] and is close to the structure of the Capella model. The block Controller, which graphical representation is sketched in Fig. 4 on the right, corresponds to the life-cycle diagram given Fig. 4 on the left, the block Functional -to the functional architecture diagram given Fig. 2 and the block Physical to the physical architecture diagram given Fig. 3. The allocation of functions (see Table 1) is represented by the aggregation relation ("embeds" clause). For instance, the function SupplyPowerByGrid aggregates the grid, the circuit breakers and the transformer of the Line 1 of the primary power supply system in the phase 1.

System architecture and safety analyses can be seen as two faces of the same medal. System architecture focuses on how the system works, what it should do and should be. It is ruled by so-called architectural frameworks such as the CESAM framework [START_REF] Krob | CESAM: CESAMES Systems Architecting Method: A Pocket Guide[END_REF]. Safety analyses focus on how the system may fail and what are the consequences of failures.

Although they consider the system at about the same level of abstraction, models designed by system architects and safety analysts are quite different. In particular, the former are pragmatic while the latter are formal [START_REF] Rauzy | Foundations for model-based systems engineering and model-based safety assessment[END_REF], two characteristics that we shall define formally in the next section. Ensuring the consistency of these models is thus both extremely important and far from easy.

Model Synchronization

Models = Behaviors + Structures

Ensuring the consistency of two or more heterogeneous models requires to understand the nature and the role of each of these models. Models involved in systems engineering serve actually very different purposes. They can be roughly separated into two categories [START_REF] Rauzy | Foundations for model-based systems engineering and model-based safety assessment[END_REF]:

-Pragmatic models that are used primarily to support the communication amongst stakeholders.

-Formal models that are used primarily to calculate indicators or to perform simulations.

The latter encode eventually mathematical objects. Their syntax and their semantics must be perfectly defined. They are written in modeling languages such as Modelica [START_REF] Fritzson | Principles of ObjectOriented Modeling and Simulation with Modelica 3.3: A CyberPhysical Approach[END_REF], Matlab Simulink [START_REF] Klee | Simulation of Dynamic Systems with MATLAB and Simulink[END_REF] or AltaRica [START_REF] Batteux | Altarica 3.0 in 10 modeling patterns[END_REF]. On the contrary, the former can only be understood by referring to the system under study. They are often written in standardized graphical notations such as SysML [START_REF] Friedenthal | A Practical Guide to SysML: The Systems Modeling Language[END_REF] or Capella [START_REF] Roques | MBSE with the ARCADIA Method and the Capella Tool[END_REF].

For this reason, they have no formal syntax and even less a formal semantics. Note that formal languages could be used to design pragmatic models (the reverse is indeed not true). However, there is an epistemic gap between pragmatic and formal models: as the former aim primarily at supporting the communication, they keep a lot of knowledge implicit. Making this knowledge explicit would overload them uselessly. Even if we restrict our attention to formal models, their underlying mathematical frameworks can be very different, e.g. systems of ordinary differential equations for Modelica and Simulink and guarded transition systems for AltaRica. This is the reason why, comparing behaviors described by heterogeneous models is essentially meaningless: the comparison should focus on the structural part of models.

Systems engineering modeling formalisms and languages are actually made of two parts: an underlying mathematical model, that aims at describing behaviors, and a structuring paradigm that makes it possible to organize models, i.e. to design them by assembling parts into hierarchical descriptions. The structural parts of SysML and Capella are stemmed from prototype-oriented programming [START_REF] Noble | Prototype-Based Programming: Concepts, Languages and Applications[END_REF], although without clearly acknowledging it. Modelica and Simulink rely on object-orientation. AltaRica 3.0 relies on a combination of both.

Model Synchronization Principle

As already said, two models, possibly written into two different languages, cannot in general be compared directly, see [START_REF] Stephan | A survey of model comparison approaches and applications[END_REF] for an interesting survey on model comparison techniques. Therefore, the synchronization process is made of three steps: first, models are abstracted in a common language; second, their abstractions are compared; third, actions are possibly taken to adjust original models according to findings of the comparison. This third step is called concretization, according to the abstract interpretation terminology. This process is illustrated Fig. 6.

It is worth noticing that different abstractors and comparators can be defined. The choice of the abstractors and the comparators to apply depends on the system under study and the level of maturity of the project.

System structure modeling language (S2ML)

Describing the structure of a system is fully part of the modeling process. It helps to design, to share, to maintain and eventually to synchronize models. S2ML aims at providing a structuring paradigm of systems engineering modeling languages. It gathers and unifies concepts from object-orientation [START_REF] Abadi | A Theory of Objects[END_REF] and prototype-orientation [START_REF] Noble | Prototype-Based Programming: Concepts, Languages and Applications[END_REF]. Due to space limitations, we shall only sketch here S2ML ideas. The reader interested in a more detailed presentation should refer to our article [START_REF] Batteux | From models of structures to structures of models[END_REF].

As heterogeneous models can be essentially compared by their structure, S2ML is a perfect candidate as a pivot language for the abstraction.

S2ML relies on only eight constructs:

-Three types of basic objects: ports, connections and blocks.

-Three structural relations: composition, inheritance and aggregation.

-Two mechanisms making possible to reuse modeling elements: the prototype/clone and the class/instance mechanisms.

Ports are basic objects of models, e.g. variables, events, parameters. They have a basic type such as Boolean, integer, real or some enumerated value.

Connections are used to describe relations between ports, e.g. equations, transitions, assertions.

Blocks are containers to compose ports, connections and other blocks. They are prototypes in the sense of object-oriented theory.

Attributes are pairs (name, value) used to associate information to ports, connections and blocks.

The most important and the simplest structural relation is the composition: a container (prototype or class) composes an element if this element "is part of" the container. The inheritance and the aggregation are respectively "is-a" and "uses" types of relation.

Prototypes and classes are containers. As suggested by their names, prototypes have a priori a unique occurrence in the model. It is however possible to clone a prototype. Classes are on-the-shelf, reusable modeling elements. Strictly speaking, they are not part of the models. Rather, they are instantiated into models. Respective advantages and drawbacks of prototypes and classes are discussed in reference [START_REF] Batteux | From models of structures to structures of models[END_REF].

The S2ML+X paradigm consists in designing domain specific modeling languages as the combination of S2ML with a given underlying mathematical framework (the X). We applied already this principle to design AltaRica 3.0, but also to design languages for constraint solving and combinatorial optimization, Boolean reliability models, hierarchical graph representations, hierarchical Markov chains and process algebras (themselves used to describe business processes).

In the S2ML+X paradigm, models are seen as scripts. S2ML provides commands to declare modeling elements. The actual model is obtained by executing these commands. This process works in two steps:

-First, the model is rewritten into a hierarchy of blocks. Each block of the hierarchy may compose ports and connections. This step is called instantiation in the S2ML jargon. -Second, the hierarchy is removed to get a model made of only one block composing ports and connections. This step is called flattening in the S2ML jargon.

In the framework of model synchronization, the rewriting process is stopped after instantiation, as we are interested in keeping hierarchical, i.e. structural, information.

Note that the abstraction of original models into S2ML models can vary significantly from one model to the other one. It depends on the objectives of the synchronization as well as on the modeling formalism used to design the source model.

Model Comparison

A key step of model synchronization consists in comparing the two instantiated S2ML models.

Instantiated S2ML models

S2ML models to be compared are instantiated, i.e. they are made of three types of objects: ports, connections and blocks. Ports and blocks are uniquely identified by their name. Connections are structured terms involving constants, ports and operators. They may also have some attributes. However, they are just considered as (anonymous) sets of ports in the comparison process. Finally, blocks can compose ports, connections and other blocks. All objects may have some attributes but we shall not consider them here. A model is just a block, possibly rooting a hierarchy of blocks.

Formally, a model is thus a quintuple P, C, B, , r where:

-P and B are two disjoint finite sets of symbols called respectively ports and blocks. -C is a multiset of connections, i.e. of subsets of P . We denote by M the set of instantiated S2ML models defined as above.

Matchings

We can now define mappings from models to models. For the sake of model comparisons, we are especially interested in structure preserving mappings.

A mapping α from the model M : P M , C , B M , M , r M to the model N : P N , C N , B N , N , r N is structure preserving if the following conditions hold.

-For any block b ∈ B M and any object o

∈ P M ∪ C M ∪ B M , b M o ⇒ α(b) N α(o). -For any connection c = {p 1 , . . . , p k } ∈ C M , α(c) ⊇ {α(p 1 ), . . . , α(p k )}, more- over for all p ∈ P M , if p ∈ c then α(p) ∈ α(c).
A structure preserving mapping is injective if the following condition holds.

-For any two objects o, o

∈ P M ∪ C M ∪ B M , o = o ⇒ α(o) = α(o ).
Injective structure preserving mappings can be seen as projections. Now, let M , N 1 and N 2 be three models. N 1 and N 2 are matched by M if there exist two injective structure preserving mappings α 1 : M → N 1 and α 2 : M → N 2 . The model M catches the commonalities between N 1 and N 2 . Building such models M is the objective of the comparison process.

Note that instantiated S2ML models together with structure preserving mappings form a category, see e.g. [START_REF] Pierce | Basic Category Theory of Computer Scientists[END_REF] for an introduction. The notion of matching defined here is inspired from the notion of pullback in category theory.

Experiments

SmartSync platform

The SmartSync platform supports model synchronization. It is based on S2ML as a pivot language for the abstraction. It works as illustrated Fig. 7. The objective is to check the consistency of two models of the same system possibly written in two different languages.

This works in three phases. The first phase consists in abstracting original models into S2ML. As of today, this is done manually but this could be automated.

The next phase consists in comparing model abstractions. It involves designers of both models. It aims at establishing a structure preserving matching between the elements of the two abstract models This matching is concretely encoded by means of a two columns table (one per model). In a first step, elements are automatically matched by traversing down the structure of each model and according to identifiers. Elements that could not be matched are highlighted. It is then possible to match elements "by hand". It is also possible to indicate that an element should not be matched because it is specific to its model. The automatic matching process is then launch again. This process is iterated until no progress can be done anymore.

At the end of the second phase, a (possibly empty) list of inconsistencies is obtained. This list is the input for the third phase, which consists in doing some "homework" on each original model so to solve the problems.

The whole process can be itself iterated.

Case study: a power supply system

We apply our model synchronization framework to the case study presented in Section 2. We present a collaborative design of the power supply system. The collaboration is between two teams: system architecture and safety analyses. Each team performs different activities. The first activity is modeling which is performed independently by members of both teams using different modeling languages and tools. System architecture models designed with Capella and safety models written in AltaRica 3.0 are given in Section 2.2.

The second activity is model synchronization, i.e. the verification of consistency between models that ensures that both models are describing the same system. This activity is performed by the members of both teams and involves the SmartSync platform.

First, both models are abstracted, i.e. transformed into S2ML. For AltaRica 3.0 the transformation is straightforward, as the language uses S2ML as its structural paradigm. State and flow variables, events and parameters are abstracted to S2ML ports; transitions and assertions are transformed into connections; different structural constructs like inheritance, cloning, instantiation, etc. are transformed into their equivalents in S2ML.

For Capella functional and physical architecture diagrams the transformation is also quite simple: blocks are transformed into S2ML blocks, ports into S2ML ports and connections between ports are transformed into S2ML connections between corresponding S2ML ports. The allocation table (see Table 1) is transformed as follows: each functional S2ML block aggregates (via the "embeds" clause) the corresponding allocated physical S2ML blocks.

In the next step, the abstractions are compared and a report is generated. This report is analyzed by members of both teams. All the differences are listed in the matching file, which makes it possible to establish the correspondence between the two models. Table 2 shows the matching file of the first iteration. The first column is the element type (port, block, aggregated block or connection).

The second column is the name of the element of the first model, the third column is the name of the corresponding element in the second model. When there is no correspondence, the keyword "forget" is used. It is possible to add a fourth column with comments to justify matching decisions. The following differences are detected:

-Different names of blocks (e.g. the block FunctionalPart in the Capella model corresponds to the block Functional in the AltaRica 3.0); -Elements of the safety model not represented in the system architecture (e.g. observers LossOfBusbarPowerSupply and LossOfIsolation represent the failure conditions and do not have any equivalent in the Capella model).

The produced matching file is used to compare again the abstractions of the system architecture and safety models. In the next iteration of the comparison, new differences are detected. They are analyzed again and the matching file is populated with new matching information summarized in Table 3 As we can see it is quite simple to establish the correspondence between system physical architecture PhysicalPart and the block Physical of the safety model: each Capella block has a corresponding block in the AltaRica 3.0 model, almost each port of the Capella model has a corresponding port in the AltaRica 3.0 model, there are ports in the AltaRica 3.0 model which do not have any correspondence in the Capella model (state variables, events, some flow variables representing failures). Obviously, it is possible in the abstraction step of the safety model not to consider state variables and events as they represent the internal behavior of components and are not expected to have any equivalence in the architecture model.

Concerning the operational part, it is not so obvious to establish the correspondence between the state chart diagram given Fig. 4 on the left and the AltaRica 3.0 model of the Controller sketched in the same figure on the right.

For the functional part, the correspondence is not so easy: the functional decomposition of the architecture model is finer than that of the safety model. However, the established correspondence is given in the following table. Models are then compared again. When no more differences are detected, the structural consistency between system architecture and safety models is verified. The matching file establishes the correspondence between the two models. In case of inconsistencies detection, the initial models need to be adjusted.

Conclusion

In this article, we presented model synchronization -a formal framework for management of heterogeneous models. This framework is based on S2ML (System Structure Modeling Language). We showed that this framework can be used to ensure the consistency of heterogeneous models, designed within different formalisms and different modeling environments.

To support model synchronization, we developed the SmartSync platform, which relies on S2ML as a pivot language. With SmartSync, we studied the electrical power supply system. We checked consistency between system architecture and safety models. The process of making models consistent is iterative and involves representatives of the engineering disciplines at stake. The Smart-Sync platform helps not only to check the consistency between models, but also to detect inconsistencies within models and to support the dialog between stakeholders.

Some questions about the comparison of heterogeneous models remain open. As future works, we plan to improve the SmartSync platform, notably by developing new comparison algorithms and abstraction methods.

Fig. 2 .

 2 Fig. 2. Functional architecture of the power supply system represented with Capella.

Fig. 3 .

 3 Fig. 3. Physical architecture of the power supply system represented with Capella.

Fig. 4 .

 4 Fig. 4. Capella life-cycle diagram (operational architecture) and graphical representation of the AltaRica 3.0 controller of the power supply system.

Fig. 5 .

 5 Fig. 5. Excerpt of the AltaRica code for the power supply system.

Fig. 6 .

 6 Fig. 6. Model synchronization: principle.

  -is a composition relation, i.e. a subset of B × (P ∪ C ∪ B) verifying: -For each object o ∈ P ∪ C ∪ B, there exists at most one block b ∈ B such that b o. b is called the parent of o. -r ∈ B is the unique block with no parent, moreover for all object o ∈ P ∪ C ∪ B, r o, where denotes the transitive closure of .

Fig. 7 .

 7 Fig. 7. Models synchronization process.

  . Other differences are detected: -Different names of ports (e.g. the port Busbar.input in the Capella model corresponds to the port Busbar.vfInflow in the AltaRica 3.0 model); -Elements of system architecture model not represented in the safety model (e.g. the port PhysicalPart.input has no correspondence in the safety model); -Different structural decomposition (e.g. in the Capella model the block Grid belongs to the block PhysicalPart whilst in the AltaRica 3.0 it belongs to the block PrimaryPowerSupply).

Table 1 .

 1 Power supply system: functions allocation table

	Phase		Control elec-	Transform	Control elec-	Generate	Control	Isolate
			trical power	electrical	trical power	backup	power	non-
			delivered by	voltage deliv-	delivered to	electrical	delivered	functioning
			the Grid	ered by the	the Busbar	power	to Busbar	parts
				Grid
	Phase	1	CBU1	TR1	CBD1			CBU2,
	(Line1)							CBD2,
								CB3
	Phase	2	CBU2	TR2	CBD2			CBU1,
	(Line2)							CBD1,
								CB3
	Emergency				DG	CB3	CBU1,
	mode							CBD1,
	(Backup)							CBU2,
								CBD2

Table 2 .

 2 Power supply system architecture and safety models matching, iteration 1.

	Type Model1 (Capella)	Model2 (AltaRica 3.0)
	block SystemArchitecture	PowerSupplySystem
	port forget	LossOfBusbarPowerSupply
	port forget	LossOfIsolation
	block FunctionalPart	Functional
	block OperationalPart.StateMachine Controller
	block PhysicalPart	Physical

Table 3 .

 3 Power supply system architecture and safety models matching, iteration 2.

	Type Model1 (Capella)	Model2 (AltaRica 3.0)
	block SystemArchitecture	PowerSupplySystem
	block FunctionalPart	Functional
	block SupplyElectricalPowerToBusbar SupplyElectricalPowerToBusbar
	block GenerateBackupElectricalPower BackupSupply
	block SupplyElectricalPowerFromGrid SupplyElectricalPowerByGrid
	...	...	...
	block PhysicalPart	Physical
	block Busbar	Busbar
	port input	vfInflow
	block Grid	PrimaryPowerSupply.GR
	port input	forget
	port output	vfOutflow
	block BackupPowerSupply	BackupPowerSupply
	port output	vfOutflow
	port forget	vfFailed
	block DieselGenerator	DG
	block CB	CB
	port input	vfInflow
	port output	vfOutflow
	port forget	fail close
	...	...	...
	block PrimaryPowerSupply	PrimaryPowerSupply
	block Line1	Line1
	port input	vfInflow
	port output	vfOutflow
	port forget	vfFailed
	block CBD	CBOut
	block CBU	CBIn
	...	...	...


Michel Batteux
email: michel.batteux@irt-systemx.fr

Tatiana Prosvirnova
email: tatiana.prosvirnova@onera.fr

Antoine Rauzy
email: antoine.rauzy@ntnu.no

Modeling patterns for the assessment of maintenance policies with AltaRica 3.0

Keywords: Assessment of maintenance policies, AltaRica 3.0, modeling patterns

Modeling patterns for the assessment of maintenance

policies with AltaRica 3.0

Introduction

AltaRica 3.0 is an object-oriented modeling language dedicated to probabilistic risk and safety analyses of complex technical systems [START_REF] Batteux | Altarica 3.0 in 10 modeling patterns[END_REF]. It is of primary importance, in order to make the modeling process efficient (in AltaRica 3.0 as with any other modeling formalism), to reuse as much as possible modeling components. In AltaRica 3.0, reuse is mostly achieved by the design of modeling patterns, i.e. examples of models representing remarkable features of the system under study. Once identified, patterns can be duplicated and adjusted for specific needs. Patterns are actually pervasive in engineering, see e.g. [START_REF] Maier | The art of systems architecting[END_REF][START_REF] Gamma | Design Patterns -Elements of Reusable Object-Oriented Software[END_REF]. Patterns are not only a mean to organize and to document models, but also and more fundamentally a way to reason about systems under study.

In this article we present modeling patterns to represent and to assess maintenance policies with AltaRica 3.0. We focus actually on corrective maintenance policies (components are repaired only when they are failed) taking into account that resources required to perform them (such as the number of repairmen or spare parts) may be limited. We show different modeling approaches, involving advanced features of AltaRica 3.0, such as the synchronization of events or the aggregation of prototypes.

The contribution of this article is thus twofold: first, it provides effective modeling patterns for the assessment of maintenance policies; second, it demonstrates the interest of AltaRica 3.0 advanced modeling constructs.

The remainder of this article is organized as follows. Section 2 introduces a case study that we use throughout the article to illustrate the presentation. Section 3 makes a brief description of the AltaRica 3.0 modeling language. Section 4 presents the maintenance policy modeling, according to three different modeling patterns. Section 5 provides some results on the three corresponding models. Finally, section 6 concludes the article and discusses future works.

Illustrative example

Fig. 1 shows a system made of two subsystems: an equipment under control and a control system.We focus our study on the latter. This system is made of three sensors, a controller and two actuators. The controller is made of three data acquisition units (one per sensor) and a voter, also called a logic solver, which works according to a 2-out-of-3 logic. Each actuator is made of two components. All the components may fail in operation and be repaired. Failure rates (h -1 ) are respectively 10 -5 for sensors, 10 -6 for data acquisition units, 10 -8 for the logic solver and 10 -6 for actuators. A maintenance operation is launched when the system as a whole is failed, i.e. if either two or more sensors are failed or two or more data acquisition modules are failed or the voter is failed or the two actuators are failed. All failed components are repaired during the maintenance operation and can be considered as good as new after. Failed components are repaired one by one. Mean times to repair components are one shift, i.e. 8 hours for actuators, 4 hours for sensors, data acquisition units and the logic solver. To accelerate maintenance operations, two repairers are involved (and can thus repair components in parallel).

The objective of this study is to calculate, for example, the system operational availability during its mission time, taking into account maintenance policies of the components.

3 AltaRica 3.0 modeling 3.1 The AltaRica 3.0 modeling language AltaRica 3.0 is an event-based and object-oriented modeling language dedicated to probabilistic risk and safety analyses of complex technical systems [START_REF] Prosvirnova | The altarica 3.0 project for model-based safety assessment[END_REF]. This language is the combination of two parts: the mathematical framework GTS, for Guarded Transition Systems ([10]- [START_REF] Batteux | Altarica 3.0 assertions: the why and the wherefore[END_REF]) to describe the behavior of the system under study; the structuring paradigm S2ML, for System Structure Modeling Language ( [START_REF] Batteux | From models of structures to structures of models[END_REF]), to organize the model.

The execution of an AltaRica 3.0 model, done by the mathematical framework GTS, is quite similar to other event-based formalisms. It means that when a transition is enabled, it is scheduled and will be potentially fired after its associated delay ([6]- [START_REF] Zimmermann | Stochastic Discrete Event Systems[END_REF]). These delays can be deterministic or stochastic. For stochastic delays, AltaRica 3.0 provides usual probability distributions: exponential, Weibull, uniform or user defined ones.

To structure an AltaRica 3.0 model, S2ML provides the appropriate primitives. S2ML unifies the two main structuring paradigms for modeling languages: object-oriented and prototype-oriented. With S2ML, one can design the model in two ways. The 'top-down' approach: the system is considered at its highest level and modeling patterns are mainly used; it is the realm of prototype-oriented. The "bottom-up' approach: the system is considered at its lowest level (the components) and libraries of components are mainly used: it is the realm of object-oriented.

Two main structural constructs can be used in AltaRica 3.0: a 'block' and a 'class'. A class is an "on-the-shelf", reusable modeling component. It is defined and then can be instanced in a model, or inherited by another class or block. A block is a modeling component with a unique instance, as opposed to a class which can have several instances. The definition of a block is also its (unique) instance. More information can be found in [START_REF] Batteux | From models of structures to structures of models[END_REF].

Modeling with AltaRica 3.0

To design the AltaRica 3.0 model of the system depicted Fig. 1, we start by modeling the main part. We only consider that this main part contains a set of hierarchically ordered components, without thinking about how these components are internally designed.

Main part of the AltaRica 3.0 model The main part is given Fig. 2. It is defined with the block System, which contains two parts: one with the declaration of the different structural elements, the other defining the behavior.

The main part represents the hierarchy of declared components and the links between them (the behavioral part). It is composed of: -A block Control, which is a sub-block of the main block System. This block declares three instances DA1, DA2 and DA3 of the class DataAcquisition.

It declares an internal block LogicSolver, which inherits from the class RComponent. We assume that the class RComponent represents reparable components and contains two parameters lambda and mu that we overload with the values 10 -8 and 4. This inheritance means that the block LogicSolver is a reparable component: it takes the features of the class RComponent. Furthermore, the block LogicSolver declares four flow variables in1, in2, in3 and out. These variables are used in the second part defining the behavior of the LogicSolver: the assertion defines the external behavior according to the internal behavior, i.e. the update of the variable out according to the other variables in1, in2, in3 and a state variable vs (an internal variable) coming from the inherited class RComponent. Finally the block Control specifies the external behavior of its sub-parts in the assertion. -A block Actuator declaring a sub-block Line1. Line1 represents the first line of actuators. It is composed of two instances A1 and A2 of the class Actuator.

These actuators are linked thanks to the assertion. The sub-block Line1 is cloned: a copy of Line1 is made and named Line2. One can notice that these two blocks Line1 and Line2 will independently live their own lives: changes into one block (e.g. the update of a variable, or the firing of a transition) has no impact on the other. -Finally, a Boolean observer TE (Top Event) is declared. This observer observes if the two flow variables out, coming from the two actuators A2 of the two lines, are false.

After the first declarative part, the main block System defines the assertion, which describes how the sub-parts (the sensors, the control and the actuators) are linked together and with the environment. We assume here that the equipment under control cannot fail and the sensors always receive a correct value as input (i.e. the value true because we consider Boolean variables).

Library of components

The main part of the AltaRica 3.0 model contains different components, which are instances of classes. These classes are defined in a dedicated library and are depicted Fig.

Modeling pattern for maintenance

The (part of the) AltaRica 3.0 model, presented previously, does not integrate the behavioral description of a reparable component, as well as the maintenance policy according to the limited number of repairers. We start with the definition of two AltaRica 3.0 elements in Fig. 4

Maintenance policies

According to the European standard NF EN 13306 X 60-319, there are two main kinds of maintenance. The first one is the corrective maintenance, which is carried out after failure detection and is aimed at restoring an asset to a condition in which it can perform its intended function. This kind of maintenance implies an unavailability either of the overall or of a part of the system. The second one is the preventive maintenance, which aims at performing an intervention before the occurrence of a failure. Different kinds of preventive maintenance also exist. Planned maintenance is realized according to a specific bound reached by the system (e.g. date, time of running, distance travelled, etc.). Conditionbased maintenance is realized according to a monitoring of the system. Finally, predictive maintenance uses sensor data to monitor a system, then continuously evaluates it against historical trends to predict failure before it occurs. AltaRica 3.0 is a flexible and versatile tool. Maintenance policies can be taken into account with AltaRica 3.0, of course by realizing some kinds of abstraction. For example, [START_REF] Zhang | A modelling methodology for the assessment of preventive maintenance on a compressor drive system[END_REF] presents a modelling methodology for the assessment of preventive maintenance on a compressor drive system. In the following, we focus on the corrective maintenance policy at the component level. We introduce some condition at system level, to realize maintenance actions, i.e. when a sufficient number of components are failed: at least two sensors are failed, or two data acquisition units or the logic solver unit or one actuator per lines. Furthermore we consider only two repairers to repair failed components.

In The two events maintenanceReq and maintenance are defined with an instantaneous delay, represented by the distribution Dirac(0.0). It means that the transitions, labelled by these instantaneous events, are fired as soon as they are enabled. In the following, we will associate the transition and its label, if there is no ambiguity.

The transition maintenanceReq specifies the maintenance policy in the guard, by using the operator IsNotFailed with the states of the components: at least two sensors are failed. This transition is hidden (the attribute hidden of the labelling event is set to true), meaning it will never be fired alone, it must be synchronized with other transitions. Furthermore, no action is associated to this transition: the instruction skip. By defining the two events, and their associated transitions, maintenanceReq and maintenance, we totally separate the definition of the maintenance policy (in the guard of the transition maintenanceReq) and the action of maintenance (in the transition maintenance).

The transition maintenance synchronizes the transition maintenanceReq and all the transitions maintenance of the components. The symbol ! means that the transition maintenanceReq is mandatory: to fire this transition maintenance, the guard of the transition maintenanceReq must be true. Conversely, the symbol ? means that the transitions maintenance of the components are optional: the transition can be fired if its guard is true, but it is not required. When the transition maintenance of a component is fired, it changes its state from FAILED to WAITING REPAIR: it has to wait the availability of a repairer.

The behavior of a reparable component RComponent is described according the state machine depicted Fig. 6. Nodes represent the different states of the component, which are from the domain SDomain. Edges represent transitions between states. It is a generic behavior which will be adapted according to the considered modeling pattern. In the following we present how to model the availability of a repairer to repair a component, with three different patterns: by propagation of flow variables, by synchronizing events, or by using the virtual aggregation.

Repair by propagation of flow variables

Fig. 7 represents the reparable component for the pattern propagation of flow variables. The component is initialized to the state WORKING: the attribute init of the state variable vs is set to WORKING. The event maintenance is synchronized at system level: its attribute hidden is set to true. Two flow variables are defined. rUsed indicates that a repairer repairs the component. rAvailable takes the value of the availability of a repairer, and is used in the guard of the transition repairStart, i.e. to launch the repair of the component. Fig. 8 shows the additions to the main part of the AltaRica 3.0 model, which are needed for the pattern by propagation of flow variables. The parameter repairer defines the number of repairers (i.e. 2). The flow variable rUsed provides the number of used repairers to repair components. This variable is updated in the assertion by adding all flow variables rUsed of the components. Finally the flow variable rAvailable provides the information that a repairer is available. It is updated according to the value of rUsed and repairer. Then, it is used to update all the variables rAvailable of the components. Fig. 10 represents the additions to the main part of the AltaRica 3.0 model used for the pattern by synchronizing events. A new block Repairer is added. It defines the behavior of the repairer crew according to dedicated events. It is basic: it defines the start and stop of a repair if one of the two repairers is available. Then two new events repairStartC and repairEndC are defined for all components C. These events are used in the transition part to synchronize the own events repairStart and repairEnd of the component C, with the events repairStart and repairEnd of the block Repairer.

Repair by virtual aggregation

For the pattern with the virtual aggregation, the class defining the component is represented Fig. 11. This class is the same as the one defined in Fig. 9. In addition, it virtually aggregates a new element of type T, which is used in the class with the alias t. This virtually aggregated element is used in the class within the two transitions repairStart and repairEnd, by synchronizing them with two events of t. When the class is instantiated (i.e. when an object with this class as type is declared), this aggregation is resolved by indicating a real object (an instance of a class or a block to be used instead of T). This object must be compatible according to the use of it in the declared class.

Fig. 12 represents the additions to the main part of the AltaRica 3.0 model used for the pattern by virtual aggregation. A new block Repairer is defined. It is the same as for the previous pattern by synchronizing events. This block is used when all classes are instantiated, inheriting from the class RComponent, to resolve the virtually aggregated element. The resolution of the virtual aggregation is done by the attribute (virtual T = main.Repairer). It means that the virtual element T, used in the class with the alias t, is equal to the block Repairer. The keyword main, preceding the word Repairer with a dot between them, indicates block System // Declaration of elements ... block Repairer parameter Integer repairer = 2; Integer rAvailable (init = repairer); event repairStart, evRepairEnd (delay = Dirac(0.0), hidden = true); transition repairStart: rAvailable > 0 -> rAvailable := rAvailable -1;

repairEnd: true -> rAvailable := rAvailable + 1; end event repairStartS1 (delay = Dirac(0.0)); event repairEndS1 (delay=exponential(S1.mu)); event repairStartS2 (delay = Dirac(0.0)); event repairEndS2 (delay=exponential(S2.mu));

... // For all components, two new events 'repairStart' and 'repairEnd' // Definition of the behavior

Experiments

Table 1 shows different quantitative features of the models for these three patterns: the model Mf for the pattern propagation of flow variables, the model Me for the pattern synchronizing events, and the model Mv for the pattern virtual aggregation. The first two features are done for the designed models, whereas the others are done for the compiled models. The difference between models Mf and Me concerns the number of flow variables and their updates in the assertion: more important in the model Mf. Nevertheless, this result hides the additional events, per components, defined in Me; which is not indicated in this table but can be found thanks to the number of lines. Furthermore models Me and Mv seem to be equal when compiled. More precisely, they are equal and it is totally normal because the virtual aggregation pattern considers synchronization of events, but from a generic way: by including it directly into the class. The main difference is thus according to the size of the designed models. In the following, especially with the assessment tools, these two models are used equally. Finally it is recommended to use the pattern by virtual aggregation. On the one hand, fewer errors are made at the design phase. On the other hand, it defines fewer flow variables, than the pattern by propagation of flow variables, which has a cost when the model is evaluated by the assessment tools: these variables are updated in the assertion and there is a computational cost for that at runtime. Some experiments are also realized in order to evaluate the Boolean observer TE. This observer indicates when the values of the two flow variables out, of the two actuators A2 of the two lines, are false. It means that the system is failed. We used the AltaRica 3.0 stochastic simulator of the OpenAltaRica platform ( [START_REF] Aupetit | Improving performance of the AltaRica 3.0 stochastic simulator[END_REF]) to perform the experiments.

Table 2 shows the means of fired transitions for the following number of generated histories: 10 5 , 10 6 and 10 7 , for a mission time equal to 20 years (175200 units of time). The execution time, to generate these histories, has not been taken into account. On the one hand, it is quick: 1-2 minutes for 10 7 histories on a personal laptop. On the other hand, our interest does not focus on performance analysis of the tool. Elements can be found in [START_REF] Aupetit | Vers la définition d'un kit d'évaluation pour les simulateurs stochastiques[END_REF] or [START_REF] Aupetit | Improving performance of the AltaRica 3.0 stochastic simulator[END_REF]. Table 3 shows statistics provided by the stochastic simulator, on the observer TE, for 10 7 generated histories. The considered mission time was 20 years and we also considered different time instants: 5, 10 and 15 years. We focused on the two following statistics. 'had-value' (denoted h-v) is equal to 1 if the observer took the value true for a non-null period at least once from time 0 to time d (with d equals to 5, 10, 15 or 20 years), and 0 otherwise. 'number-of-occurrences' (denoted n-o) is equal to the number of dates the observer started taking the value true over the time period [0, d] (with d equals to 5, 10, 15 or 20 years). The obtained results are quite similar.

Conclusion

In this article, we presented three different modeling patterns with the AltaRica 3.0 modeling language to represent a corrective maintenance policy on a set of components, with a limited number of repairers. A main modeling part of the system has first been proposed. This part is common to the three modeling patterns and was realized with a 'top-down' approach. Behaviors of the components were not directly defined. Furthermore we included the maintenance policy into this main part.

Regarding the limited number of repairers, meaning their assignment to failed components according to their availability, the three different patterns were presented. The first one uses the propagation of flow variables. This pattern is not difficult but error prone. In addition it could be less efficient during execution. In fact it duplicates the number of flow variables, thus the number of elements to update in the assertion. The second and third patterns use the synchronization of events. The second one defines these synchronizations by hand, for all the components. The third one uses the virtual aggregation to integrate these synchronizations into a generic class. This third pattern is more easy to design models, and thus less error prone.

These modeling patterns for maintenance policies with AltaRica 3.0 open the way to new opportunities. On the one hand, modeling patterns allow engineers to model simply and efficiently classical safety features: e.g. periodically tested component, (warm) redundancies, shared resources, common cause failures, etc. Some of these patterns are defined in libraries. For the others, it is possible, in an easy way, to design tools helping engineers to create models with such patterns. On the other hand, it is possible to extend the use of AltaRica 3.0 modeling language to study other performance indicators than those for safety, e.g. scheduling maintenance policies.

Fig. 1 .

 1 Fig. 1. An equipment under control and its control part.

Fig. 4 .

 4 Fig. 4. AltaRica 3.0 code for the domain and operator.

Fig. 5 ,Fig. 5 .

 55 Fig. 5. Main part of the AltaRica 3.0 model with the maintenance policy.

Fig. 6 .

 6 Fig. 6. State machine of a reparable component.

Fig. 9 .

 9 Fig. 9. AltaRica 3.0 code of the reparable component for the pattern by synchronizing events.

Fig. 10 .Fig. 11 .

 1011 Fig. 10. Main part of the AltaRica 3.0 model with the pattern by synchronizing events. class RComponent embeds virtual T as t; SDomain vs (init = WORKING); parameter Real lambda = 1.0e-5; parameter Real mu = 2.0; event failure (delay = exponential(lambda)); event maintenance (delay = Dirac(0.0), hidden = true); event repairStart (delay = Dirac(0.0)); event repairEnd (delay = Dirac(mu)); transition failure: vs == WORKING -> vs := FAILED; maintenance: vs == FAILED -> vs := WAITING_REPAIR; repairStart: !t.repairStart & vs == WAITING_REPAIR -> vs := REPAIR; repairEnd: !t.repairEnd & vs == REPAIR -> vs := WORKING;

Fig. 12 .

 12 Fig. 12. Main part of the AltaRica 3.0 model with the pattern by virtual aggregation.

-

  Three instances S1, S2 and S3, of the class Sensor. We only assume that this class Sensor contains two flow variables in and out (we can see them in the second part defining the behavior).

	block System
	// Declaration of elements
	Sensor S1, S2, S3;
	block Control
	DataAcquisition DA1, DA2, DA3;
	block LogicSolver
	extends RComponent (lambda = 1.0e-8, mu = 4);
	Boolean in1, in2, in3, out (reset = false);
	assertion
	out := if vs == WORKING
	then (in1 and in2) or (in1 and in3) or (in2 and in3)
	else false;
	end
	assertion
	LogicSolver.in1 := DA1.out;
	LogicSolver.in2 := DA2.out;
	LogicSolver.in3 := DA3.out;
	end
	block Actuators
	block Line1
	Actuator A1, A2;
	assertion
	A2.in := A1.out;
	end
	clones Line1 as Line2;
	end
	observer Boolean TE = (Actuators.Line1.A2.out == false) and
	(Actuators.Line2.A2.out == false);
	// Definition of the behavior
	assertion
	S1.in := true; S2.in := true; S3.in := true;
	Control.DA1.in := S1.out;
	Control.DA2.in := S2.out;
	Control.DA3.in := S3.out;
	Actuators.Line1.A1.

in := Control.LogicSolver.out; Actuators.Line2.A1.in := Control.LogicSolver.out; end Fig. 2. AltaRica 3.0 code for the main part.

  : a domain and an operator. The domain SDomain defines four values, WORKING, FAILED, WAITING REPAIR and REPAIR, which will be used after to define types of elements (e.g. variables, parameters or observers). The operator IsNotFailed returns an integer value (1 or 0) according to the value of the argument aState, of type SDomain.

	class RComponentIO
	extends RComponent;
	Boolean in, out (reset= false);
	assertion
	out := vs == WORKING and in;
	end
	class Sensor
	extends RComponentIO (lambda = 1.0e-5, mu = 4);
	end
	class DataAcquisition
	extends RComponentIO (lambda = 1.0e-6, mu = 4);
	end
	class Actuator
	extends RComponentIO (lambda = 1.0e-6, mu = 8);
	end
	Fig. 3. AltaRica 3.0 library of components.

domain SDomain {WORKING, FAILED, WAITING_REPAIR, REPAIR} operator Integer IsNotFailed(SDomain aState) if (aState != FAILED) then 1 else 0 end

  that the object Repairer is declared at the main hierarchical level of the model, i.e. the block System.

	block System
	// Declaration of elements
	block Repairer
	parameter Integer repairer = 2;
	Integer available (init = repairer);
	event repairStart (delay = Dirac(0.0), hidden=true);
	event repairEnd (delay = Dirac(0.0), hidden=true);
	transition
	repairStart: available > 0 -> available := available -1;
	repairEnd: true -> available := available + 1;
	end
	Sensor S1, S2, S3 (virtual T = main.Repairer);
	block Control
	DataAcquisition DA1, DA2, DA3 (virtual T = main.Repairer);
	block LogicSolver
	extends RComponent (lambda = 1.0e-8, mu = 4.0,
	virtual T = main.Repairer);
	...
	end
	...
	end
	block Actuator
	block Line1
	Actuator A1, A2 (virtual T = main.Repairer);
	...
	end
	...

Table 1 .

 1 Quantitative features for the three patterns.

	Features	Mf Me Mv
	Number of lines, at design	143 177 130
	Number of lines of the main block (System), at design 84 124 66
	Number of state variables	11 12 12
	Number of flow variables	48 24 24
	Number of events	34 34 34
	Number of lines of the assertion	48 24 24

Table 2 .

 2 Means of fired transitions.

	Number of histories 10 5	10 6	10 7
	Mv	22.9015 22.9089 22.9002
	Mf	22.9133 22.8936 22.8997

Table 3 .

 3 Statistics on the observer. Mv 5 years h-v 0.315882 0.315438 n-o 0.343274 0.343362 10 years h-v 0.646718 0.646189 n-o 0.848165 0.849419 15 years h-v 0.830037 0.829901 n-o 1.35688 1.3594 20 years h-v 0.919748 0.920068 n-o 1.86367 1.86752

	Mf

Repair by synchronizing events

Fig. 9 represents the reparable component used for the pattern by synchronizing events. The three events maintenance, repairStart and repairEnd have their attributes hidden set to true in order to synchronize them at the system level.


METEORITES The tumultuous childhood of the Solar System

Yves Marrocchi and Laurette Piani

The peculiar carbon isotopic compositions of carbonates in the Tagish Lake meteorite suggest that D-type asteroids accreted in the outer part of the protoplanetary disk-beyond 10 AUbefore being dispersed sunwards to the main asteroid belt.

Asteroids are airless bodies of varying sizes revolving around the Sun and are considered to be the remnants of planetary formation processes. Although asteroids have been visited by several past and current space missions, asteroid formation condition, timing and location remain poorly understood. Writing in Nature Astronomy, W. Fujiya and colleagues 1 use the carbon isotope compositions of a unique meteorite -the Tagish Lake chondrite-to get hints on the formation location of D-type asteroids, kindred to this meteorite.

From the discovery of the first asteroids in the early nineteenth century, the asteroid belt, located between Mars and Jupiter (Fig. 1), was long considered to be a 'living relic' of planetary formation, with asteroids remaining at the heliocentric distance at which they formed. Opinions started to change some 40 years ago with the discovery of compositional variations as a function of distance from the Sun 2 . Since then, the census of the orbital and compositional characteristics of tens of thousands of asteroids 3 revealed the structure of the asteroid belt to be even more complex, with asteroids showing a large range of eccentricities and inclinations, as well as the radial mixing of different asteroid types across the asteroid belt.

We know now that the peculiar properties of the main asteroid belt are the direct consequences of the tumultuous childhood and chaotic history of the Solar System. Numerical simulations show that the migration of giant planets over distances of several astronomical units (AU) shaped the Solar System during its first billion years of evolution 4 . The asteroid belt thus resulted from large-scale gravitational perturbations induced by planetary migration events 4.56 and 4.1 Ga.

Among the wide diversity of asteroids in the main belt, D-type asteroids are rare, potentially organic-rich rocky bodies with compositions that have likely remained unchanged since their formation; they are located in the outer asteroid belt and constitute the majority of the Jupiter Trojans. Numerical simulations suggest that D-type asteroids formed beyond ~15 AU from the Sun 5 and potentially as far as the Kuiper Belt (30-50 AU) 6 , but their origin, dynamical evolution, and mineralogical characteristics remain largely unknown. No confirmed D-type meteoritic sample is known, with the possible exception of the Tagish Lake chondrite that was recovered after its fall in 2000. This carbon-rich meteorite is characterized by unique features, including large D and 15 N enrichments and high concentrations of presolar grains and carbonate minerals 7,8 .

Fujiya et al. 1 take advantage of the high abundance of carbonates in the Tagish Lake chondrite to estimate where D-type asteroids accreted within the protoplanetary disk. The idea is quite simple. The precipitation of chondritic carbonates required a carbon source whose origin can be tracked based on the carbon isotopic compositions of the carbonates. Within chondritic parent bodies, three C sources are generally invoked 9 : (i) inorganic cometary carbonaceous ices (CO, CO 2 ), (ii) presolar grains, and (iii) soluble organic matter. Until now, soluble organic matter was considered as the best candidate to explain the range of carbon isotopic compositions observed in carbonates of hydrated CM chondrites 9 . However, Fujiya and co-authors 1 show that the amount of soluble organic matter in Tagish Lake is too low to have produced its high abundance of carbonates. More critically, the unusual 13 C-rich carbon isotopic composition of Tagish Lake carbonates reported by Fujiya et al. 1 cannot be explained without invoking the accretion of large amounts of CO 2 cometary ices.

Based on these results, Fujiya and co-authors 1 calculate that the CO 2 /H 2 O ratio of ice accreted by the Tagish Lake parent body is similar to that estimated for cometary ice. The carbon budget of the Tagish Lake parent body was thus dominated by cometary ice, which is at odds with the carbon sources considered for other carbonaceous chondrites. Fujiya et al. 1 conclude that the Tagish Lake parent body formed beyond 10 AU, in regions of the protoplanetary disk that were cold enough for CO 2 to condense (Fig. 1). This supports an outer Solar System origin for D-type asteroids and suggests that the violent dynamical evolution of the giant planet orbits led to large-scale perturbations in the Solar System upon the transport of primitive trans-Neptunian objects to the asteroid belt.

Despite its peculiar features, the Tagish Lake chondrite is surprisingly not so structurally different from other carbonaceous chondrites that are thought to have formed closer to the Sun. All the ingredients of the chondrite recipe are present: calcium-aluminiumrich inclusions (CAIs), chondrules, and fine-grained matrix. If the Tagish Lake parent body indeed accreted in the outer Solar System as claimed by Fujiya and co-authors 1 , it would have deep implications for the dynamics of the protoplanetary disk. It would mean that large-scale outward mixing must have occurred during the disk's evolution, as previously inferred from the presence of CAI-and chondrule-like objects in the Stardust cometary samples 11 , because it is unlikely that reduced high-temperature assemblages (CAIs and chondrules) formed in the cold, water-rich outer zones of the protoplanetary disk. Furthermore, the fact that Tagish Lake chondrules have oxygen isotopic compositions similar to those of CM carbonaceous chondrites, which are thought to be representative of the most common C-type asteroids 11 , could be taken as an argument that chondrules formed from a homogeneous oxygen isotopic reservoir in the inner protoplanetary disk before being dispersed throughout the disk. Fujiya et al. 1 do not discuss these issues in detail nor do they address the possible similarity of the oxygen isotopic compositions of CI, CM, and Tagish Lake alteration fluids 10,[13][14][15] . Indeed, no significant heavy isotope enrichment seems to be present in Tagish Lake water and carbonates [14][15] , although such enrichments are expected for objects that formed in the outer Solar System where interstellar water ice grains would have dominated the water budget 16 . Interpreted in the framework of the protoplanetary disk's dynamical evolution, this could imply that the oxygen isotopic composition of water is also homogeneous at a large-scale.

The results reported by Fujiya et al. 1 therefore raise many questions about the origin of isotopic variations, such as the role of photochemical processes in producing 13 Cenrichments 17 , and the general structure of the protoplanetary disk. Future comparison of the present data with samples of hydrated B-and C-type asteroids expected to be returned to Earth by the OSIRIS-REx and Hayabusa 2 missions will thus be fundamental to further quantifying large-scale pertubations in the early Solar Sytem.

Yves Marrocchi and Laurette Piani entre de echerches trographi ues et ochimi ues , , , niversit de orraine, rue otre ame des auvres, andoeuvre-l s-Nancy, France. e-mail: Yves Marrocchi (yvesm@crpg.cnrs-nancy.fr) and Laurette Piani (piani@crpg.cnrsnancy.fr)

Fig. 1 :

 1 Fig. 1: Schematic representation of the Solar System showing the location of the different planets and the asteroid belt. The data reported by Fujiya et al. suggest that D-type asteroids were formed in the outer part of the Solar System before being implanted in the main asteroid belt. CC = carbonaceous chondrites, CAIs = calcium-aluminum-rich inclusions