Franck Petitdemange
email: franck.petitdemange@irisa.fr

Isabelle Borne
email: isabelle.borne@irisa.fr

Jérémy Buisson
email: jeremy.buisson@irisa.fr

Codis56 Codis35

Modeling System of Systems configurations

System of Systems (SoS) engineering is a challenging research direction because an SoS has distinctive characteristics in comparison to distributed systems. UPMD and SysML provide adequate frameworks and notations which help in the process of modeling and architecting SoS. Projects such as DANSE and COMPASS have selected the most relevant views among the numerous views of UPDM. By nature, an SoS evolves after its initial deployment. To deal with evolutions, the architect needs to model configurations, what was not considered in previous state of the art. Modeling configuration is indeed key before we can model the evolution itself. In this paper, our contribution is a new modeling process, based on UPDM and SysML, that helps the architect in designing the configuration of an SoS. The proposed process is illustrated with the case study of the French emergency service.

I. INTRODUCTION

The growing complexity of distributed systems leads to consider new engineering approaches. Among them, the system of systems (SoS) approach [START_REF] Gorod | Case studies in system of systems, enterprise systems, and complex systems engineering, ser. Complex and enterprise systems engineering[END_REF] addresses the case in which the constituents retain their own operational and managerial independence. The architecture of a system of systems focuses on the communications between its constituents, from which the overall behavior emerges. Model-based techniques are suitable to assist the architect with development, maintenance and adaptation steps. Models of constituents, connectors and environment are helpful to analyze trade-offs, to determine the contracts binding the SoS to the constituents, and to deal with complexity by documenting the structural, behavioral and communication aspects of the system of systems.

In comparison to classic distributed systems, an SoS rises specific issues that have to be dealt with, including heterogeneity that follows from managerial independence of the constituents, difficulty to bound a system that is intrinsically open, and dynamicity. Previous state of the art has highlighted that UPDM provides an adequate framework and that SysML is a set of suitable notations when an architect wants to model an SoS, as evidenced by projects DANSE [START_REF] Lochow | Concept Alignment Description[END_REF] and COMPASS [START_REF] Forcolin | Accident Response Use Case Engineering Analysis Report Using Current Methods & Tools[END_REF]. While UPDM is a large framework with numerous views that address many aspects in the lifecycle of a project, only valuable views are selected in the UPDM framework in order to focus the work of the architect on specific concerns.

In this paper, we focus more specifically on the following characteristic: an SoS usually involves critical systems or economic systems (e.g. emergency services, transportation services) that cannot support the disruption or degradation of some services. The SoS architecture continuously evolves and the architect needs to evaluate the current architecture to redeploy it.

Accurate and precise models are therefore important artifacts in such evolutionary development of SoSs. For this reason, in this paper, we focus more specifically on the modeling of configurations.

Our main contribution is a process that helps an SoS architect produce models for the configurations of the SoS under consideration. To do this, our contribution relies on the analysis of UPDM, DANSE and COMPASS. Then we contribute an adapted selection the UPDM views that are targeted at defining configurations for an SoS. We propose the SysML notations that appear to be the most relevant ones for these views.

The paper is organized as follows. The next section describes the real case study that we use to illustrate the modeling process. Then, we investigate in Section III the related works in order to identify the main modeling issues and existing approaches to get the architectural charateristics needed to model SoS architecture configurations. Section IV describes the modeling process applied to the case study. Section V discusses and motivates the choices we have made in the proposed modeling process. Finally we draw conclusions and perpsectives.

II. MOTIVATING USE CASE

We present in this section a typical use case that will exemplify system of systems modeling. Our emergency rescue SoS is based on the French emergency service whose mission is to protect property and people. It is the setting up of an exceptional rescue organization in the case of natural disasters.

Here it is about a flood of a whole area. The SoS is formed by the interaction of several systems which cooperate to fulfill an objective that they cannot provide individually.

The Figure 1 shows the main participants. There are several rescue teams which are the constituent systems collaboraring in the SoS. We consider:

• The departmental operation center of fire and help (CODIS 1 ) which oversees and coordinates the whole operational activity of a departmental fire and rescue service (SDIS 2 ). Here two operation centers are involved • The SAMU 3 is the center for emergency medical regulation and regulates urgent care resources (ambulances for example). • Finally, the Civil Security, involved in major crisis situations, can provide air assets. Each type of system is deployed on each French department with its own funding and hierarchical structure, and it provides its own communication infrastructure. The constituent systems share the same telecommunication standard. Consequently, systems can communicate with each other and/or share their infrastructure.

We focus on three possible SoS configurations. The first one considers two SDIS having an operational collaboration, that is, they communicate directly, only with respect to field actions performed in order to fulfill the mission. Such a collaboration is set up, for instance, when one SDIS faces understaffing, and it therefore requests missing resources from a neighbour SDIS for a small-sized mission. In our scenario, this configuration is used when inhabitants call for emergency services in response to what is thought to be a localized flood.

In the second configuration, two SDIS have a tactical and a strategic collaboration, that is, a hierarchical command chain is set up. In addition to the operational collaboration, the tactical collaboration allows commanders to communicate with their subordinates, in order to give them instructions and collect reports with regard to field actions. The strategic collaboration ensures that consistent directions are adopted by the collaborating SDIS in order to address higher-level objectives defined by the mission. This second configuration is used when the crisis is bigger, hence calling for more resources than provided in the first configuration, and when these resources require tight coordination. In our scenario, the SoS evolves to this second configuration when the emergency services discover that the flood is more critical than they initially thought. 3 Service d'Aide Médicale Urgente Finally, in the third configuration, a SDIS collaborates with the Emergency Medical Assistance Service (SAMU) and the civil security. This configuration occurs when the fire and rescue services need help from other services in order to deal with the crisis. In our scenario, SAMU is involved in order to regulate evacuation of wounded persons to closest hospitals, and civil security provides helicopter resources when the flood makes roads unusable.

III. SOS MODELING ISSUES

This section describes current practices in the context of SoS modeling. We also emphasize issues that are specific to the context of SoS.

On the one hand, standard modeling languages like UML and SysML provide acknowledged notations, and XMI allows tool interoperability. SysML relies on the core concept of block, which is the unit of which a system is composed. The block concept extends UML's class with the notion of composite structure. Within a system, blocks interact through ports that can be connected to one another. Like UML, SysML defines several diagrams, for both behavioral and structural aspects of the system. While not being exhaustive, use case diagrams describe interactions between users and the system; sequence, activity and state machine diagrams describe the course of action within blocks; block definition (bdd), internal block (ibd) and parametric diagrams describe blocks and their interactions.

On the other hand, the Unified Profile for DoDAF and MODAF (UPDM [4]) is an architectural framework that prescribes a comprehensive set of more than 40 views, which help in the process of modeling and architecting SoS. Like its name tells, it unifies the preexistent DoDAF and MODAF architecture frameworks, from the USA Department of Defense and UK Ministry of Defence respectively. The framework defines a collection of modeling intentions, by describing the objective of each specific view. The main groups of UPDM views are:

• Acquisition/Project Views (AcV/PV) describe organizational aspects of projects, including their timeline and milestones.

• The All-Views (AV) gather global information and metadata about elements of the architecture. • Operational Views (OV) are a collection of views that describe the activities involved in the SoS, as well as the resources (human or machinery) that perform these activities.

• Service-Orientated Views (SOV) describe the services, in terms of their interfaces, as well as the function services are expected to perform in order implement activities described in Operational Views. • Strategic/Capability Views (StV/CV) are a group of crossproject long-term views that describe and organize capabilities of an organization, in anticipation of projects. • System/Services Views (SV/SvcV) are a collection of views that describe how operational capabilities described in Operational Views and user requirements can be real-ized in terms of equipment (or human) capability, that is, the specification of constituents involved in the system. • Technical/Standards Views (TV/StdV) describe technologies, rules and standards underpinning the implementation of the system, hence providing a tool to anticipate technological progress or disruption that may affect the system. While UML and SysML are only languages and do not provide any associated process, UPDM does not prescribe any modeling language for none of the views. The two technologies complement each other.

Instead of considering UPDM as a whole, and in order to avoid the numerous views of UPDM, previous work in the DANSE project [START_REF] Lochow | Concept Alignment Description[END_REF] suggest to focus on selected views. Operational View OV-1 is intended to describe the mission or scenario of the SoS. Then, Operational View OV-5 aims at describing the tasks involved in achieving the mission. Next, Operational View OV-2 describes interactions and exchange of information between operational capabilities of the system. System View SV-5 traces what functions can implement the operational capabilities of OV-5. System View SV-1 addresses the composition and interaction of resources. Last, System View SV-10A is used in order to express functional and nonfunctional constraints.

