Stefan Naujokat
email: stefan.naujokat@cs.tu-dortmund.de

Louis-Marie Traonouez
email: louis-marie.traonouez@inria.fr

Malte Isberner
email: malte.isberner@cs.tu-dortmund.de

Bernhard Steffen
email: steffen@cs.tu-dortmund.de

Axel Legay
email: axel.legay@inria.fr

Domain-Specific Code Generator Modeling: A Case Study for Multi-Faceted Concurrent Systems

In this paper we discuss an elaborate case study utilizing the domain-specific development of code generators within the Cinco meta tooling suite. Cinco is a framework that allows for the automatic generation of a wide range of graphical modeling tools from an abstract high-level specification. The presented case study makes use of Cinco to rapidly construct custom graphical interfaces for multi-faceted, concurrent systems, comprising non-functional properties like time, probability, data, and costs. The point of this approach is to provide user communities and their favorite tools with graphical interfaces tailored to their specific needs. This will be illustrated by generating graphical interfaces for timed automata (TA), probabilistic timed automata (PTA), Markov decision processes (MDP) and simple labeled transition systems (LTS). The main contribution of the presented work, however, is the metamodelbased domain-specific construction of the corresponding code generators for the verification tools Uppaal, Spin, PLASMA-lab, and Prism.

Introduction

Code generators can be regarded as the enablers for model-driven software engineering (MDSE) [START_REF] Brambilla | Model-Driven Software Engineering in Practice[END_REF], as they provide the means to bridging the final gap to the actual use of a system. Despite this importance the state of the art is still pretty disappointing: typically, models and code generators in MDSE environments are very generic and only generate partial code which needs to be manually completed. This does not only require a lot of expertise but it also leads to the typical problems of round-trip engineering whenever the systems evolve. Domain-specific tools have the potential to overcome this situation by providing full code generation for their naturally more restrictive contexts.

Metamodeling frameworks support the development of domain-specific modeling environments to great extent, but the development of code generators for a domain-specific language (DSL) defined in those frameworks is still a complicated task despite the existence of special code generator DSLs, such as Xtend [START_REF]Xtend[END_REF] for the Eclipse modeling ecosystem [START_REF] Gronback | Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit[END_REF], the MetaEdit+ Reporting Language (MERL) [START_REF]MetaEdit+ Version 4.5 Workbench User's Guide -5.3 MERL Generator Definition Language[END_REF] in the context of Domain-Specific Modeling [START_REF] Kelly | Domain-Specific Modeling: Enabling Full Code Generation[END_REF] with MetaEdit+ [START_REF] Kelly | MetaEdit+: A Fully Configurable Multi-User and Multi-Tool CASE and CAME Environment[END_REF], or the IPTG language of Eli/DEViL [START_REF] Kastens | The Eli System[END_REF][START_REF] Schmidt | Generating visual structure editors from high-level specifications[END_REF]. These code generator DSLs provide means that extend the possibilities of manual programming with simple string concatenation or template frameworks, but they are difficult to learn and very generic: they are specific to the underlying metamodeling framework, but do not exploit the specifics of the considered problem domain.

The Cinco framework3 [START_REF] Naujokat | Full generation of domain-specific graphical modeling tools: a meta 2 modeling approach[END_REF] aims at aiding in the development of domainspecific modeling tools in a holistic fashion that in particular comprises code generation. While the domain's metamodel and the graphical editor can be fully generated from higher-level specifications, Cinco additionally provides modeling tool developers with a domain-specific code generator language specifically generated for their tool. In fact, this domain-specific code generation language can be automatically obtained from the same abstract specification as the GUI.

In this paper we discuss an elaborate case study utilizing this domain-specific development of code generators within the Cinco meta tooling suite: we show how to rapidly construct custom graphical interfaces for different kinds of concurrent systems, comprising non-functional properties like time, probability, data, and costs. As a result, the corresponding user communities and their favorite tools are provided with graphical interfaces tailored to their specific needs. This will be illustrated by generating graphical interfaces for timed automata (TA) [START_REF] Alur | A theory of timed automata[END_REF], probabilistic timed automata (PTA) [START_REF] Kwiatkowska | Automatic verification of real-time systems with discrete probability distributions[END_REF], Markov decision processes (MDP) [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF] and simple labeled transition systems (LTS) [START_REF] Katoen | Labelled Transition Systems[END_REF]. The main contribution of the presented work, however, is the metamodel-based domain-specific construction of the corresponding code generators for the verification tools Uppaal [START_REF] Bengtsson | Uppaal -a Tool Suite for Automatic Verification of Real-Time Systems[END_REF], Spin [START_REF] Holzmann | The SPIN Model Checker -Primer and Reference Manual[END_REF], PLASMA-lab [START_REF] Boyer | Plasma-lab: A flexible, distributable statistical model checking library[END_REF], and Prism [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF].

We do not know of any other approach that provides the automatic generation of domain-specific code generator languages. As mentioned before, existing languages are commonly specific to the used modeling framework, but not specific to one's very own metamodel. Cinco's code generation concepts are based on preliminary work [START_REF] Jörges | Construction and Evolution of Code Generators -A Model-Driven and Service-Oriented Approach[END_REF][START_REF] Lybecait | Entwicklung und Implementierung eines Frameworks zur grafischen Modellierung von Modelltransformationen auf Basis von EMF-Metamodellen und Genesys[END_REF] for the creation of transformation and code generation modeling components for arbitrary Ecore [START_REF] Steinberg | EMF: Eclipse Modeling Framework (2nd Edition)[END_REF] metamodels.

The paper is structured as follows: in order to be able to explain the Cinco specification, transformation and code generation concepts using the "PSM" (Parallel Systems Modeling) case study as running example, the upcoming Section 2 motivates and explains it in detail. Section 3 then presents the basic concepts of Cinco and how the specification of the full graphical editor works. Section 4 details on the code generation concepts and how the individual code generators for our target tools are realized, before Section 5 elaborates on the model-to-model transformation of the various source model types into the PSM intermediate language. The paper concludes with a summary and plans for future work in Section 6.

The PSM Case Study

There is a wealth of model checking tools of concurrent systems, each with their own profile concerning the supported communication paradigm and features like time, probability, data, and costs. It is therefore not surprising that these tools come with dedicated input languages and formats, which can be graphical as in the case of Uppaal or textual, as in most other cases. This makes it difficult to work with (more than one of) these tools, in particular, as one needs to be aware of their syntactic peculiarities.

The "Parallel Systems Modeling" (PSM) case study therefore facilitates Cinco to rapidly construct custom graphical interfaces for the types of concurrent systems supported by those tools. The envisioned realization does not only allow one to customize the graphical interface, but also to generate tool-specific code which can directly be used as input in the considered tool landscape. In fact, it is possible to easily design one's own graphical language which can then be provided at low cost with code generators for the input formats of the considered tools.

Architecture

In our case study project several different model types (or languages) are involved, each of them represented by an own metamodel generated from a Cinco specification. Fig. 1 illustrates their overall architecture and interplay based on various model to model (M2M) and model to code (M2C) transformations.

Graphically designed model structures for LTSs, MDPs, TAs, and PTAs are transformed into the PSM superset language which faithfully captures all language paradigms provided by those 'source' languages. This richness implies some discipline in its use: by far not every syntactically correct PSM model makes sense. Of course, this does not pose any problems for the PSM models generated from the graphically designed 'source' language models, as they are consistent by construction. Moreover, constraints reminiscent of a type discipline can be used to address the consistency problem also directly at the PSM level.

The code generators for the considered target tools are then based on this PSM language to have one common technical input format that is available to all code generators. Of course, although the PSM models are consistent by construction, not each of them can be fed into all the code generators, as not all considered model types are supported by all target tools. Sometimes unsupported features can be emulated by others, e.g. modeling probabilistic decisions as nondeterministic choices, but in case this is not possible, the respective code generator will produce an error message.

Language Feature Selection

As a starting point, we have begun developing the PSM model type to contain the following language features of LTSs, MDPs, TAs, and PTAs (further features can be added at need):

Modules (or processes) define the concurrent components of the system. Each module is designed with a dedicated automaton.

States are the most fundamental modeling components. Their description typically comprises a name (i.e. a unique identifier), and additional information in terms of atomic propositions like being a start or an accepting state.