The COMPASS project [START_REF] Forcolin | Accident Response Use Case Engineering Analysis Report Using Current Methods & Tools[END_REF] also selects a subset of views, but, unlike DANSE, the COMPASS project does not follow UPDM. Though, some similarities can be observed, beginning with the distinction between Operational View and System View, named logical and physical, respectively. Most of the views match the DANSE project, since both projects follow the RUP process. But we observe the following differences. Instead of a single view OV-1 to describe the mission of the SoS, the COMPASS project uses two views: the first one gives an outline of the general organization; the other one focuses on the use cases expected from the SoS. Similarly, SV-1 is split into one view specifically targeted at the relationship between contituents and missions, and a separate view that describes collaborations within the SoS. Last, COMPASS has no counterpart for SV-10A.

Both DANSE and COMPASS reduce the architecture framework according to targeted objectives. The differences between the two reduced frameworks can be explained by different objectives: on the one side, DANSE is more targeted at SoS validation and adaptation to the environment; on the other side, COMPASS focuses on SoS evolution.

In the remainder of this section, we focus on specific modeling issues, and how these issues are addressed in the state of the art.

A. Heterogeneity

Since an SoS establishes a collaboration between constituent systems coming from several independent organizations, several stakeholders are involved in the production of the corresponding models. For instance, each fire department has it own system organization which is different of SAMU organization. But when it comes to the SoS, the models produced by all these stakeholders must be combined. Heterogeneity of languages and practices is an obstacle.

Altogether, UML/SysML/XMI and UPDM provide frameworks that have good chance to be adopted by independent organizations. In practice, both DANSE and COMPASS use this combination for most of the diagrams they rely on.

In addition to modeling language and framework, the participation of several independent stakeholders rises the issue of concept (mis)alignment. To address this issue, [START_REF] Nguyen | Models composition in FORM-L: Study of complex socio-cyber-physical systems and large scale systems of systems[END_REF], [START_REF] Neureiter | A standards-based approach for domain specific modelling of smart grid system architectures[END_REF], [START_REF] Mazeika | MBSE driven approach for defining problem domain[END_REF], [START_REF] Morkevicius | Using a systems of systems modeling approach for developing Industrial Internet of Things applications[END_REF] propose to use traceability information in order to describe the relationship between related or similar concepts in models produced by different stakeholders. UPDM defines traceability views in order to help verifying that all the abstraction layers, e.g., Operational View and System View are consistent with one another.

B. SoS boundary

When an SoS is under definition, its border is generally blurred in the sense that identifying the constituents of the SoS is not trivial.

T-AREA [START_REF]Trans-Atlantic Research and Education Agenda in Systems of Systems[END_REF] illustrates this issue with the example of Apple's supply chain. At that time, all of the Apple's direct suppliers for a specific category of batteries used to share the same second-level supplier, for one of the critical materials. Despite apparent redundancy when only the constituents directly contributing to the mission of the SoS were considered, that shared supplier was in practice a single point of failure. This was revealed by an earthquake which caused a disruption of the shared supplier, according to [START_REF]Trans-Atlantic Research and Education Agenda in Systems of Systems[END_REF]. In this case, if the second-level supplier is not part of model, reliability analysis of the SoS fails to report the weakness.

At the same time, in our case study of Section II, it is obvious that modeling all the emergency services from all the French departments (one hundred departments) is irrelevant. Even if they all possibly provide resources, only few of them have effective impact on the SoS. Only the services in the departments where the flood is located, plus possibly the neighbour departments, are significant.

The challenge is to decide which constituents should be included in the models, while omitting those constituents that do not provide valuable information.

In the DANSE project, described above, the boundary of the SoS is defined by the production of UPDM's OV-1 expressed as a schematic picture. COMPASS uses in addition a use case diagram.

C. Dynamicity

Due to its nature, an SoS can include hundreds of constituents which are versatile. Consequently, dynamic models are not as usable as in simpler systems.

To face this issue, [START_REF] Bryans | Maintaining Emergence in Systems of Systems Integration: a Contractual Approach using SysML[END_REF] suggests to restrict the use of state machine diagrams to the specification of contracts. [START_REF] Oquendo | Architecturally describing the emergent behavior of software-intensive system-of-systems with SosADL[END_REF], [START_REF] Woodcock | Features of CML: A formal modelling language for Systems of Systems[END_REF] propose to focus models on static regularity of the considered SoS. Instead of giving all the details of instances, the SoS is described by a set of constraints over how constituents can be connected to one another. The same approach is used in the

D. Dynamic architecture

In our case study, we observe that an architecture is first defined as a response to the initial call to the emergency services. Then, while the SoS provides initial services, the environment evolves or the environment is discovered to be different from the initial thought. The SoS needs to evolve accordingly. New constraints are required during the SoS execution because new types of constituents are involved. Consequently, architecture models are required during SoS operation too. According to, e.g., [START_REF] Allen | Specifying and Analyzing Dynamic Software Architectures[END_REF], it is a good practice to ensure clean separation of concerns between reconfiguration logic and the rest of the architecture, while at the same time reusing the same paradigms and description languages. To the best of our knowledge, none of the previous SoS modeling approaches take this issue into account.

E. Positioning of our work

In our work detailed in Section IV, in comparison to related work, we specifically consider the configuration of the SoS and its modeling, thus leading to a different combination of choices. Indeed one objective of our work is in the context of dynamic reconfiguration. We also put the emphasis on the process in addition to the views and modeling language. UPDM serves as a basis for our work, because it appears to be well-adapted to the modeling of complex systems. With respect to the identification of the boundary of the SoS, we restrict to (semi-formal) structured notations: use case diagrams in the context of OV-1. With regard to dynamicity, we improve over previous approaches by introducing the use of architectural styles, and more specifically the architectural primitives [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF].

IV. SYSTEM OF SYSTEMS MODELING PROCESS

This section is dedicated to the modeling process from which the objective is to obtain the various configuration Fig. 3. Use case diag. of operational collaboration between SDIS 56 and 35 models of our SoS. As we explained in the previous section, we choose UPDM which is a good candidate to address the modeling of complex systems. Our modeling process is composed of four steps, which are outlined in Figure 2. The process we propose is a top-down process, where the architect first bounds the system under consideration by means of functional analysis. Then the architect produces activity diagrams for each use case to detail how the tasks performed by each constituent can be combined to achieve SoS-level functions. Next the architect identifies and composes the constituents by means of block definition diagrams. Last the architect obtains the configuration as an internal block diagram that describes interactions between the constituents that have been engaged in the system of systems to implement the activies previously described.

As we do not have room to detail the three configurations outlined in Section II, we will proceed with the process on the first case, which is the initial configuration.

The first step of the process aims at drawing out the boundaries of the SoS under consideration. Similarly to UPDM's Operational View OV-1, our goal is to enumerate the functionalities and missions expected from the SoS as well as to elicit the actors that are related to these missions. A use case diagram allows to describe the general organization with coarse-level actors. The second step should detail the activities associated with each use case. The operational view OV-5 in UPDM translates into activity diagrams. For every use case previously identified, an activity diagram describes the normal course of operations. Figure 4 shows an activity diagram for the operational coordination of the workforce. It illustrates the communication protocol between the CODIS operator of SDIS 56 and the SDIS 35 team leader, and the sending of the instructions by the operator. The communication channel (here voice radio) is shared. In consequence, the French procedure requires that the CODIS operator first waits for the end of ongoing calls. We see that phases of identification, confirmation of listening and reception are required

The third step concentrates on the composition of the constituents. The system view SV-1 in UPDM suggests using block definition diagrams (bdd) to model the constituent organization. Figure 5 shows this diagram for our example. The actors are part of the constituents used by the SoS. To differentiate between constituent classes, stereotypes are mentioned such as <<human>>, <<software>> or <<material>> with their intuitive interpretation. We can see that the SoS aggregates CODIS operators, operational communication channels and team leaders. Furthermore, at the level of the material constituents we see that the CODIS has a fixed communication post, every operational channel has a relay and every team leader is in charge of a VTU.

Step four focuses on the interaction of constituents in the SoS. The internal block diagram (ibd) in figure 6 shows the operational coordination between SDIS 56 and SDIS 35. In our case study, CODIS operators communicate with team leaders. As seen in the activity diagram Figure 4, the collaboration protocol between a CODIS operator and a team leader is a disciplined commander/subordinate relationship. In the internal block diagram (ibd), we decided to reflect this fact by introducing a tactical layer (containing CODIS operator) and a distinct operational layer (containing team leader). In order to document such design decisions, we propose to rely on architectural primitives [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF]. In Figure 6, the <<Group>> stereotype annotates packages that denote layers in the architecture. Package inclusion is used to connect constituents with the package that models the layer to which constituents belong. The internal block diagram hence states that CODIS operator belongs to the CODIS56 layer (tactic layer) and team leader belongs to the routine intervention layer (operational layer). According to its definition in [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF], <<Group>> prevents direct communication between constituents from distinct layers, which is indeed the constraint we want to express, such that CODIS operator and team leader are forced to use the operational channel in order to communicate. The <<ShieldPort>> stereotype, from [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF] annotates the only port that is allowed for cross-layer communications. OCL constraints enforce this restriction: these constraints ensure that any binding either connects ports of constituents that belong to the same <<Group>> package, or connects a port to a <<ShieldPort>> port. The <<IShield>> stereotype is used to denote shield interfaces, involved in cross-layer interactions.

Finally we can consider the evolutions of the studied configuration. One evolution corresponds to the transition between the first and the second configuration described in section II. The number of constituents deployed for local intervention (FloodingIntervention layer) has increased considerably, so CODIS can no longer fully manage the intervention. A group leader has to be deployed to supervise a local intervention. CODIS 35 decides to deploy a group leader to assume the role of CODIS operator in the previous configuration. Following the same modeling approach, Figure 7 shows the resulting configuration that corresponds to a strategic collaboration beween SDIS 56 and SDIS 35. The <<Group>> primitives are reused to model the partition of constituents and to define communication points. The <<Layer>> primitives are introduced to capture constraints, with an attribute levelNumber that states the position of the layer in the hierarchical command chain. An OCL constraint ensures that cross-layer interactions through <<ShieldPort>> ports do not skip intermediate Fig. 7. ibd of strategic collaboration between SDIS 56 and 35 levels in the command hierarchy. For example constituents from FloodingIntervention layer cannot directly communicate with constituents of the CODIS56 layer. Other configurations exist for this case study which we cannot expose here.

Without going into all the details, we have described the main steps of our modeling process which allows us to obtain a modeling of an SOS configuration. All the diagrams obtained form the basis of the SoS architecture. Our ultimate goal is to be able to reconfigure the architecture of a SoS and facilitate the transition from one configuration to another.

V. DISCUSSION

The work described in this paper lies in the context of a larger work towards assisting the architect in the design of reconfigurations when the SoS evolves. Even if this paper does not address the specific issues of evolution and reconfiguration, we keep this intention in mind as one of the goals of the model that results from the process of Section IV. More specifically, reconfiguring the SoS after deployment, when the SoS evolves, requires to ensure runtime properties such as timeliness, safety, continuity of operation. To correctly assess whether these properties are met, modeled configurations must capture exact and precise dependencies required by each constituent to provide its services to the SoS.

In this regard, each view we select contributes in the following way. By adopting a top-down modeling approach, our process forces the architect to address SoS boundary first. OV-1 and the use-case diagram forces the architect to model the goals of the SoS as well as the actors that interact to contribute to these goals. Indeed, we use actors to model constituents. is the contribution of each constituent, modeled by lanes in the activity diagram. It is an opportunity for the architect to discover possibly missing constituents, and therefore to ensure the boundary is correctly defined. SV-1, block definition diagram and internal block diagram yield to the configuration the architect intends to model: bdd details the type of the constituents that fulfill the goals previously described in OV-1; bdi shows dependencies between involved constituents, whose knowledge will later be useful to ensure safety and continuity of operation during reconfiguration.

In Section IV, we do not specifically address dynamicity of the architecture. No UPDM view accounts for this specific issue. We leave this issue for future contributions.

In this paper, we focus on a modeling process yielding to a model of the SoS configuration, with subsequent reconfiguration in mind. This is the reason why we select only few of the UPDM's views. Of course, the proposed process of Section IV can be included in a larger process that takes into account additional concerns. In the following, we review why other views are not relevant in the context we consider.

All-views gather only administrative information and indexes. Acquisition views focus on organizational aspects such as the definition of milestones and project timeline. These views are clearly not releveant with respect to our context.

Strategic views define organization-level capabilities, independently of any system. In our case study, these views describe capabilities listed in Section II as well as additional capabilities such as chemical protection capabilities that have been set up, e.g., in anticipation of plant incident. While the content of strategic views may be helpful to design configuration, the anticipation process that yields to strategic views is not in the scope of our work.

Likewise, technical views track standards, rules and conventions that the system implementation must satisfy. Technical views describe for instance the communication conventions that we have implemented in the activity diagrams of Figure 4 or the hierarchical organization modeled by the <<Layer>> stereotype in Figure 7. The process of producing technical views is beyond the scope of our work.

Service-orientated views are used to associate capabilities identified in the operational views with services, that is, units of work with well-defined required and provided interfaces, which are in turn performed by the configuration described in system views. In Section IV, we skip service-orientated views, because we are more interested in the configuration that describes interactions between constituents, rather than the services they implement.

Regarding operational views, we have selected only OV-1 and OV-5, that is, the goals of the SoS as well as the normal course of actions for each goal. Indeed, other operational views concern information model and organizational aspects. Hence other operational views are not of interest in our context. Regarding system views, we have chosen to consider only SV-1, the specification of constituent interactions. While SV-2 would describe links between constituents, we observe that sufficient information in this regard has already been embedded in SV-1.

SV-8 models system evolution as a timeline, where each milestone is characterized by a group of member constituents. In our approach, we rather foresee that each milestone is going to be characterized by a complete SV-1 model, hence containing a group of member constituents along with connection paths in order to be able to describe richer evolutions. Other system views address behavior models, non-functional properties and information models, and are therefore not of interest in the context of our work.

VI. CONCLUSION

In this paper, we proposed a process that helps an architect in designing the configurations of an SoS. For that we selected adequate UPDM views that are relevant with respect to this modeling objective. First, the architect draws out the boundaries of the SoS under consideration, yielding to OV-1 as a use case diagram. In the second step, the architect details the activities associated with each use case, resulting in activity diagrams representing OV-5. In the third step, the architect focuses on the organization of the constituents, yielding to block definition diagrams for SV-1. Last, in the fourth step, the architect designs configurations, which describe constituent interactions as internal block diagrams.

To illustrate the proposed process, we applied it to a real use case, the French emergency service. After having informally described the scenario, our process allowed us to design several configurations, one for each evolution of the SoS. For space reason, in this paper, only two of these configurations are depicted.

For our future work, we plan to rely on the modeled configurations following the proposed process in order to further study the reconfiguration of the SoS architecture. To this end, we will reuse our previous work [START_REF] Petitdemange | Assisting the evolutionary development of SoS with reconfiguration patterns[END_REF], that defines reconfiguration patterns, in order to model how the SoS changes its configuration each time an evolution is required.

Fig. 2 .

 2 Fig. 2. Modeling process

Figure 3

 3 describes the operational collaboration between two CODIS operators. The SDIS 56 operator needs to engage a constituent belonging to SDIS 35: a vehicle equipped with a pump (VTU). It is the first use case. Once the VTU is deployed on the ground, an operational coordination must be established between the SDIS 56 operator and the SDIS 35 team leader. It is the second use case. These two actors communicate via an operational canal as we see in the use case at the bottom of the figure. Communication networks are concerned because part of the path from the vehicle to the intervention is covered by SDIS 35 network only.

Fig. 4 .

 4 Fig. 4. Activity diagrams

  OV-5 and the activity diagram help fully investigating the boundary of the SoS. It requires the architect to tell what constituents contribute to each goal of the SoS, and what


Jérémy Buisson
email: jeremy.buisson@irisa.fr

Seidali Rehab
email: seidali.rehab@misc-umc.org

Generation of Inductive Types from Ecore Metamodels

Keywords: Model-Driven Engineering, Model Transformation, Inductive Type, QVT-Operational, Ecore, Xtext, Coq

HAL is

Introduction

In this paper, we present our work that is specifically related to the implementation of support tools for a formal architecture description language for system of systems engineering, named SosADL [START_REF] Sos | Toolchain for the formal architecture description and analysis of software-intensive systems-of-systems with SosADL[END_REF]. In this paper, we do not intend to describe this novel architecture description language. We would like to put the emphasis on difficulties that arise when we want to benefit from convenient tools like Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF] and, at the same time, formally ensure language properties by means of proofs.

Nowadays the creation of a language and its infrastructure becomes easier thanks to the tools that model-driven engineering offers. Among these effective tools we find MPS [START_REF] Voelter | Language and IDE Modularization and Composition with MPS[END_REF] or Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF]. A complete editing environment can be generated from a combined description of concrete and abstract syntax. This can include syntax-highlighting, auto-completion and elaborated error reporting. A compilation or interpretation framework accompanies these tools in order to smoothly interact with the generated editing environment. For SosADL we choose Xtext to benefit from the mature Ecore/EMF ecosystem.