Data is stored in local variables (that belong to a module) or global variables. They can be updated with arbitrary expressions using assignments. We assume a C-like syntax for the expressions. Integer and Boolean variables are currently available, with the former one having a defined range (usually smaller than [0,MAXINT]).

Time is modeled using dedicated clock variables that all increase at the same pace. Clocks are always local and can only be reset (i.e. set to 0 using an assignment).

Guards and Invariants are expressions over all the variables that control the possible evolution of a module. Guards are assigned to edges and control which transitions are possible in a given a state. Invariants are assigned to a state and limit the evolution of clock variables in this state.

Probability is frequently used in models to represent uncertain behavior. It can be inserted using probabilistic decision nodes that split a transition into several outcomes according to probability weights. Additionally, a rate can be assigned to each state to model an exponential distribution for modeling the progress of time. Nondeterminism is allowed whenever two transitions are enabled at the same time.

Arbitrary Code in form of C functions is realized in two ways. In the first case a dedicated node type contains a String attribute where the function body can be inserted. The second case makes use of Cinco's prime reference concept: Externally defined components can be placed in the model via drag&drop, creating a different kind of node that is automatically linked to that external element. This way arbitrary external libraries of modeling components can be included without the need to change the tool or metamodel. This closely resembles the concept of Service Independent Building Blocks (SIBs) from jABC [START_REF] Steffen | Model-Driven Development with the jABC[END_REF].

Communication between processes is realized with channels on via transitions may be synchronized. They are declared globally and can be of three types:

-Pairwise (handshake) synchronization involves two transitions (possibly identified with input and output modalities added to the channel) chosen among the possible synchronizations. -Global synchronization involves all the modules that may synchronize on the channel. Thus it may introduce deadlock in case one of the involved modules is not ready to participate in the corresponding communication. -Broadcast synchronization involves a sender (identified with an output modality) that synchronizes with all the enabled transitions labeled by an input of the channel.

Example System

We consider a classical rail road example where two tracks are merged into one at a gate section and a controller of this system must ensure that trains arriving from either track will never collide by blocking one of the trains until the other one has passed (cf. Fig. 2). The time for passing the gate would in reality depend on several factors (e.g. length, speed, acceleration/deceleration etc.), but for our simplified example model we consider the amount of wagons the single factor that determines the passing time.

High-Level Graphical Editor Specification

Technically, our solution is realized using the Cinco meta tooling suite [START_REF] Naujokat | Full generation of domain-specific graphical modeling tools: a meta 2 modeling approach[END_REF], a framework based on various libraries from the Eclipse ecosystem [START_REF] Mcaffer | Eclipse Rich Client Platform[END_REF][START_REF] Steinberg | EMF: Eclipse Modeling Framework (2nd Edition)[END_REF][START_REF] Gronback | Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit[END_REF]. Cinco is designed to ease the generation of tailored graphical modeling tools from specifications in terms of metamodels.

Metamodeling is the modern answer to the development of domain-specific tools. However, although popular metamodeling solutions -such as the Eclipse Modeling Framework (EMF) and its multitude of accompanying plug-ins -are quite rich in the provision of code generation and transformation features, it is still tedious to develop sophisticated graphical modeling tools on their basis. The goal of Cinco is to simplify this development by providing means to specify a tool's model structure as well as its graphical user interface (and partly also semantics) in an abstract fashion that suffices to automatically generate the whole corresponding modeling tool.

The key to obtaining this degree of automation is the restriction of EMF's generality to focus on graph-based models consisting of various types of nodes and edges. With this reduction, Cinco follows the "easy for the many, difficult for the few"-paradigm that dictates the bulk of problems to be solvable very easily [START_REF] Margaria | Simplicity as a Driver for Agile Innovation[END_REF]. In our experience, it is surprising how far this paradigm carries and how seldom we need to resort to the difficult for the few part.

At the core of each Cinco product4 lies a file in the Meta Graph Language (MGL) format, which is in fact a domain-specific language for the specification of model types consisting of nodes and edges. 5 type GuardedTransition have several declared attributes that allow to configure their instances. Furthermore, the valid source and target node types are configured for the GuardedTransition. MGL allows arbitrary annotations to be added to the elements, which are interpreted by meta plug-ins during the Cinco tool generation process.

The annotation @style is used to refer to an element from the second core DSL of Cinco: the style definition file. Elaborating on the possibilities to describe the nodes' and edges' visual appearance in the generated editor is beyond the scope of this paper. 6 Just note that it is possible to combine different shapes, colors, line types etc. Beyond this static declaration it is also possible to add dynamic elements. For instance, the contents of attributes can be passed as a parameter to the style (as done with the parameters guard, channel, and number). Those parameters are formulated in the Java Expression Language (EL). They are evaluated at runtime and live updated whenever the attribute values change. Furthermore, it is possible to have arbitrary AppearanceProviders implemented in Java, which we, for instance, use to dynamically show a small arrow tip in the top left corner of a State node's visual representation in case isStartState is true.

Overall, the Cinco PSM tool specification that fully realizes the model and its editor only consists of 84 lines of MGL code, 155 lines of Style code, and 19 lines of Java code. In contrast, the generated Graphiti editor alone7 already consists of over 7,000 lines of code. Of course, generated code tends to be a bit verbose, but it is fair to say that Cinco reduces the amount of code writing by an order of magnitude. Moreover, the required code is much simpler and better structured. In particular it does not require special knowledge about Eclipse and the Graphiti APIs.

Figure 3 shows a screenshot of the generated editor. It consists of some common Eclipse parts (called views), such as the Project Explorer, Miniature View, Console, and Properties. In the center is the main editor area showing the model for our train example. It consists of three Module containers, one for each train and one for the gate. The gray circles are State nodes, of which the one with the arrow tip marker depicts the initial state of the module. The small gray squares represent probabilistic decisions and the blue rectangles are variable assignments. Small circles with different background colors represent clocks, channels, and variables. Variables can either be placed within a module to become local variables, or outside, directly on the diagram canvas to become global variables. Channels are only allowed outside while clocks must be local.

The train model works as follows: in the transition from the initial state 0 to state 1 the train's approach is signaled via channel appr1, the local timer x is reset and the length of the train, here modeled as a random decision, is assigned to the variable l. If the train is signaled to stop within 10 time units, it will go to state 2 and wait for the resume signal on channel go1. Otherwise, it can pass the gate. The second train is modeled analogously. The gate will transition from state 0 to 1 as soon as one of the two trains arrives. If the second train arrives before the first one has left, the local variable wait is set to true. In the waiting state 1, as soon as the first train has left, the go signal is given to the other one, either via state 2 or 4.

Code Generation

So far we have explained how Cinco can be used to easily construct a metamodel and a graphical editor for the PSM superset language. In order to introduce semantics, a code generator needs to be realized, providing a translational semantics for PSM models. In fact, we will have three different code generators, one for each target language.

Cinco comes with a meta plug-in for code generation that interprets a @generate annotation in the MGL file. It generates the required Eclipse code, so that the programmer of the generator does not need to take care of any Eclipse APIs. A Generate button is added to the action bar of the Cinco product that triggers the generation of the currently edited model. The generator realization has to implement a certain interface and is then directly provided with the model, leaving all the Eclipse details transparent to the developer.

Domain-Specific Code Generation

The (main) metamodel of a Cinco product is generated from the MGL specification. This means that we have more precise knowledge on the metamodel's structure than in the standard, purely Ecore-based EMF settings: models always have a graph structure with different node, container and edge types. Thus, the Cinco metamodel generator is directly enabled to generate a library of domainspecific functionality that allows for systematically traversing a given model instance. For example, the following operations are directly supported with a metamodel generated with Cinco:

-Retrieval of successors and predecessors of a given node element. Those specifically generated getters can even be parameterized with a node type to only retrieve successors and predecessors of a given type. -Access to the source and target nodes with correctly typed getters for every edge type. -Type sensitive access to all the inner modeling elements of a container (i.e. nodes or other containers). Please note that these are only some examples and that we constantly enrich the Cinco generator with new domain-specific operations. Of course, similar functionality can also be directly implemented for Ecore metamodels that are not generated with Cinco. However, this would require a lot of tedious code comprising of "instanceof" checks and type casting. In contrast, the Cinco approach allows for the fully automatic generation of this domain-specific functionality.

Within the Cinco approach we provide domain-specific functionality for the development of code generators in a twofold fashion: for Java programmers on the one hand a dedicated API is generated. Technically, this is for the most part realized by generating special EOperations and their according implementations into the metamodel. On the other hand, for domain experts who are not necessarily programmers, we generate the same domain-specific functionalities as modeling components for the jABC process modeling framework [START_REF] Steffen | Model-Driven Development with the jABC[END_REF] (cf. Fig. 4(a)). The resulting Service-Independent Building Blocks (SIBs) can then easily be combined with SIBs for output generation (e.g. for StringTemplate [START_REF] Parr | String Template[END_REF] or Velocity [START_REF]The Apache Software Foundation: Apache Velocity Site[END_REF]; see also [START_REF] Jörges | Construction and Evolution of Code Generators -A Model-Driven and Service-Oriented Approach[END_REF]) into a modeled code generator. Figure 4(b) shows an excerpt from the modeled Prism code generator (cf. upcoming Sec. 4.2) using the generated PSM components as well as some generic components for text generation with StringTemplate (ST on the icon), file I/O, and common tasks such as iterating over elements and error processing. The first model shows the top level of process hierarchy (i.e. the generator root model), while the second one exemplary shows one expanded submodel. While the gain for non-programmers using the jABC is obvious, we think that also people who know programming (which probably can be assumed for developers of modeling tools) strongly benefit from our domain-specific API, as it hides the internal Eclipse structures and is thus also service-oriented in spirit.

Each of the following subsections details on one code generator. As Prism and PLASMA-lab use the same input format, they are treated in one section, followed by the Uppaal generator and the Promela generator. The code generators each assume that certain restrictions apply to the model, as the PSM language allows us to build models none of the code generators can handle anymore. Of course, if a new target platform supports more features included in PSM, they would be easy to capture by a corresponding code generator.

Prism/PLASMA-Lab

The Reactive Module Language (RML) is a textual language based on the Reactive Modules of Alur and Henzinger [START_REF] Alur | Reactive modules[END_REF]. The language has been introduced in the model-checker Prism [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF] and is also used by the statistical model-checker PLASMA-lab [START_REF] Boyer | Plasma-lab: A flexible, distributable statistical model checking library[END_REF]. It describes a set of concurrent components with four different semantics:

1. Discrete time Markov chains (DTMCs).

Continuous time Markov chains (CTMCs). 3. Markov decision processes (MDPs). 4. Probabilistic timed automata (PTAs).

Each semantics imposes some restrictions on the syntax of the language, although the main elements described below are similar. We present briefly the syntax of the language8 and then discuss the generation of RML models from our framework.

In RML each component is modeled as a module that consists of a set of local declarations of integer and Boolean variables, and a set of commands. A command is enabled by a guard and then performs a probability choice among a set of updates. An update consists of a set of assignments that update the values of the variables of the model. Commands can be a assigned to a channel, in which case a global synchronization must be performed between all the modules that communicate with the channel. In CTMCs probability choices are governed by rates according to a race semantics, whereas in DTMCs, MDPs and PTAs only probability values may be used. The sum of the probabilities of a command must then be equal to 1. RML also allows to model PTAs by introducing real-time clocks as a new type of variables and an invariant expression to each module.

To generate a RML model from our framework, each state is assigned to a value of the state variable of the module. Then each meta-transition from a state to a set of states, passing trough assignments and probability node, is translated in a command. In this process assignments that happen before a probability node are copied in each update. This operation is only safe if these assignments prevent any side effects in the value of the probabilities. Finally, if the model is not a CTMC, all the probabilities of leaving a probabilistic decision node are normalized such that in the generated code the sum of the probabilities is always equal to 1. The resulting generator is able to produce valid RML models from our meta-model under the following restrictions:

-Synchronizations are only global.

-Clocks are only used in the PTA model.

-Synchronized transitions only update local variables.

Example 1. From the model presented in Fig. 3 we generate the following RML code:

module Train1 x : clock; l : [0..4] init 0; s : [0..4] init 0; invariant (s=1 => x<=20+l)&(s=3 => x<=15+l)&(s=4 => x<=5+l) endinvariant [appr1] s=0 -> (2)/((2)+(1)):(s'=1)&(x'=0)&(l'=4) + (1)/((2)+(1)):(s'=1)&(x'=0)&(l'=2); [stop1] s=1 & x<=10+l -> (s'=2); [] s=1 & x>=10+l -> (s'=4)&(x'=0); [go1] s=2 -> (s'=3)&(x'=0); [] s=3 & x>=7+l -> (s'=4)&(x'=0); [leave1] s=4 & x>=3+l -> (s'=0); endmodule 4.3 UPPAAL
Uppaal [START_REF] Behrmann | Uppaal 4.0[END_REF] allows us to design timed automata models, possibly extended with variables and stochastic features, and load them from XML files. A model in Uppaal consists of a set of templates, each modeled by a timed automaton. Local and global variables can be integers, Booleans, and clocks. A timed automaton consists of a set of control states, called locations, to which may be assigned an invariant expression and an exponential rate. Uppaal also allows us to use probabilistic decision nodes that are used by the statistical model-checker. Then two types of transitions are possible:

-Transitions between two states, or from a state to a probabilistic decision node, may comprise a guard expression, a synchronization channel and a set of assignments. -Transitions from a probabilistic decision node to a state may comprise a probability weight and a set of assignments.

We can generate Uppaal models in XML format if the following restrictions apply:

-The model is only a PTA.

-Synchronizations are pairwise or broadcast, with input and output modalities.

Example 2. From the model presented in Fig. 3 we generate the Uppaal model of Fig. 5. The semantics of colors in this model are the following: invariants are drawn in purple, guards in green, synchronization in light blue, assignments in blue, probability weights in brown and exponential rates in red.

Promela

Promela (short for Process Meta Language) is the input language for the Spin software model checker [START_REF] Holzmann | The SPIN Model Checker -Primer and Reference Manual[END_REF]. Due to the popularity of Spin, various other tools have been adapted to accept Promela input as well (for instance LTSmin [START_REF] Blom | Ltsmin: Distributed and symbolic reachability[END_REF]), making it an attractive choice especially for the comparison of different model checking tools. The syntax of Promela closely resembles that of the C programming language, augmented by inter-process communication constructs such as buffered or unbuffered channels, atomic sections etc. Moreover, unlike C, Promela allows for non-deterministic choices via statements with non-disjoint guards. A Promela model consists of one or more process types or process behaviors (proctypes), which may be instantiated to form running processes. These processes can communicate via (buffered or unbuffered) channels or shared (global) variables. A process type can be thought of in analogy to a C function that, when instantiated, is executed in parallel with other running processes. Like C functions, process type declarations may be parameterized, with the actual arguments supplied at instantiation time.

While this would theoretically allow for an unbounded number of instantiated processes (technically, the number of simultaneously running processes is limited to 255 in Spin), we do not make use of the possibility of run-time process instantiations: the notion of modules as set out in Sec. 2.2 requires that there exists an a-priori known, fixed set of parallel components (processes). For process type declarations which are used for a single process instance only, Promela provides the active keyword as a prefix to proctype declarations to denote that the corresponding process type is to be instantiated once at the beginning of the program.

Unlike the languages presented in the previous sections, Promela neither supports time nor probabilities. While there do exist extensions for both aspects (Probmela [START_REF] Baier | PROBMELA: A Modeling Language for Communicating Probabilistic Processes[END_REF] for probabilistic processes and RT-Promela [START_REF] Tripakis | Extending PROMELA and SPIN for Real Time[END_REF] for real-time properties), for this case study we chose to focus on the original Promela due to the popularity of the Spin model checker.

In order to generate Promela files, the model has to fulfill the following prerequisites:

no clocks, invariants, or exit rates occur in the model, -synchronizations are pairwise only, with input and output modalities, -each guard only contains either an expression over variables or a synchronization via a specific channel, but not both simultaneously.

The last restriction is due to the fact that in Promela, evaluating the synchronization expression chan ? MSG is not side-effect free, and thus cannot be performed in conjunction with a simple expression such as x >= 10. Note that we do not forbid probabilistic choices in the model. However, as probabilities cannot be expressed in Promela, those will be realized as simple non-deterministic choices.