In the formal side, principled language design has been promoted by language theory. This is done using well-established techniques to specify a language in terms of, e.g., semantics and type system, and then prove that this specification is sound. Proof techniques, relevant properties and proof techniques have been proposed in the meta-theory related to language theory. And several proof assistants as Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions[END_REF] or Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-order Logic[END_REF] have been successfully used to mechanize such specifications and proofs. For SosADL we choose Coq.

The problem in our work is how to ensure the automatic transformation between the two technical spaces in order to benefit from their crossed contributions, so that the disadvantages of one can be overcome thanks to the contributions of the other. This question comes from the fact that there is a difficulty of integration between the modeldriven engineering tools like Xtext or MPS and the proof assistants. Some (modeldriven engineering) researches often rely on graph-based modeling, while the others (proof assistants) use inductive data types, despite some exceptions such as Rascal [START_REF] Klint | Model Transformation with Immutable Data[END_REF].

In other words, we need to make sure that both sides, that is, informal implementation in the Ecore/EMF technical space, and the formal specification in the Coq technical space are consistent. To overcome this problem, we base SosADL tools on the proofcarrying code approach [START_REF] Necula | Proof-carrying code[END_REF]. Therefore, we aim to generate automatically large parts of the infrastructure for proof-carrying code.

In this paper, we study how to generate Coq types for the abstract syntax tree from an Ecore metamodel, such that the abstract syntax of the language is shared in the two technical spaces. Our contribution is an improved transformation in comparison to prior state of the art: constraints on the input metamodel are relaxed, especially with respect to inheritance, to the detriment of not being injective.

The work described in this paper is an extended version of our earlier publication [START_REF] Buisson | Automatic transformation from Ecore metamodels towards Gallina inductive types[END_REF]. In addition to more detailed description of the transformation, we better describe its implementation, and more specifically the transformation framework we have designed. We extend the test suite that we use to validate our transformation with realworld metamodels. And we extend the validation with some discussion of execution time.

Section 2 describes the overall context of our work. Section 3 gives a brief description of Ecore and of inductive types. Section 4 presents related work about transforming from metamodels to inductive types. Section 5 describes a running example that we use in the subsequent description of the transformation, given in Section 6. Section 7 discusses specific points, noticeably why we consider having an injective transformation is not that important in our case. Section 8 gives indications about implementation issues. Section 9 summarizes how we validate the transformation. Finally, section 10 concludes the paper with perspectives.

Context and Motivations

When one wants to use model-driven techniques to implement the supporting tools for a formally-defined language, the question arises how to ensure the implementation actually conforms to the formal definition of the language. In this paper, we consider that this issue is solved by means of proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF].

With the proof-carrying code, the compiler (or any supporting tool for the language) not only generates compiled code. It also generate a verifiable proof of properties about the source or compiled code. By checking the validity of the proof, one can easily ensure that the compiler performed correctly. For instance, the Java compiler generates annotations in the compiled byte-code such that the Java virtual machine can easily ensure that the generated byte-code has been correctly generated, without having to perform complete type checking.

Our general approach described in Figure 1 explains the proof-carrying code approach in the way we apply it to the SosADL [START_REF] Sos | Toolchain for the formal architecture description and analysis of software-intensive systems-of-systems with SosADL[END_REF] context. This one is divided into two parts. The first (upper) part of the figure, which aims to produce at the end output artifacts, starts with the generation of our complete editing environment from a concrete grammar. This operation, which generates a metamodel, an editor, a compilation infrastructure and a parser, is performed using Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF]. Thanks to this generated code, the model that is an instance of the metamodel is obtained from the textual source thanks to the parser. Then, we develop a compiler using the compilation infrastructure, which (the compiler) is in turn the tool for transforming the object-oriented model to the output artifacts. The second (bottom) part of the figure gives the explanation of the proof-carrying code. The proof generation infrastructure is used by our compiler to provide a proof. This proof is an instance of the language's specification, i.e., of the type system or semantics. Terms compose this proof, which represent instances of abstract syntax type. In addition, these terms map with models, and thus we have to ensure a strong consistency between the metamodel and the abstract syntax type, that is, any object that is an instance of a metamodel class maps to a term whose type come from the abstract syntax, and conversely.

Background

In this section, we introduce Ecore and inductive types, which are the two languages which we consider to express an abstract syntax.

Ecore

An Ecore [START_REF] Steinberg | EMF: Eclipse Modeling Framework 2.0[END_REF] metamodel is an object-oriented description of the abstract syntax of a modeling language. An Ecore metamodel consists in hierarchically-nested packages, where the root packages are the Ecore files. Each package contains several classes, which describe the types of objects that can exist in instance models. As usual in objectoriented modeling languages, Ecore supports inheritance and subtyping by means of a specialization-generalization relationship between classes. A specific kind of classes, abstract classes, denote classes that cannot be instantiated in models; only their concrete, i.e., non-abstract specialization classes can be.

An Ecore class contains structural features, namely, the fields declared by the class. In Ecore, fields can be either attributes or references. The former (attributes) denote fields whose type is a plain Java type imported as a data type; while the latter (references) are fields whose type is described by an Ecore type. References are further refined as either containment references or non-containment references, where the semantics of containment is the same as UML's composition.

An instance model, which is an instance of a metamodel, is a tree of objects (according to the containment references) whose classes are the classes described in the metamodel. Additional non-containment references allow to describe arbitrary graphs. An instance model either resides in memory or is serialized to an XMI file.

Orthogonal to the attribute/reference classification, structural features have additional properties. To transparently represent collections, each structural feature has multiplicity indication. The actual kind of collection is further refined by uniqueness and ordering properties. In addition, a feature is said derived when its value is computed on-demand; transient when it is omitted from XMI serialization; or volatile when it is omitted from the in-memory object. Ecore classes also contain operations. But operations are not relevant in the context of this work. Figure 2 shows an example metamodel, which contains an abstract class named Tree specialized by two concrete classes Leaf and Node. So only Leaf and Node can be instantiated in models. While Leaf has no structural feature, Node contains an attribute x, whose type is data type EInt, the data type that imports Java's int primitive type, and two containment references (containment is denoted by the diamond) named left and right. The attribute and the references all have here 1..1 multiplicity, meaning that each instance of Node contains exactly one left Tree and one right Tree.

Inductive Types

Inductive type is a usual approach to the definition of data types in the context of functional programming. Without lack of generality, in the following, we consider the specific case of Gallina and Vernacular, Coq's languages for terms and for module-level commands.

Each inductive type is a set of constructors, each of which declares a variant of the type. The data structure associated with a given constructor is specified by the formal parameters of that constructor. Types are gathered in hierarchical modules, where each file is a module too.

To illustrate, consider the following example in Gallina and Vernacular:

Inductive Tree: Set := | Leaf: Tree | Node: Tree → nat → Tree → Tree.
This code reads as the definition of an inductive type named Tree, for which two constructors are defined:

-When a Tree is built by the Leaf constructor, its does not contain any data: the type of Leaf is Tree. -When a Tree is built by the Node constructor, it contains a Tree, a nat (a natural integer), and another Tree. The type of Node states that it is a function that takes 3 parameters and returns a Tree.

Any value is the result of calling the constructors. A term is therefore inherently a tree that mimics the abstract syntax tree of itself, like: Definition x := Node (Node Leaf 2 Leaf) 6 Leaf.

Related Works

Language theory provides background on how one specifies a language and what properties of such specification should be investigated for in order to convince that the language specification is sound. The idea to extend the theoretical approach to languages with effective tools to help in the implementation of language supporting tools has already been investigated, like witnessed by several projects. For instance, Ott [START_REF] Sewell | Ott: Effective tool support for the working semanticist[END_REF] is a tool that, given a single description of inference rules, e.g., for semantics or type systems, generates boilerplate code, as well as definitions suitable for mechanization with a proof assistant and L A T E X-based documentation. Lem [START_REF] Mulligan | Lem: Reusable engineering of real-world semantics[END_REF] goes one step further and generates in addition executable functions from inductive relations encoding operational semantics or type systems. The K-framework [START_REF]SIMPLE case study[END_REF] is a comprehensive approach to generate interpreters and tools from the executable semantics of a language.