The translation from an automaton-like structure, as is the modeling formalism for process behavior in our tool, to Promela code can be realized in a fashion similar to that for Prism described in Sec. 4.2: each process has a (local) integer variable indicating the current state of the process, initialized to the value corresponding to the respective initial state. The process body then consists of a do...od block, executing transition statements (assignments, non-deterministic choices, and state changes) according to the current state and satisfied guards. In order to be consistent with the RML notion of updates (cf. Sec. 4.2), each sequence of transition statements is wrapped in an atomic block.

Model-to-Model Transformations

Cinco allows for the easy creation of many different graphical modeling tools. Thus, the so far presented MGL specification of the modeling language PSM can simply be stripped down to the needed parts, fed into the Cinco tool generator, resulting in the automatic creation of a dedicated modeling tool for any language L ⊆ P SM . This could, for instance, result in an LTS modeling tool that only contains states and transitions with channels. In fact, the required changes to the code generators would only be marginal, as one only needs to remove those parts of the generator code that handle the no longer present artifacts, like clocks, assignments, variables etc.

The resulting tools look very similar to the full PSM modeler as presented in Fig. 3. The only immediate difference is that the components palette on the right contains fewer elements and that the elements when configured in the Properties view contain fewer parameters. Even though these differences might look marginal at first sight, they may drastically ease the working with the specialized tools.

However, manually changing the code generators is impractical, especially if extensions to PSM are made that would require all derived code generators to be manually adapted again. Therefore, as already introduced before (cf. also Fig. 1), we use only one code generator base and provide model-to-model (M2M) transformations that translate other model types into PSM. As PSM is designed to provide all the required features, these transformations turn out to essentially be simple injective mappings, which may e.g., require renaming channels into alphabet symbols for labeled transition systems.

Figure 6 illustrates this concept in more detail for labeled transition systems. There exist two different MGL specifications and thus two different metamodels Fig. 6. Multiple products of the PSM family realized as subsets of the full language (PSM.ecore and LTS.ecore) are generated. As explained before, the code generators operate on the PSM metamodel. Thus the domain-specific LTS models need to be transformed into PSM models, a fact which is hidden to the user, who is only confronted with states and transitions.

Of course, the here depicted LTS instance (Trains.lts) does not contain time, probabilities or variables. Thus, the resulting PSM instance (Trains.psm) semantically differs from the one presented in Fig. 3. It just models the gate as a semaphore preventing both trains to enter simultaneously. It can, however, now be translated into all three target languages.

Technically, the realization of the M2M transformations is a special case of the code generator concepts presented in Sec. 4.1. The only difference is that instead of generating the domain-specific library of components for one MGL model, we now have two, and that instead of reading one model type and writing text, we now read one model type and write the other. We are currently investigating ways how these transformations can also be created automatically.

Conclusion

We have presented the PSM case study, a generic conceptual framework to rapidly construct custom graphical interfaces with corresponding code generators for multi-faceted, concurrent systems that is based on the Cinco meta tooling suite. The point of the Cinco project is the explicit support of domainspecificity in order to simplify the tailored tool development. The impact of this approach has been illustrated by generating graphical interfaces for timed automata, probabilistic timed automata, Markov decision processes, and simple labeled transition systems, and the corresponding metamodel-based construction of code generators for Uppaal, Spin, PLASMA-lab, and Prism.

Key to the case study is the development of a 'unifying' super-set parallel systems modeling language (PSM) which serves as a 'mediator' between the multiple 'source' modeling languages and the various targeted input formats for model checking tools. This does not only allow for the generation of the domain-specific tools, but it also provides a means for systematically studying the differences and commonalities of the various system scenarios.

PSM is designed to allow the easy specification of model-to-model transformations from the source models. Moreover, our Eclipse-based framework provides automatically generated domain-specific code that frees the developer of the code generator from dealing with intricate Eclipse APIs. We envision that these features can be combined to further increase the potential of automatic code generation in order to also automatically generate the required model-tomodel transformations into the intermediate PSM language.

Fig. 1 .

 1 Fig. 1. Model-to-code (M2C) generation of multiple model checkers' input formats from one general model type after model-to-model (M2M) transformations on the specialized model types

Fig. 2 .

 2 Fig. 2. Train 2 waiting for Train 1 to pass the gate

  Listing 1.1 shows an excerpt from the PSM.mgl: the specified node type State as well as the edge @style ( state , " $ { number } " ) node State { attr EInt as number attr EBoolean as isStartState attr EString as invariant attr EString as e xp on e nt ia lR a te } @style ( guardedTransition , " $ { guard } " , " $ { channel } " ) edge G u a r d e d T r a n s i t i o n { attr EString as guard attr EString as channel sourceNodes ( State ) targetNodes ( State , Assignment , P r o b a b i l i s t i c D e c i s i o n ) } Listing 1.1. Excerpt from the MGL file

Fig. 3 .

 3 Fig. 3. Screenshot of the generated PSM tool showing the train crossing example

Fig. 4 .

 4 Fig. 4. Excerpts from the modeled Prism code generator with domain-specific component library.

Fig. 5 .

 5 Fig. 5. UPPAAL model of the train

Cinco is developed open source under the Eclipse Public License 1.0. The framework as well as example projects are available at the Cinco website: http://cinco.scce.info

With the term Cinco product (CP) we denote a modeling tool that is developed using Cinco.

This actually makes MGL a meta modeling language or, synonymously, a metametamodel for Cinco products.

Please refer to[START_REF] Kopetzki | Model-based generation of graphical editors on the basis of abstract meta model specifications[END_REF] for a detailed explanation on the Meta Style Language (MSL) and the other possibilities of the GUI generator.

The Ecore metamodel is generated as well, together with the Java code that implements certain EOperations. However, much of the corresponding over 6,000 lines of Java code are generated by the EMF framework without Cinco support.

See http://www.prismmodelchecker.org/ for a more complete description.


Uli Fahrenberg

Mathieu Acher

Axel Legay

Andrzej Wąsowski

Sound Merging and Differencing for Class Diagrams

Class diagrams are among the most popular modeling languages in industrial use. In a model-driven development process, class diagrams evolve, so it is important to be able to assess differences between revisions, as well as to propagate differences using suitable merge operations. Existing differencing and merging methods are mainly syntactic, concentrating on edit operations applied to model elements, or they are based on sampling: enumerating some examples of instances which characterize the difference between two diagrams. This paper presents the first known (to the best of our knowledge) automatic model merging and differencing operators supported by a formal semantic theory guaranteeing that they are semantically sound. All instances of the merge of a model and its difference with another model are automatically instances of the second model. The differences we synthesize are represented using class diagram notation (not edits, or instances), which allows creation of a simple yet flexible algebra for diffing and merging. It also allows presenting changes comprehensively, in a notation already known to users.

Introduction

Model management is an essential activity in a model-driven development process. Numerous tools exist to visualize, validate, transform, refactor, compute differences, or merge models and structured data. The basic management operations can be combined to realize complex maintenance and design tasks. In this paper, we consider merging and differencing of models-two crucial management operations-for class diagrams, the most popular modeling language used in the industry [START_REF] Hutchinson | Empirical assessment of MDE in industry[END_REF]. Class diagrams are used to create domain models, structural system models, and lower level design models. Class diagrams also serve as meta-models, or abstract syntax types, in implementation of domain specific languages (DSLs).

Merging. When a single model is not sufficient to capture all the aspects of a problem or a system, engineers have to merge several models to produce a single integrated model [START_REF] France | Providing support for model composition in metamodels[END_REF][START_REF] Kolovos | Merging models with the epsilon merging language (EML)[END_REF][START_REF] Nejati | Matching and merging of statecharts specifications[END_REF][START_REF] Reddy | Directives for composing aspect-oriented design class models[END_REF][START_REF] Sabetzadeh | Global consistency checking of distributed models with TReMer+[END_REF][START_REF] Xing | UMLDiff: an algorithm for object-oriented design differencing[END_REF]. Model merging also arises when factoring out commonalities of different variant models, e.g., following a product line approach (e.g., see [START_REF] Acher | Composing your compositions of variability models[END_REF][START_REF] Rubin | Combining related products into product lines[END_REF][START_REF] Rubin | Quality of merge-refactorings for product lines[END_REF]). Fig. 1. Two simple class diagrams (above) and their merge (below). Note that the object models of the merge are precisely the ones which model both individual aspects: here, the merge is both sound and complete.