More than just interpreters or tools, it may be convenient to generate compilation infrastructure, as well as full-featured editors and development environments. The idea is not new like witnessed by older projects like Centaur [START_REF] Borras | Centaur: The system[END_REF] and ASF+SDF [START_REF] Klint | A meta-environment for generating programming environments[END_REF]. It has been renewed in the context of model-driven engineering and domain-specific languages, that rise the issue of routinely producing supporting tools and editors for many languages. In this perspective, Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF] generates a full-featured text editor and a compilation framework based on the Eclipse IDE, from a combined description of concrete and abstract syntax. MPS [START_REF] Voelter | Language and IDE Modularization and Composition with MPS[END_REF] is based on projectional editor, i.e., edition is made directly at the level of the abstract syntax. MPS also provides a declarative language for executable type systems. Other language workbenches like Spoofax [START_REF] Kats | The Spoofax language workbench: Rules for declarative specification of languages and IDEs[END_REF] and Rascal [START_REF] Klint | EASY meta-programming with Rascal[END_REF] have similar objectives of generating both compilation infrastructure and IDE services.

There is therefore a need for bridging the gap between model-driven engineering, which enables automatic generation of convenient IDE from the language definition, and formal methods that allows precise specification and analysis of the language and its semantics. To bridge this gap, one possible approach consists in generating a formal description of the language from a metamodel, or conversely in generating a metamodel from a formal language description.

Several previous work have studied how one can analyze a metamodel thanks to tools coming from formal methods, e.g., [START_REF] Barbier | Inductive UML[END_REF][START_REF]On the verification of UML/OCL class diagrams using constraint programming[END_REF][START_REF] Meyer | A systematic approach to transform OMT diagrams to a B specification[END_REF][START_REF] Lano | UML to B: Formal Verification of Object-Oriented Models[END_REF]. These work usually address the question whether a metamodel is consistent, especially when the metamodel is partly specified by constraints such as OCL constraints. These work propose approaches to decide whether the metamodel is inhabited and contradiction-free, i.e., whether some instance model exists and conforms to the metamodel. Since they try to prove properties of the metamodel, the main object made available in the proof assistant is the metamodel itself.

In Section 2 and Figure 1, we have depicted a slightly different issue. What we are interested in is ensuring, here by means of proof-carrying code, that an analysis or a transformation conforms to its specification, and, of course, to encode this specification. In this context, the main object we would like to manipulate in the proof assistant is instances of the metamodel, and not the metamodel itself. So the metamodel has to be transformed into types, such that instances of this metamodel could be transformed into manipulable terms conforming to these types. Such a transformation has already been studied in [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF]. Authors have defined a bidirectional transformation between Ecore and Isabelle's inductive type: each abstract class A is mapped to an inductive type t; and each concrete class C is transformed to a constructor c of the inductive type a mapped from the super class A of C. Fields of class C are mapped to formal parameters of constructors c. Examples given in Section 3 illustrate this transformation scheme on a simple case. To apply this transformation, the metamodel must conform to the strict pattern of having only abstract classes without any super type nor any field, and each concrete class must specialize exactly one abstract class. The transformation is injective. But multiple inheritance, or even having a class that specializes another class that specializes yet another class is prohibited.

Rascal [START_REF] Klint | Model Transformation with Immutable Data[END_REF] comes with another similar transformation. Instead of restricting the metamodel, the transformation described in [START_REF] Klint | Model Transformation with Immutable Data[END_REF] leverages a preprocessing step of the metamodel before the scheme of [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF] is used. First, structural features are pushed to concrete classes (same as our step 6 in Figure 4); then references are generalized, i.e., a reference to any class C is replaced with a reference to C's most general super class, hence flattening the inheritance tree to two levels. After this preprocessing step, the metamodel obviously conforms to the restrictions required by [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF]. The second step of preprocessing intrinsically assumes that a most general super class exists for any class. But in presence of multiple inheritance, this assumption may not hold, unless a class implicitly generalizes all the other classes, e.g., like Ecore [START_REF] Steinberg | EMF: Eclipse Modeling Framework 2.0[END_REF]'s EObject or Java's Object classes. And if such a class exists, it turns out that the transformation issues a single inductive type for this class, to which all the constructors belong. In the end, terms manipulated in the proof assistant are therefore untyped, what is undesirable.

This last comment is the issue we address in this paper. In Section 6, we follow the same principles as [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF][START_REF] Klint | Model Transformation with Immutable Data[END_REF], but without any restriction on the input metamodel. Furthermore, when multiple inheritance is not used, our transformation generates narrower types than the transformation of [START_REF] Klint | Model Transformation with Immutable Data[END_REF] by duplicating constructors. As counterpart, generating a term from a model is going to be harder, because the right constructor has to be selected with respect to the expected type for the term. Like in [START_REF] Klint | Model Transformation with Immutable Data[END_REF], our preprocessing steps break injectivity.

A Running Example

To illustrate the discussion in subsequent sections, we use the metamodel for λ terms of Figure 3. A File is composed of Definitions, each containing a Term. A term is either an Abstraction, an Application or a Variable. In order to avoid issues related to naming and scopes, the abstract syntax assumes variables have already been resolved, hence Variable has a non-containment reference to Binder, which is either an abstraction or a definition. Classes are generic such that terms can be annotated, e.g., with types.

We expect that our transformation generates the following Coq script (or equivalent), i.e., inductive types such that any model that is an instance of the source metamodel can be written as a term whose type is one resulting from the transformation.

The Transformation

The transformation that we propose is decomposed into 12 steps, like shown in Fig- ure 4. It follows the same principle as [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF][START_REF] Klint | Model Transformation with Immutable Data[END_REF]: it maps classes to inductive types, concrete classes to constructors, and structural features to constructor parameters. In our transformation, the improvements lie the preprocessing of the metamodel, especially to handle multiple inheritance in the source metamodel, as well as in the more elaborate post-processing specifically targeted at Gallina and Vernacular. Our transformation does not consider any behavioral element, such as operations and derived, transient or volatile features, as these elements are irrelevant with respect to the context depicted in Section 2. To describe the transformation, we begin first with the Ecore-specific front-end, i.e., steps 1 to 4 in Section 6.1. Then, in Section 6.2, we present the main steps 5 to 8 of the transformation. Last, Section 6.3 describes the Coq-specific back-end containing steps 9 to 12 .

Ecore-specific Front-end

The goal of the front-end step is to first transform the Ecore metamodel in order to normalize and simplify its representation. The first step 1 erases the concept of package: all the classes are gathered in a single top-level package and a single file. Indeed, it would be tempting to map packages to modules. However, while each class can be member of any package, regardless of the relationships between classes, the situation is different in the context of inductive types. The constructors of an inductive type belong to that type, and therefore they are all members of the same module. But like explained in Section 6.2, constructors are mapped from classes. If the packages were not ignored, our transformation would attempt to generate the constructors of a single inductive type within several distinct modules, which is forbidden in the target language.

To illustrate more concretely, consider an abstract class A in package p1, specialized by concrete class C of package p2. In Section 6.2, we will see that class C maps to constructor C, which belongs to type A, itself being mapped from class A. If packages were mapped to modules, type A should be in module P1 and constructor C should be in module P2. This is impossible since constructors belong to types, not to modules.

To show the effect of step 1 , Figure 5 gives an excerpt of the result when applied to the metamodel of Figure 3. The metamodel is almost unchanged. Still, classes from the Ecore metamodel are pulled into the single root package, starting with EObject because it is used as the raw type of type in Term. Because of boundName in Binder, EString is pulled too. Any other class that EObject depends on is pulled as well, and the process is repeated until all the dependencies are gathered. Like shown in the XMI excerpt of Figure 5, the transformation encodes the name of the originating package in the class name. By using this systematic renaming scheme, the transformation avoids name clashes after all the classes are gathered in a single package.

In step 2 , the transformation deals with the representation of types in Ecore. In its early versions, Ecore did not support generic classes. In this context, types and classes were confused in a single concept. Thus, the type of, e.g., a reference or an attribute were given as a direct reference to the data type or to the class. Since the introduction of generic classes in Ecore, types and classes have been made two distinct concepts, yielding to the introduction of EGenericType to represent types. But due to backward compatibility, old-style types are still allowed when referring to non-generic data types or classes. Figure 5 contains examples of both:

-The super class of lambda_Binder (line 4) is given as a direct reference to the ecore_EObject class, which is indeed a non-generic class. -The type of boundType (line 8) is given as an instance of EGenericType, here to represent type variable U.

Step 2 translates all the types to a simpler uniform representation, whose abstract syntax is given in Figure 6, regardless the types were initially given old-style or newstyle. We define five kinds of types:

-GEClassifierType is a type built by applying effective parameters (eArguments) to a possibly generic classifier, i.e., either a data type or a class. If the referenced classifier is not generic, i.e., if it does not have any formal type parameter, then eArguments is empty. -GEVariableType is a type variable eTypeParameter, e.g., bound by an enclosing generic classifier. -A GEAnyType represents the any-type wildcard.

-GELowerBoundType is a wildcard type with a lower bound.

-GEUpperBoundType is a wildcard type with an upper bound. direct reference to ecore_EObject, is now encoded as an instance of GEClassifierType (lines 5 and 6); and the type of boundType is an instance of GEVariableType referring to formal type parameter U of lambda_Binder (lines 14 and 15).

Steps 3 erases behavioral elements, that is, operations and derived, transient or volatile features. In step 4 , all the non-containment references are replaced with attributes of type _URI. These attributes are intended to store identifiers of the referred objects. Feature multiplicities are expanded to appropriate collection types at the same time, hence completing the simplification of the types:

-Features with 0..1 multiplicity are mapped to type _Option.

-Features with 1..1 multiplicity keep their original type.

-Features with m..n multiplicity where n ≥ 2 are mapped to types _List, _Set or _Bag, depending on uniqueness and ordering properties stated in the source Ecore metamodel.

In subsequent steps of the transformation, these collection types are suitably interpreted such that they are ultimately mapped to corresponding Coq types.

Core of the Transformation

During steps 5 to 7 , constructors are added to the classes, before they can be turned into inductive types.

First, in step 5 , each concrete class of the metamodel is mapped to a newly-created constructor. Figure 8 illustrates the result of step 5 : in this excerpt, two constructors are created for the two concrete classes Abstraction and Definition. Each constructor refers to the structural features defined or inherited by the corresponding class.

Then in step 6 , structural features are pulled down and cloned into the constructors, through inheritance. Like shown in the excerpt of Figure 9, the structural features are duplicated to all the constructors that inherit from them. Step 6 also ensures correct handling of generic classes by substituting type variables when the structural features are inherited, like illustrated by type and boundType in Figure 9.

The last step that deals with constructors is step 7 . This step duplicates constructors previously built up at each level of the generalization relation, including at abstract classes. For instance, because the Abstraction class inherits from the Term and Binder abstract classes, the Abstraction constructor is duplicated at these two classes. Because Binder is also a generalization of the Definition class, the Binder class is also made containing a duplicate of the Definition constructor. At the end of step 7 , the generalization / specialization relation can be discarded. For each constructor duplicate, an assignment stores the precise type of the value built, hence taking into account of generic classes correctly.

Step 8 straightforwardly turns each class into an inductive types, without any further transformation.

Coq-specific Back-end

In Gallina and Vernacular, it is forbidden that an inductive type refers to another type that is not previously defined or that does not belong to the same group of definitions. Inductive type definitions must be ordered accordingly to their dependencies. To do so, step 9 computes strongly connected components in the dependency graph in order to build groups of types, then this step sorts the groups according to topological order.

For instance, in the result of step 9 , types Binder and Term shall be in the same group, since they refer each other. Indeed, constructor Variable (in Term) has a parameter of type _URI<Binder<V>>; and constructor Definition (in Binder) has a parameter of type Term<D>. This group is put before Definition, which refers to Term.

Step 10 ensures that each name is unique, as well as conforms to lexical constraints of Gallina and Vernacular. Step 11 introduces Vernacular commands (like Inductive) and builds Gallina terms for each type to build a correct script.

Traceability

Orthogonal to the previously described steps, the transformation ensures traceability. That is, it records mapping information between objects in the source metamodel, objects in intermediate steps and objects in the Gallina model. This information is subsequently used when instances of the source metamodel have to be transformed into Gallina terms.

Discussion

Our transformation restricts to metamodels that strictly conform to Ecore constraints as implemented in EMF, including constraints at the warning level.

In addition, the following patterns are ignored:

-When a multi-valued reference in an Ecore metamodel refers to a class that contains two features named key and value, and when this class's instance class name is java.util.Map$Entry, the Ecore tool chain handles this reference as a hash map.

Our transformation ignores the pattern, yielding to a collection of pairs. «abstract» A x: EInt «abstract» A B B x: EInt Fig. 11. Two different metamodels yielding to identical Coq scripts. Source [START_REF] Buisson | Automatic transformation from Ecore metamodels towards Gallina inductive types[END_REF].

-When a multi-valued attribute has type EFeatureMapEntry and if it is suitably annotated, the attribute declares a feature map, that is, a structural feature that merges several subset structural features in a single one. Values in the collection are indexed by subset features. Because the subset features must be volatile, transient and derived, they are erased at step 3 of our transformation. But the attribute's type is not decoded to the correct type, which should be the union of the types of all the grouped subset features.

Except the above-described limitations, Ecore is fully supported. Hence the transformation cannot be injective. To illustrate the reason, consider Figure 11: the two metamodels, despite different, result in identical Coq scripts. When the structural features are pulled from classes to constructors at step 6 , our transformation does not track the class they originate from. By the way, this information is irrelevant in Gallina.

The fact that the two metamodels yield to the same Coq script is not an issue: any model that is an instance of any metamodel of Figure 11 is also an instance of the other one. Indeed, these models contain only instances of B that contain an integer named x, regardless x is declared in B or inherited from one of its super classes.

Still Like described in Section 6, the transformation is a pipeline decomposed in many steps. This approach makes each individual step simpler as each one focuses on a single issue (or few related issues). The first steps 1 to 4 of the transformation are specific to Ecore, and steps 9 to 12 are specific to Gallina and Vernacular. If other source or target languages were considered, only the related steps would have to be changed. Consider MOF [START_REF]OMG: OMG Meta Object Facility (MOF) Core Specification[END_REF] for instance: according to [START_REF] Gerber | MOF to EMF: There and back again[END_REF], older versions of MOF and Ecore are convertible to one another. To adapt the transformation to MOF, step 1 has to deal with nested classes, e.g., similarly to the way packages are merged; step 4 has to deal with MOF's richer reified associations; and data type mapping has to be updated, since MOF is not based on Java types. Likewise, switching to, say, Isabelle/HOL would require changing steps 10 and 11 in order to take into account the different abstract and concrete syntax.

Implementation

The decomposition of the transformation in multiple steps allows us to mix several implementation technologies. Our overall choice is in favor of industrial-strength freelyavailable technologies: Eclipse's mature EMF-and-Java ecosystem. Model-to-model transformations are implemented in plain Java and QVT-Operational. The final modelto-text step 12 uses Acceleo.

Steps 1 to 10 perform only local modification. At each of these steps, when considered individually, the transformation rebuilds the overall structure of the source (meta)model into the target one, only substituting some specific subtrees. Rather than using a general-purpose approach to model transformation, we design an ad-hoc framework that duplicates an EMF (meta)model with hooks to customize its behavior at some features of some classes. Our framework is a mixture of EMF's EcoreUtil.copy, ATL's refining mode [START_REF] Tisi | Refining models with rule-based model transformations[END_REF] and Rascal's visit operation. But unlike these inspiring approaches, our framework is not restricted to endogeneous transformations, and therefore adopts a copy-based strategy.

The overall algorithm of our framework is given, in pseudo-Java code, in Figure 12. At lines 2 and 3, the algorithm uses EMF's reflection to clone the object at the root of the subtree that must be transformed. The remapClass hook lets the transformation change the class of the object on the fly. Then at line 4, the algorithm records the mapping between source and target objects, in order to later resolve references. Each structural feature of the target class (line 5), is mapped back to a structural feature of the source class (line 6) by the remapFeatureBack hook.

-If the target feature is a containment feature, values are assigned immediately (line 10). By default, the remapValue hook calls the clone function in order to recursively copy model objects.

-If none of the source feature and target feature is a containment feature, the task is registered for post-processing (lines 14 and 15). After the source model has been fully handled, post-processing tasks call the remapReference (lines 26 and 27), which, by default, looks in the mapping table to set the reference in the target object (line 28). -With our framework, it is non-sense when the source feature is a containment feature, while the target feature is not. Line 17, our algorithm raises an error in this case. On top of this framework, we provide an implementation of the hook functions (remapClass, remapFeatureBack, remapValue and remapReference) based on Java reflection, yielding to simpler description of the transformation steps. Figure 13 illustrates our framework with the real source code for step 3 . In the constructor at lines 3 and 4, it directs the framework to remap classes of the Generic package to classes with same name (except a prefix) of the Structural package. The rule at lines 6 to 17 implements a remapValue hook for eStructuralFeatures of a SEClass target object, when it is mapped from a GEClass source object. Lines 8 to 11 retrieve the default behavior of the hook, that is, the cloning of objects as a function named transformer. Then, the rule retrieves the eStructuralFeatures of the source object (line 11), filters those that are neither derived nor transient nor volatile (lines 12 and 13), applies the default behavior transformer to the retained objects (line 14), and put the resulting objects in eStructuralFeatures of the target object (line 16). Other structural features in any other class are just copied by the framework. By not having any structural feature named eOperations in SEClass, operations are omitted in the target (meta)model, without any further programming.