Differencing. Models naturally evolve through editing operations (e.g., adding an inheritance relationship in a class diagram) for refactoring or extending a system. Computing differences of two revised models has applications in comprehension of an evolution, identification of instances not supported by the two models [START_REF]Bibliography on comparison and versioning of software models[END_REF][START_REF] Kolovos | Different models for model matching: An analysis of approaches to support model differencing[END_REF], etc. Merging and differencing operations can be combined when engineers have to propagate differences from one version of the model to another, as in the case of revision control systems.

Key requirements. We highlight two requirements that arise when merging or differencing models. In many engineering scenarios, the result of a merge or difference is subject to analysis: automated tools can ensure that certain instances are still present in the composed diagram; engineers (humans) can visualize the result and therefore understand the evolution of the system. Another important requirement is that the result of a merge (resp. difference) advances the design of a system, so it produces a new model that can later be used in construction. Again, both automated tools and manual activities can operate over this model. For instance, code can be generated from a class diagram; engineers can relate the class diagram to other modeling artefacts or specify a transformation. The two requirements impact the design of merging and differencing operations. First, it is beneficial that a merge (resp. difference) of two class diagrams should be a class diagram-in line with the vision exposed in [START_REF] Fahrenberg | Vision paper: Make a difference! (semantically)[END_REF] that a difference between models should be a model. This allows engineers to visualize the difference and to manipulate it using the usual tools for working with models. Second, merge (resp. difference) operations should be ideally both sound and complete, to enable further precise analysis by automated tools. In particular, an unsound merge operator can authorize objects (instances) actually not conformant to the merged diagrams. Figure 1 introduces a simple example of a merge between two class diagrams. The result (below) is a class diagram, and the merge is both sound and complete. (Note that we assume an open-world semantics, which is consistent with the view semantics used by most modeling tools, i.e. it attempts to compute a minimal model such that the two original models can be derived as its views.)

As further discussed in Sect. 2, existing merging or differencing methods, though extremely useful in practice, do not meet the two requirements. First, syntactic methods suffer from possible lack of soundness, since they do not take the semantics into account. Second, enumerative semantic methods (e.g., [START_REF] Maoz | ADDiff: semantic differencing for activity diagrams[END_REF][START_REF] Maoz | CDDiff: semantic differencing for class diagrams[END_REF][START_REF] Maoz | A manifesto for semantic model differencing[END_REF]) only synthesize a finite set of instance and are thus not complete. In both methods, the result is no longer a class diagram, precluding an algebraic combination of operations or a direct manipulation by tools and engineers.

We follow the methodology presented by us in an earlier work [START_REF] Fahrenberg | Vision paper: Make a difference! (semantically)[END_REF]-we develop the difference operator systematically, via a number of well-defined formal definition steps. We believe that these steps yield a substantial understanding of what the differences between diagrams can be (unlike methods that simply encode a lot of knowledge in a large constraint system solved by an external solver). This knowledge can later be used to advance language design for structural modeling.

The contributions of the paper include:

-A concise formal semantics for the core language of class diagrams (concise and mathematically mature definitions of such are surprising hard to find). The semantics relies purely on set theory, which is crucial for avoiding dependencies on description logics, reasoners and proof systems. -A formalisation of the standard (conjunctive) merge operator used to compute the conjunction of class diagrams (by "putting them on the same page"). To the best of our knowledge, no previous such formalisations exist; using our formalization, we can show that merge is always, automatically, sound. -An intuitive notion of subtyping which is closely related to the merge operator (which is the greatest lower bound for subtyping), and a corresponding notion of a disjunctive merge, which computes disjunctions of class diagrams (and is the lowest upper bound for subtyping). Using our formalization, we show that disjunctive merge is semantically complete. -A compositional algebra for class diagrams: We can show that using only (conjunctive) merge, all class diagrams can be constructed from a few elementary class diagrams. Together with subtyping, this gives an algebra which allows for high-level computations with class diagrams. -A difference operator which computes, in a precise sense, the best possible approximation to an inverse to conjunctive merge. Our difference operator is semantically sound, computable entirely automatically, and produces finite syntactic descriptions of infinite (semantic) differences.

The intended audience are researchers interested in semantics of structural modeling, evolution of meta-models and builders of differencing or merging tools. We proceed by discussing related work in Sect. 2. Section 3 introduces a simple abstract syntax for class diagrams, along with subtyping and compositions. Sect. 4 defines differencing. Both sections work at syntactic level. In Sect. 5, we justify these constructions by showing that they are semantically sound. We introduce a concise, set-based semantics for class diagrams and show that our operators respect it. We conclude in Sect. 6, indicating possible variants and extensions.

Related Work

Our objective is to represent merges and differences of two class diagrams as a class diagram, overcoming limitations of enumerative and syntactical methods in terms of soundness, completeness, and further exploitation by engineers. We achieve this by developing syntactic methods (with sound theoretical basis), which guarantee representation of difference in one description as a diagram.

Limitations of existing syntactic approaches. A syntactic approach to differencing operates purely by manipulating syntactic elements of diagrams, mostly without paying attention whether these manipulations are sound with respect to semantics of the language (for example that they do not ignore some instances).

Syntactic differencing methods are extremely useful in practice, for example, users can visualize a set of syntactic edit operations (e.g., create, modify, delete [START_REF] Alanen | Difference and union of models[END_REF]) and easily understand the evolution of two models. Most of the studies in the field of model differencing (see, e.g., [START_REF]Bibliography on comparison and versioning of software models[END_REF]) present syntactic differencing at either the concrete or the abstract syntax level. However, syntactic methods are inherently incomplete and unsound. They may not be able to expose and represent the semantic (meaningful) differences between two versions of a class diagram. They can also report false positives by operating at the syntactical level. The incompleteness and unsoundness can both disturb automated analysis and a further exploitation by an engineer.

Limitations of enumerative approaches. As argued in some papers and illustrated for some formalisms [START_REF] Acher | Feature model differences[END_REF][START_REF] Brunet | A manifesto for model merging[END_REF][START_REF] Fahrenberg | Vision paper: Make a difference! (semantically)[END_REF][START_REF] Maoz | ADDiff: semantic differencing for activity diagrams[END_REF][START_REF] Maoz | CDDiff: semantic differencing for class diagrams[END_REF][START_REF] Maoz | A manifesto for semantic model differencing[END_REF], models that are syntactically very similar may induce very different semantics, and a list of differences should be best addressed semantically. Recently, semantic approaches have been proposed which enumerate some examples of instances of one model that are not instances of the other [START_REF] Maoz | A manifesto for semantic model differencing[END_REF]. For instance, Maoz et al. tackle the problem of semantic model differencing, specifically for class and activity diagrams [START_REF] Maoz | ADDiff: semantic differencing for activity diagrams[END_REF][START_REF] Maoz | CDDiff: semantic differencing for class diagrams[END_REF]. The cddiff operator for class diagrams [START_REF] Maoz | CDDiff: semantic differencing for class diagrams[END_REF] computes diff witnesses using the Alloy Analyzer, a solver for relational logic with transitive closure. For the addiff operator for activity diagrams, they present algorithms that take as input activity diagrams [START_REF] Maoz | ADDiff: semantic differencing for activity diagrams[END_REF]. The advantage of enumerative methods is that they operate at the semantic level and are sound by construction: no false positives can be reported. However they are clearly incomplete since only a small, finite number of examples can be synthesized. In fact, the set of instances in the difference might well be infinite. A related problem is that engineers cannot visualize and manipulate the (infinite) set of witnesses-a concrete and compact representation is missing. It also precludes an algebraic combination of merging and differencing operations, as in the case of versioning control systems (see Fig. 3, page 10 for more details).

Other approaches and existing tools. Model matching is another important related problem [START_REF]Bibliography on comparison and versioning of software models[END_REF][START_REF] Brunet | A manifesto for model merging[END_REF][START_REF] Euzenat | Ontology matching[END_REF]. Numerous algorithms and techniques are already integrated in model-based tools (e.g., see [START_REF] Kolovos | Different models for model matching: An analysis of approaches to support model differencing[END_REF][START_REF] Nejati | Matching and merging of statecharts specifications[END_REF][START_REF] Sabetzadeh | Global consistency checking of distributed models with TReMer+[END_REF]). For simplicity the theoretical framework we develop assume a basic matching strategy (based on names, see next section). Numerous "diff" or merging tools (e.g., EMF Diff4 , Kompose [START_REF] France | Providing support for model composition in metamodels[END_REF][START_REF] Reddy | Directives for composing aspect-oriented design class models[END_REF], Epsilon [START_REF] Kolovos | Merging models with the epsilon merging language (EML)[END_REF], UMLDiff [START_REF] Xing | UMLDiff: an algorithm for object-oriented design differencing[END_REF], TReMer+ [START_REF] Nejati | Matching and merging of statecharts specifications[END_REF][START_REF] Sabetzadeh | Global consistency checking of distributed models with TReMer+[END_REF], etc.) offer the means to specify user directives (using a specific language or an API). Users can override (customize) the default behaviour of the merging or differencing algorithm and thus handle the semantics of the models. However, the manual specification, if not properly defined, does not guarantee semantic properties and can lead to unsound or incomplete merging (resp. differencing). The objective of the paper is precisely to study the soundness and completeness of operations that can be incorporated into modeling tools. Our approach is both algebraically and semantically justified: to the best of our knowledge, no previous effort guarantees such properties of merging and differencing of class diagrams. Any matching strategy that defines an equivalence on the space of class names could be naturally incorporated in our framework.

Compositional Algebra of Class Diagrams

We start by introducing an abstract syntax for class diagrams. We remark that the operators defined in this section are entirely syntactical; no reference to the semantics of class diagrams is made. The same holds for the properties we expose: they are proven at the syntactic level. In Sect. 5 we will introduce a semantics for class diagrams and show that our operators are semantically sound, but their properties as shown in the present section are completely independent of any semantics one wishes to give to class diagrams.

Let N be the set of all finite unions of finite or unbounded intervals of natural numbers (including the empty set of intervals). N is closed under union, intersection and complementation; let ¬A = ◆\A be the complement of A ∈ N .

Abstract syntax

Let Σ c , Σ a and Σ e be disjoint infinite sets of names, for classes, associations and association ends, respectively. Note that we handle generalizations of both classes and associations; this is common in modern modeling approaches. In the usual concrete syntax of class diagrams, the generalization relation is essentially transitively reduced, but in (iii) we require it to be transitively closed, in order to simplify presentation. Given that the sets of classes and associations are finite, switching between both viewpoints is just a technicality. Another common assumption in class modeling is that two classes which do not share a common subclass are disjoint. This default assumption does not work well with the open-world semantics that we will build up in this paper. It would make the semantics non-monotonic-adding a shared subclass would relax constraints on instances. To prevent this, we prefer to add, in (iv), an explicit representation of binary disjointness constraints in the abstract syntax. Again, switching between explicit and implicit disjointness constraints is just a technicality, but it will allow us to simplify presentation later on. The last condition means that we only consider binary associations. With this in mind, the function aends (vi) maps the two association ends (or, more precisely, their names) of each association to their classes. Similarly, the function acards (vii) associates cardinality constraints to association ends.

As mentioned we will use an open-world semantics, which can be summarized by the slogan that anything which is not forbidden is allowed. So, intuitively, there will be no semantic difference between a class c that does not appear in a given class diagram, and one which does, but has unrestricted cardinality. Formally, we call a class c ∈ cla in some class diagram C restricted if ccard(c) = ◆, and let rcla ⊆ cla denote the subset of restricted classes.

Merge

Ultimately, we want to create class diagrams by composing smaller chunks of them. This reflects the practice of modeling with views, as supported by many modeling tools (for example Eclipse Modeling Framework, Papyrus, or IBM Rational Modeler). Users of such tools work with projections of one large single model represented implicitly in a unified syntax tree. From the users' perspective it may often appear that they work with a number of diagrams that are unified (composed) as if they were put together on the same page, merging entities (e.g., classes) that have the same name. In the following, we propose a conjunctive merge operator, written , that composes two diagrams, as if they were put on the same page, interpreted as views of the same underlying model.

Due to syntactic restrictions, it is not possible for us to merge diagrams that have the same association with different association ends. Since we only allow one name per endpoint in abstract syntax, there is no way to merge different names. This is consistent with the behavior of common modeling tools, where different views of the same association always maintain the same end points. Definition 2. Two class diagrams C 1 , C 2 are said to be composable if it holds for all a ∈ asc 1 ∩ asc 2 that aends 1 (a) = aends 2 (a).

Definition 3. The (conjunctive) merge of two composable class diagrams C 1 , C 2 is C = C 1 C 2 defined as follows: -cla = cla 1 ∪ cla 2 , asc = asc 1 ∪ asc 2 , gen = (gen 1 ∪ gen 2 ) * , disj = disj 1 ∪ disj 2 , -aends = aends 1 ∪ aends 2 , and ccard (c) =      ccard 1 (c) if c ∈ cla 1 \ cla 2 , ccard 2 (c) if c ∈ cla 2 \ cla 1 , ccard 1 (c) ∩ ccard 2 (c) if c ∈ cla 1 ∩ cla 2 , acards (a)(e) =      acards 1 (a)(e) if a ∈ asc 1 \ asc 2 , acards 2 (a)(e) if a ∈ asc 2 \ asc 1 , acards 1 (a)(e) ∩ acards 2 (a)(e) if a ∈ asc 1 ∩ asc 2
for all c ∈ cla , a ∈ asc , and e ∈ dom(aends(a)).

Intuitively, the above merging attempts to approximate conjunction of class diagrams. Due to our open-world semantics ("anything which is not mentioned is unrestricted"), we have to apply a disjunction to the syntactic elements (classes, associations, etc.) to get a conjunctive merge. The merge in Fig. 1 in the introduction gives a simple example of the operation.

Subtyping

With the above definitions we have gathered enough structure to propose a definition of subtyping between two class diagrams:

Definition 4. For class diagrams C 1 , C 2 , we say that C 1 (syntactically) refines C 2 , denoted C 1 ≤ C 2 ,
if all the following conditions hold:

(i) cla 1 ⊇ rcla 2 , asc 1 ⊇ asc 2 (C 1 is an extension of C 2 ) (ii) gen 1 ⊇ gen 2 , disj 1 ⊇ disj 2
(generalization and disjointness constraints are inherited) (iii) ccard 1 (c) ⊆ ccard 2 (c) for all c ∈ rcla 2 (class cardinalities are restricted) (iv) aends 1 (a) = aends 2 (a) for all a ∈ asc 2 (association ends are preserved) (v) acards 1 (a)(e) ⊆ acards 2 (a)(e) for all a ∈ asc 2 and all e ∈ dom(acards 2 (a))

(association cardinalities are restricted)

Due to the open-world semantics, subtyping on syntactic elements becomes reversed subset inclusion. Also, we have to use restricted classes in the inclusion cla 1 ⊇ rcla 2 above; otherwise one could easily find subtypings which were not sound, i.e., where the subtype admits models which the supertype does not. Our selections of subtyping and merging are strongly related, in the sense that is the greatest lower bound for ≤. In practice, this means that the merge does indeed "behave like a conjunction".

Theorem 1. For all class diagrams C 1 , C 2 , D with C 1 and C 2 composable, D ≤ C 1 C 2 iff D ≤ C 1 and D ≤ C 2 .
We believe that this compatibility of subtyping and merging is of fundamental importance. Subtyping captures the intuitive notion of constraining the set of instances during modeling. A merge operator considered without subtyping can create merges that admit far fewer, or many more, instances than the user would expect. Introducing the above subtyping preorder on diagrams will later allow us to follow the method presented in [START_REF] Fahrenberg | Vision paper: Make a difference! (semantically)[END_REF] for defining differences. Intuitively, we need an order because notions of difference, distance and order are intimately related. It is surprising that so few works on merging and differencing structural models consider subtypes or other orderings (unlike for behavioral models, e.g. [START_REF] Brunet | Properties of behavioural model merging[END_REF]).