At step 11 , QVT-Operational seems a good choice as it avoids most of the notation burden. Disjunct mapping and collection operations like iterate remind patternmatching and higher-order functions, like usually found in functional programming. For the purpose of the comparison, we have also manually translated the QVT-Operational transformation into strictly equivalent Java code.

Our implementation records mapping information between source objects and generated ones, including intermediate ones, using a generic one-to-one correspondence metamodel. In order to deal with the size of mapping information, especially in the context of EMF's XMI serialization, our implementation produces two records:

-Summarized mapping information record only indirect mapping from each source Ecore object to the corresponding Gallina objects, hence omitting intermediate steps.

-Full mapping information is split into fragments in order to keep the size of each fragment below a fixed threshold. This trick lowers memory consumption by EMF's XMI serialization code. Synthetic objects, which do not belong to any intermediate model, are saved alongside mapping information.

Most of the transformation steps are exogeneous transformations, with the only exception of step 10 that is endogeneous. By making this choice, the abstract languages for target metamodels are fitted to the needs. Doing so is required to for implicit removal of objects by our framework, such as the removal of operations at step 3 like previously described. The whole transformation involves 11 different metametamodels. In the pipeline of the whole transformation, each two consecutive metametamodels must remain consistent for the elements that are not directly affected by the concerned step. Managing such 11 different metametamodels while maintaining their consistency appears to us to be a tedious and error-prone task during development, despite the small size of the metametamodels3 . We would have appreciated lightweight mechanisms for automatic application of some editing commands to a group of several metametamodels. Using transformations engines, e.g., based on QVT or ATL, for such operations appeared inconvenient: such transformations would have had to be generic enough to be applicable to several similar-yet-different metametamodels, while not offering any reuse opportunity because editing commands are one-shot.

The Java code for steps 1 to 10 contains 1555 SLOC, and the underlying Javabased framework contains 320 SLOC according to ohcount. The QVT-Operational script for step 11 is made of 218 SLOC and its Java translation contains 655 SLOC. The Acceleo template for step 11 contains 41 SLOC. The code is available at https: //bitbucket.org/jbuisson/ecore2coq.

Validation

To evaluate our transformation and our implementation, we build a benchmark suite from four third-party open-source projects, in addition to the metamodels involved in our transformation itself: EMF, Eclipse's OCL, Xtext extras, and Dresden OCL. In total, we gather 80 Eclipse projects from the repositories of these projects. Like summarized in Table 1, these projects contain 279 Ecore metamodel files, of which 241 are unique files. At the completion of Eclipse's builder task, some of these metamodels are duplicated in target directories, yielding to 338 Ecore metamodel files. In this suite, 319 files pass EMF's validator without any error nor warning, of which 226 are unique files. Our transformation produces 319 Coq scripts, of which 197 are unique files, hence illustrating that our transformation is not injective. The metamodels of our benchmark involve multiple inheritance. At most, one class has 8 immediate super types, increased to 9 after step 1 . The depth of inheritance is up to 11 levels.

Metrics on Source Metamodels and Generated Scripts

Validity of the Generated Scripts

As a first validation, we ensure that the transformation produces correct Coq scripts. To do so, we invoke the Coq compiler on each of them. Of the 319 generated scripts, 315 pass successfully compilation. Manual inspection lets us ensure that the generated scripts correspond to the source Ecore metamodels.

The remaining 4 scripts raise Coq's non strictly positive occurrence error. To better understand this error, consider the anti-pattern and generated script of Figure 14. The generated type U recursively uses itself in the type of parameter x, as a parameter of generic type T. By doing so, and depending on the type of T's constructors, one can make the logic inconsistent, but, in the case of Figure 14, this is not the case. Still Coq 4 restrict definitions of inductive types to conform to a syntactical criterion, named strictly positive recursive occurrences in order to ensure that any inconsistent definition is rejected. However, the syntactical criterion is a conservative one, hence ruling out some consistent definitions too. In Figure 14, the alternate definition of T, which differs only in Coq's internal treatment, allows to work-around the criterion by moving parameter A to the inductive type itself instead of the constructor. This alternate definition shows that, in this example, our transformation generates only consistent definitions. Figure 14 is representative of the 4 failing scripts. Because the problematic parameters are type parameters of generic classes, one could think the error could be avoided by simply changing our transformation to put type parameters at the inductive type, rather than at constructors. But doing so would prevent a non-generic class, e.g., V to inherit from, e.g., T<W> (dashed in Figure 14, where W is yet another class), while such a construct is perfectly permitted by our transformation and yields no error in the generated Coq script.

The error could be worked-around by specializing generic classes, that is, by doing partial application of type parameters. We have not yet included this strategy in our transformation.

Execution Time of the Transformation

Using the same benchmark, we have measured the execution time spent in the transformation with several platforms. In this perspective, we instrument the transformation in order to measure the time spent in each step, including serialization of the result but excluding XMI deserialization of the input. To mitigate intrinsic variations of execution time, each step is preceded by an invocation of the garbage collector. We also do our best to make the transformation reproduce identical artifacts regardless the execution environment, sometimes at the cost of sub-optimal implementation, e.g., to ensure identical order of elements even in unordered collections. In order to avoid effects of cache and JIT, every source metamodel is transformed several times before execution time is measured.

Table 3 gives the details of the execution platforms we use. For each platform, we enable G1 garbage collector and string deduplication in the Java virtual machine. In each run, we use a headless Eclipse product.

Measured execution time are given in Table 4. We first use platform D to compare Java and QVT-Operational implementations of step 11 : we observe that the Java implementation is 30 times faster than the QVT-Operational implementation. After this first observation, we measure execution time only for the Java implementation using the other platforms, hence showing that, even with real-world metamodels, our transformation is compatible with use in interactive IDE. By comparing two runs on each platform, we evaluate variability of the execution time, here up to 2.6%, despite efforts to mitigate. Because the transformation is intended to be used in interactive environments, we do not feel necessary to have more accurate measures.

To assess the relevance of summarized mapping information, the two last lines of Table 4 give the time spent when full mapping information is saved, including synthetic objects and intermediate objects generated at each step. We observe the time spent in these tasks is large in comparison to the time spent in the transformation. To better explain, in the case of Dresden OCL's UML metamodel, the biggest one of our suite, 59793 synthetic objects are created and 7414201 correspondences are recorded, while summarized mapping contains only 6287 correspondences. For the complete benchmark suite, 20GiB are generated for synthetic objects and mapping, to be compared with 6.9MiB input Ecore files, 2.5GiB generated models and 359MiB summarized mapping. This observation confirms that saving full mapping information should be avoided if unnecessary.

Usability in the Context of Proof-Carrying Code

To ensure that the generated scripts are actually usable in the context of proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF], we fully applied the approach depicted in Figure 1 in the implementation of tools supporting SosADL [START_REF] Sos | Toolchain for the formal architecture description and analysis of software-intensive systems-of-systems with SosADL[END_REF]. This paper focuses on automating only the transformation of the Ecore metamodel towards Gallina inductive types. Hence the others tasks either involve preexisting tools such as Xtext [START_REF] Bettini | Implementing Domain-Specific Languages with Xtext and Xtend[END_REF] or are done by hand. Noticeably, the transformation of SosADL architectures into Gallina terms has been manually written. Then we manually instrument SosADL's type checker in order to produce proofs that witness that the architecture under consideration is actually well-typed. Last we use Coq to check the correctness of all the generated artifacts.

This experiment witnesses that the types generated by the transformation described in this paper conform to the requirements of a proof-carrying code infrastructure.

Conclusion

In this paper, we describe a transformation from Ecore metamodels to inductive types. This transformation allows to set up a model-driven language engineering chain, e.g., involving Xtext and, at the same time, to specify the language using a proof assistant, such as Coq, and then prove properties of this specification. In comparison to previous work [START_REF] Djeddai | Integrating a formal development for DSLs into meta-modeling[END_REF][START_REF] Klint | Model Transformation with Immutable Data[END_REF], our transformation has fewer constraints on the source Ecore metamodel and ensures stronger typing in the generated inductive types, but it is not injective.