Theorem 1 immediately entails that the merge operator has the core properties expected of composition, viz. commutativity and associativity. Also, merge is monotonic with respect to the subtyping order, or, in other words, subtyping is compositional. This is a highly desirable property that introduces some regularity in the framework.

Class Diagram Algebra

Compositionality allows us to develop an algebra for class diagrams, using a few elementary diagrams and the composition operator . What we obtain is a small structural modeling calculus that is of interest by itself -class diagrams can be written concisely, in a manner that is friendly to a linear mathematically oriented text, unlike the concrete syntax representation of class diagrams, and unlike the rather unwieldy abstract syntax presented in Def. 1.

The calculus is built around a set of elementary class diagrams which are merged to obtain bigger structures. The elementary diagrams are as follows: ∅,∅,∅,∅,∅,∅ -

-⊤ = (∅,
c 1 , 2 c 2 , for c 1 , c 2 ∈ Σ c : the class diagram with cla = {c 1 , c 2 }, asc = ∅, gen = {(c 1 , c 1 ), (c 2 , c 2 ), (c 1 , c 2 )}, disj = ∅, ccard(c 1 ) = ccard(c 2 ) = ◆, and
aends = acards = ∅; -c 1 // c 2 , for c 1 , c 2 ∈ Σ c : the class diagram with cla = {c 1 , c 2 }, asc = ∅, gen = {(c 1 , c 1 ), (c 2 , c 2 )}, disj = {(c 1 , c 2 ), (c 2 , c 1 )}, ccard(c 1 ) = ccard(c 2 ) = ◆,
and aends = acards = ∅.

However simple, the above language of class diagrams is quite powerful-it is fully expressive in the sense that it can express every finite diagram as a finite composition; see also Fig. 2 for an example: Theorem 3. Every class diagram can be written as a finite conjunctive merge of elementary class diagrams.

Difference and Disjunctive Merge

We enrich our algebra with two more operators, difference and disjunctive merge. The difference operator, which is a formal adjoint to the conjunctive merge, will have the property that merging a class diagram C 1 with a difference C 2 C 1 is semantically sound, i.e., the composition C 1 (C 2 C 1 ) is a subtyping of C 2 . Later this will translate to a perhaps more intuitive semantic property that the difference does not admit too many instances; adding them to instances of diagram C 1 still obeys the constraints of C 2 . aends = aends 2 \ aends 1 , and Let us give some intuition about the rather complicated formula for gen : Like ordinary set difference, e.g. in asc = asc 2 \ asc 1 , is an adjoint to set union, what is on the right-hand side of the gen formula is an adjoint to transitive union of transitive relations. That is, gen is the smallest transitive relation for which (gen ∪ gen 1 ) * ⊇ gen 2 . The next theorem states the fundamental property of the difference operator.

Definition 5. The difference of two composable class diagrams

C 1 , C 2 is C = C 2 C 1 defined as follows: -cla = cla 2 , asc = asc 2 \ asc 1 , disj = disj 2 \ disj 1 , and gen = {r ⊆ cla 2 × cla 2 | (gen 1 ∪ r) * ⊇ gen 2 } * , C ≤ D D ′ D / / D ′ D o o C (D ′ D) ≤ D ′
ccard (c) = ccard 2 (c) if c / ∈ cla 1 , ccard 2 (c) ∪ ¬ccard 1 (c) otherwise,
Theorem 4. For all class diagrams C 1 , C 2 , C 3 , C 1 C 2 ≤ C 3 iff C 1 ≤ C 3 C 2 .
This means that C 3 C 2 is the most permissive class diagram for which (C 3 C 2 ) C 2 ≤ C 3 still holds; in that sense, is the natural diff operator induced by . In this sense, is the most precise difference operator which can be soundly represented using the class diagram syntax defined in this paper. Since the language elements that we omit do not deal with restricting those that we include, there is no hope that using a richer selection of language elements from the standard set can lead to a better operator. One could, instead, resort to using Object Constraint Language to obtain more precise differencing.

E ◆ T ◆ M ◆ E {1} ◆ T E ms mB ◆ {0,1} M E // T M // T
Fig. 4. A disjunctive merge of two diagrams (top) presented in concrete syntax (bottom left) and as a composition of elementary diagrams (bottom right). The overlap between "Manager" and "Employee" seen in the abstract syntax to the right (no disjointness constraint) is not visible in the concrete syntax on the left.

The classes can overlap due to the generalization in the rightmost input diagram.

We turn now to another kind of merge operator that can also be induced by subtyping: a "merge in union mode", the least upper bound for subtyping: for all c ∈ cla , a ∈ asc , and e ∈ dom(aends(a)).

Definition 6. The disjunctive merge of two composable class diagrams C 1 , C 2 is C = C 1 C 2 defined as follows: cla = cla 1 ∩ cla 2 , asc = asc 1 ∩ asc 2 , gen = gen 1 ∩ gen 2 disj = disj 1 ∩ disj 2 , ccard (c) = ccard 1 (c) ∪ ccard 2 (c) aends = aends 1 ∩ aends 2 , acards (a)
Note the "contravariance" again: disjunctive merge becomes a conjunction of syntactic elements. As expected, is least upper bound for ≤:

Theorem 5. For all class diagrams C 1 , C 2 , D with C 1 and C 2 composable, C 1 C 2 ≤ D iff C 1 ≤ D and C 2 ≤ D.
Example 2. Figure 4 shows two variants of the simple class diagram from Fig. 2 together with their disjunctive merge. We see that extracts precisely the common features of the two diagrams. Hence disjunctive merge can be used for factoring out common features in diagrams.

⊓ ⊔

Semantic Soundness

In this section we give a precise semantics to class diagrams and use this to show that our constructions of subtyping ≤, composition , and difference (object types are consistent with generalizations) 3. For all ℓ ∈ lnk and all a, a ′ ∈ asc with Lty(ℓ, a) and gen(a, a ′ ), also Lty(ℓ, a ′ ) (link types are consistent with generalizations) 4. For all ℓ ∈ lnk and all a ∈ asc with Oty(ℓ, a), dom(lends(ℓ)) = dom(aends(a))

(link endpoints inherit their names from their type) 5. For all ℓ ∈ lnk and all a ∈ asc with Lty(ℓ, a), it holds for all e ∈ dom(lends(ℓ))

that Oty(lends(ℓ)(e), aends(a)(e)) The first, and most important, theorem in this section shows that subtyping is semantically sound. The proof is basically a careful inspection of the conditions for subtyping and implementation.

(
Theorem 6. For all class diagrams C 1 , C 2 , C 1 ≤ C 2 implies C 1 ⊆ C 2 .
We sum up the semantic properties of our operators; all follow easily from their syntactic properties and Theorem 6. Note that and are semantically sound, i.e., under-approximations, whereas is semantically complete.

Theorem 7. For all pairs of class diagrams C 1 , C 2 : C 1 C 2 ⊆ C 1 ∩ C 2 , C 1 (C 2 C 1 ) ⊆ C 2 , and C 1 C 2 ⊇ C 1 ∪ C 2
Intuitively, Thm. 7 states that our operators behave as expected not only with respect to the syntactic subtyping, as shown in Sections 3-4, but also with respect to the semantics (our ultimate goal). Crucially, Thm. 7 follows almost directly from the theorems of those sections, once we have Thm. 6. So the main work required to transfer the results of this paper to another semantic variation for class diagrams, is to obtain the equivalent of Thm. 6 for the new semantics.

Using simple examples, we can show that subtyping and composition are not semantically complete. For subtyping, we use inconsistency:

Let C 1 = A ∅ and C 2 = B ∅ . Then C 1 = C 2 = ∅, but C 1 ≤ C 2 , because C 2 contains a restricted class which is not in C 1 ; for the same reason, C 2 ≤ C 1 .
This also exposes the fact that ≤ does not have a unique bottom element; there is no class diagram B such that B ≤ C for all class diagrams C.

For incompleteness of composition, we observe that generalizations can implicitly force object typing in one diagram which is forbidden in another: Let

C 1 = A , 2 B , C 2 = B 1 , then C 1 C 2 = A , 2

Conclusion and Final Remarks

We have presented a compositional algebra of class diagrams with subtyping, conjunctive and disjunctive merge and difference. All operators are described by means of manipulations of minimal syntactic elements of the diagrams, which are also basic terms of our class diagram algebra. To the best of our knowledge, this is the first attempt to define these syntactic operations in a provably sound manner. The operations are all efficiently computable and thus can be automated. The results of operations are represented in the syntax of the input language (they are class diagrams themselves), so that they can later be further processed using regular tooling for class diagrams.

We have worked with a simple core part of the class diagram language, which has allowed us to include all the technical constructions in the paper. Some extensions to other language elements are straightforward, some others require more extensive work. From the point of view of differencing, treating attributes is relatively simple, e.g. by boxing these as classes and treat them in the same way as classes. This is somewhat unsatisfactory though, as treating attributes specially would allow presenting the differences in a more concise and clear manner. Operations would require also computing differences between their signatures-we have decided not to discuss this, as it is not specific to structural modeling, but can be done using techniques for textual programming languages. To handle n-ary associations, one could introduce association classes and treat them in the same way as we treat regular classes. Allowing association classes to be evolved into regular classes (and vice-versa) would require more extensive changes though. Handling abstract classes is not much different from handling concrete ones, and the same goes for directed associations (vs. undirected ones). However, computing differences between diagrams where classes are changed from concrete to abstract, or associations from directed to undirected, or where association endpoints are moved, seems more challenging. Finally, note that we have used element identities to match them for the purpose of merging and differencing. Clearly, in a real application one should use an externally computed mapping, using for instance existing matching heuristics.

We have chosen to work with sound approximations for simplicity and clarity. Experience with building theories for behavioral models shows that a search for precise (i.e., both sound and complete) refinements and compositions leads to complex constructions with high computational complexity [START_REF] Antonik | EXPTIMEcomplete decision problems for modal and mixed specifications[END_REF][START_REF] Beneš | EXPTIME-completeness of thorough refinement on modal transition systems[END_REF], so it should only be done once the overall structure and properties of the design space are well understood on simpler cases. We speculate that more precise operators could be expressed in our algebra if we had a complementation for class diagrams. Unfortunately, in our current framework, complements of class diagrams will need infinitely many classes, hence are outside the syntax. Alternatively, to overcome the limitations of the class diagram notation, one can consider using Object Constraint Language to specify more precise differences and merges. We intend to investigate these possibilities in future work.

We remark that the semantics we give to class diagrams in this paper is only one out of a plethora of different existing class diagram semantics which are being used, c.f. [START_REF] Maoz | Semantically configurable consistency analysis for class and object diagrams[END_REF]. We have shown that our constructions are semantically sound for our particular semantics, but this soundness may break if other semantics are used. However, to check that the constructions are sound, one only needs to see that subtyping is semantically sound, i.e. that the semantics is monotonic with respect to subtyping; if this is in place, then all other semantic properties follow. Hence our work lends itself easily to different semantics configurations [START_REF] Maoz | Semantically configurable consistency analysis for class and object diagrams[END_REF], a point we intend to elaborate in the future. The work reported here is part of a larger project on model management. Our long term objective is to develop semantically sound (and reasonably complete) model management operations for other formalisms, beyond class diagrams and feature models [START_REF] Acher | Composing your compositions of variability models[END_REF][START_REF] Acher | Feature model differences[END_REF][START_REF] Fahrenberg | Vision paper: Make a difference! (semantically)[END_REF].

Definition 1 .

 1 A class diagram is a tuple C = (cla, asc, gen, disj, ccard, aends, acards) consisting of (i) A finite set cla ⊆ Σ c of classes, (ii) A finite set asc ⊆ Σ a of associations, (iii) A reflexive transitive relation gen ⊆ cla × cla ∪ asc × asc capturing generalizations between classes and between associations, (iv) An irreflexive symmetric relation disj ⊆ cla × cla representing class disjointness constraints, (v) A mapping ccard : cla → N encoding class cardinality constraints, (vi) A partial function aends : asc → Σ e ⇀ cla mapping each association to its endpoints, and (vii) A partial function acards : asc → Σ e ⇀ N mapping each association to its endpoint cardinality constraints. Also |dom(aends(a))| = 2 and dom(acards(a)) = dom(aends(a)) for all a ∈ asc.

Theorem 2 .

 2 The operator is commutative and associative, and for all class diagrams C 1 , C 2 , D 2 , D 2 with C 1 and D 1 composable and C 2 and D 2 composable, C 1 ≤ C 2 and D 1 ≤ D 2 imply C 1 D 1 ≤ C 2 D 2 .

c 2 ,Fig. 2 .

 22 Fig. 2. The five types of elementary class diagrams (above), a simple class diagram in concrete syntax (below left), and its decomposition into elementary class diagrams (below right, where we have abbreviated names).

Fig. 3 .

 3 Fig. 3. Use of difference for automatic evolving of subtypes: If C is a subtype of D, then C merged with the difference D ′ D is a subtype of D ′ .

  acards (a)(e) = acards 2 (a)(e) if a / ∈ asc 1 , acards 2 (a)(e) ∪ ¬acards 1 (a)(e) otherwise for all c ∈ cla , a ∈ asc , and e ∈ dom(aends(a)).

Example 1 .

 1 Consider a situation as presented in Fig. 3. We have a class diagram C which is a subtype of another, D. Now the diagram D is evolved, e.g. by adding more classes or streamlining its associations, into a new class diagram, D ′ . Our abstract properties of composition and difference now ensure that C can be evolved to a subtyping of D ′ , automatically, by merging it with D ′ D: C (D ′ D) ≤ D (D ′ D) ≤ D ′

  (e) = acards 1 (a)(e) ∪ acards 2 (a)(e)

Definition 7 .Definition 8 .

 78 are semantically sound. That is, subtypings of a class diagram C have fewer implementations than C, the implementations of a merge C D are all also implementations of both C and D, and the implementations of a difference D C merged with C are also implementations of D. The semantics of a class diagram is given by a set of instance diagrams, or object models, which implement the class diagram. An instance diagram essentially consists of objects and links which are typed by classes and associations: An instance diagram is a tuple M = (obj, lnk, oty, lty, lends) of -A finite set obj of objects, -A finite set lnk of links, -A total relation oty ⊆ obj × Σ c associating objects with their object types, -A total relation lty ⊆ lnk × Σ a associating links with their link types, -A partial function lends : lnk → Σ e ⇀ obj mapping each link to its endpoints. We require that |dom(lends(ℓ))| = 2 for each ℓ ∈ lnk. We use the common notation "a : A" for object and link typing, instead of the more cumbersome "(a, A)". An object type relation specifying one object a of type A and another, b, of type B, will thus be denoted by oty = {a : A, b : B}. An instance model M is said to implement a class diagram C, denoted M |= C, if there exist extended typing relations Oty ⊇ oty, Lty ⊇ lty such that the following hold: 1. |{o ∈ obj | Oty(o, c)}| ∈ ccard(c) for all c ∈ cla (class cardinalities are respected) 2. For all o ∈ obj and all c, c ′ ∈ cla with Oty(o, c) and gen(c, c ′ ), also Oty(o, c ′ )

  link endpoints are well-typed) 6. For all o ∈ obj, a ∈ asc and e ∈ dom(aends(a)) with Oty(o, aends(a)(e)), we have |{ℓ ∈ lnk | Lty(ℓ, a) & lends(ℓ)(e) = o}| ∈ acards(a)(e) (association end cardinalities are respected) 7. There are no o ∈ obj, c, c ′ ∈ cla for which disj(c, c ′ ), Oty(o, c) and Oty(o, c ′ ) (disjointness constraints are respected) The set of implementations of C is C = {M | M |= C}.

B 1 .

 1 Now let M = {a : A, b : B}, the instance model with one object a of type A and another, b, of type B. Then M |= C 1 , as witnessed by the extended object typing Oty 1 = {a : A, a : B, b : B}, and M |= C 2 , witness by Oty 2 = oty M = {a : A, b : B}. However, M |= C 1 C 2 , as any witness to this would have to include the typing {a : A, a : B, b : B} with two objects of type B.

http://eclipse.org/diffmerge/

⋆ Supported by The Danish Council for Independent Research under Sapere Aude project VARIETE