To validate our proposal, we implement the transformation using QVT-Operational, Acceleo, and EMF-and-Java. We fetch of 226 Ecore metamodels from open source projects, in order to gather both synthetic and real-world metamodels for the purpose of benchmarking. For all of them, except 4 metamodels, our transformation produces valid Coq scripts. The 4 erroneous cases correspond to a specific pattern that infringes a syntactic criterion that prevents Coq from accepting potentially inconsistent type definitions. Still, this criterion is a conservative approach, and we analyze that, in our case, none of the generated type definitions may introduce any contradiction in the underlying logic. We propose to further study this point, investigating how partial application of type parameters may work-around Coq's restriction.

Our experience shows that, regardless the execution platform, our transformation scales to real-world metamodels.

In the near future, we will continue automatic generation of the proof-carrying code infrastructure from an Ecore metamodel. Our next step will be to produce a second transformation, that will generate the transformation from instance models to terms, such that the terms have the types generated by the transformation described in this paper.

Fig. 1 .

 1 Fig.1. The big picture of our general approach.

Fig. 2 .

 2 Fig. 2. Example of a simple Ecore metamodel.

FileFig. 3 .

 3 Fig.3. Ecore metamodel of the example. Source[START_REF] Buisson | Automatic transformation from Ecore metamodels towards Gallina inductive types[END_REF].

Fig. 4 .

 4 Fig. 4. Decomposition of the Ecore-to-Coq transformation.

Figure 7 Fig. 6 .

 76 Figure7shows an excerpt of the resulting XMI file, in our running example. For instance, the super-class of lambda_Binder, which where initially given as an old-style

Fig. 8 .Fig. 9 .Fig. 10 .

 8910 Fig. 8. Metamodel excerpt after step 5 introduce. Source [8].

Fig. 12 .

 12 Fig. 12. Pseudo-code of our Java-based transformation framework.

  Type → Type := | T T: ∀ (A: Type), (T A). Inductive U: Type := | U U: ∀ (x: T U), U. (* alternate definition of T *) Inductive T (A: Type): Type := | T T: (T A).

Fig. 14 .

 14 Fig. 14. Anti-pattern leading to Coq error.

  Fig. 5. XMI excerpt after step 1 link. Source [8].

	1 < LEPackage >
	2	< eClassifiers name =" ecore_EString " ... / >
	3	< eClassifiers name =" lambda_Binder "
	4	eSupertypes =" // ecore_EObject " ... >
	5	< eTypeParameters name ="U" / >
	6	< eStructuralFeatures name =" boundName " ... / >
	7	< eStructuralFeatures name =" boundType " ... >
	8	< eGenericType eTypeParameter =" // lambda_Binder /U" / >
	9	</ eStructuralFeatures >
	10	</ eClassifiers >
	11	...
	12 </ LEPackage >

  , we can further analyze what steps of the transformation are injective, and what steps are not: -Steps 5 , 8 , 11 and 12 are straightforwardly injective.-When the naming scheme is robust enough, steps1 and 10 are obviously injective too. -Step 4 is not injective, mainly because multiplicities are simplified as one of 0..1, 1..1 or 0.. * . Though, Gallina would allow to preserve any exact multiplicity if desired. -Step 2 is trivially not injective because Ecore's representation of non-generic types is not unique. But making the distinction between old-style representation and EGenericType is irrelevant as both are considered as interchangeable by the Ecore tool chain. -Step 9 discards the order of metamodel elements. -Steps 3 , 6 and 7 discard information from the metamodels.

  Fig. 13. Java code for step 3 eliminate.

	1 public class G2S extends GenericRemapper {
	2	public G2S () {
	3	super ( GenericPackage . eINSTANCE , " GE " ,
	4	StructuralPackage . eINSTANCE , " SE " );
	5	}
	6	@Rule public void eStructuralFeatures (
	7	GEClass source , SEClass target ) {
	8	Function < EObject , EObject > transformer =
	9	maybeTransform ( GE_CLASS__ESTRUCTURAL_FEATURES ,
	10	SE_CLASS__ESTRUCTURAL_FEATURES );
	11	source . getEStructuralFeatures (). stream ()
	12	. filter (( s) -> !s. isDerived () && !s. isTransient ()
	13	&& !s. isVolatile ())
	14	. map ( transformer )
	15	. map ( cast ( SEStructuralFeature . class ))
	16	. forEach ( target . getEStructuralFeatures ():: add );
	17	}
	18 }

Table 1 .

 1 Summary of the benchmark suite.

		Ecore files Ecore files Ecore files Coq scripts
		(downloaded) (after build) (validated) (generated)
	raw count	279	338	319	319
	unique files	241	241	226	197

Table 2

 2 summarizes some metrics about few source metamodels and generated scripts. The biggest metamodel is the UML metamodel in its version coming from the Dresden OCL project: it contains 247 classes, of which 199 are concrete and 48 are abstract. It

		Ecore source		after step 1 link		Gallina target
		classes				classes
	File	concr.	abs.	type enum. concr.	abs.	type enum.	ind. cons.	def.
		20				20
	Ecore	15	5	33	0	15	5	33	0	20	61	41
		247				265
	UML	199	48	4	13	212	53	15	13	278 1964	23
						...
		4113				11578
	Total	3421	692	943	210 8777 2801 4092	367 11945 43584 6675

Table 2 .

 2 Metrics on source metamodels and generated scripts. also contains 4 data types and 13 enumeration types. Not shown on Figure 2, the classes of the source metamodel contain 508 references and 110 attribute; increased to 554 references and 140 attributes after step 1 . After step 1 , additional classes are pulled in, increasing the size to 265 classes (212 abstract classes and 53 concrete classes), 15 data types and 13 enumeration types. Because one inductive type is generated for each class and for each enumeration type, 278 inductive types are generated, which altogether define 1964 constructors. The 23 generated type definitions come from the 15 data types after step 1 , and 8 predefined types definitions, i.e., types like _URI and _Option mentioned at Section 6.1. In total, the source metamodels of our benchmark contains 3421 concrete classes and 692 abstract classes containing 5529 references and 2996 attributes, 943 data types and 210 enumeration types. After step 1 , it contains 11578 classes (8777 concrete classes, 2801 abstract classes, 23743 references and 13589 attributes), 4092 data types and 367 enumeration types. Our transformation produces 11945 inductive types made of 43584 constructors, as well as 6675 type definitions.

Table 3 .

 3 Execution platforms used in experiments. .4 67.0 68.2 61.0 61.0 82.9 81.2 10 rename 65.5 65.9 34.3 34.0 33.5 33.5 61.6 60.9 11 generate 39.2 39.1 19.5 19.5 19.6 19.1 42.1 1332.9 12 generate 94.1 95.3 52.6 50.2 45.1 45.1 49.6 49.0 save mapping summary 193.1 199.2 119.3 116.5 114.5 115.5 123.8 123.3 Total (transformation) 1120.5 1142.9 534.1 523.6 497.7 510.0 643.2 1923.6 save synthetic objects 579.5 579.1 358.6 353.8 357.2 370.3 437.5 433.1 save full mapping 2731.9 2737.4 1658.4 1727.5 1748.7 1709.9 1817.1 1792.9

	Platform CPU	RAM OS			JDK		Heap size
	A	2x Xeon L5640	48GiB Debian 9.4		Oracle 8 162 64-bits	16GiB
	B	4x Xeon E5-2630 v4 128GiB Debian 9.2		Oracle 8 162 64-bits	16GiB
	C	4x Xeon E5-2630 v4 128GiB Debian 9.2		Oracle 10+46 64-bits	16GiB
	D	1x i7-4702HQ	16GiB Windows 10 1709 Oracle 10+46 64-bits	8GiB
			A		B		C		D
	Step		Java 1 Java 2 Java 1 Java 2 Java 1 Java 2 Java QVTo
	1 link	7.7	7.5	2.8	2.9	2.7	2.7	9.4	9.4
	2 normalize	5.8	5.7	2.1	2.1	1.9	2.0	6.9	6.6
	3 eliminate	3.9	3.8	1.3	1.2	1.2	1.2	5.0	5.0
	4 eliminate	4.8	4.6	1.8	1.8	1.6	1.7	5.6	5.4
	5 introduce	5.8	5.6	2.2	2.2	2.1	2.1	6.4	6.1
	6 percolate	14.8 15.4	6.2	6.0	5.7	5.9 10.7 10.5
	7 flatten	495.4 509.4 202.1 196.6 187.3 197.9 207.6 202.9
	8 translate	43.8 45.0 22.9 22.4 21.5 22.3 31.7 30.5
	9 schedule	146.7 146

Table 4 .

 4 Measured execution time (seconds) of each individual step.

Each metametamodel contains approximately 20 classes, 50 references, 30 attributes, and 30 data types