Tewfik Ziadi
email: tewfik.ziadi@lip6.fr

Jean-Marc Jezequel
email: jezequel@irisa.fr

PLiBS: an Eclipse-based tool for Software Product Line Behavior Engineering

Keywords: Software product line, variability, sequence diagrams, state machines, synthesis

This paper presents the PLiBS (Product Line Behavior Synthesis), an Eclipse-based tool for modeling and deriving behavior aspects in Software Product Lines (SPL). PLiBS allows specifying SPL behaviors using UML2 sequence diagrams extended by variability mechanisms. PLiBS implements a two-step approach to derive product behaviors. The first one uses model transformation to specialize sequence diagrams. While the second one uses UML state machines synthesis from sequence diagrams. This paper presents a guided tour around PLiBS. It presents its architecture and its main components. It also illustrates its uses on the Banking Product Line example.

INTRODUCTION

Software Products Lines (SPL) aim at decreasing development costs and times by developing a family of systems instead than one system at a time. Rather than describing a single software system, the model of a software product line describes the set of products in the same domain. This is done by distinguishing elements shared by all the products of the line, and elements that may vary from one product to another. Concepts of commonality and variability are respectively used to designate common and variable elements in a product line [START_REF] Weiss | Software Product-Line Engineering: A Family Based Software Development Process[END_REF]. Beyond variability modeling, the product derivation process is defined as a complete process of constructing products from the software product line [START_REF]Message sequence charts (MSC)[END_REF].

While many works have investigated the modeling and derivation of functional [START_REF] Bertolino | Use Case Description of Requirements for Product Lines[END_REF][START_REF] Halmans | Communicating the variability of a software-product family to cutomers[END_REF][START_REF] John | Tailoring Use Cases for Product Line Modeling[END_REF][START_REF] Robak | Extending the UML for modeling variability for system families[END_REF] and static [START_REF] Clauß | Generic modeling using UML extensions for variability[END_REF][START_REF] Kaim | Managing variability in the LCAT SPLIT/Daisy[END_REF][START_REF] Webber | The Variation Point Model For Software Product Lines[END_REF] aspects of SPL, there is few research on supporting behavior modeling of SPL [START_REF] Bass | Software Architecture in Practices[END_REF][START_REF] Flege | System Family Architecture Description Using the UML[END_REF][START_REF] Gomaa | Object Oriented Analysis and Modeling for Families of Systems with UML[END_REF][START_REF] Robak | Extending the UML for modeling variability for system families[END_REF] and none for related product.

Behavior modeling plays an important role in the traditional engineering of software-based systems; it is the basis for systematic approaches to requirement captures, design, simulation, code generation, testing and verification. Two complementary formalisms for modeling behavior have proven useful in practice: interaction-based (focusing on the global interactions between actors and components, eg.; UML2 sequence diagrams) and state-based modeling (concentrating on internal states of individual components, e.g.; UML2 state machines). In the context of the Families project [START_REF]FAMILIES project[END_REF], we have implemented an Eclipse-based tool, called PLiBS (Product Line Behavior Synthesis) for SPL behavior engineering.

The approach implemented in PLiBS is based on these two formalisms. UML2 sequence diagrams are firstly used to model SPL behaviors. While UML state-machines represent the results of the PLiBS derivation process.

The rest of the paper is organized as follows: Section 2 summarizes the approach that PLiBS implements. Section 3 presents the PLiBS architecture and its main components. Section 4 illustrates the use of PLiBS on the Banking Product Line example. Finally Section 6 concludes this work and dresses some perspectives.

THE APPROACH

It's admitted in the literature that software product line engineering defines two mains levels: 'Product Line' and 'Single Product'. At the first one, the architecture of the SPL is defined and the variability is explicitly specified. At the second one, the specified variability is resolved and the SPL architecture is specialized to obtain product-specific architectures.

The approach implemented in the PLiBS tool (cf. Figure 1) uses this level duality to model the behavior aspect of SPL architecture. Behavior modeling plays an important role in the traditional engineering of single software-based systems; it is the basis for systematic approaches to requirement captures, design, simulation, code generation, testing and verification. Two complementary formalisms for modeling behaviors have proven useful in practice: interaction-based (focusing on the global interactions between actors and components, eg.; UML2 sequence diagrams) and state-based modeling (concentrating on internal states of individual components, e.g.; UML2 state machines). Our approach is based on these two formalisms. UML2 sequence diagrams are used at the "Product Line" level to model SPL behaviors. While UML state-machines represent the results of our process derivation; they specify the product-specific behaviors. Our initial objective in this paper is to present the tool that implements the approach and not the approach itself. The approach is previously published in [22]. So in this section we only summarize main steps of our approach. We firstly describe how UML2 sequence diagrams are used to model SPL behaviors. Then we show how product-specific UML statemachines are derived.

Modeling Software Product Line Behavior

Our approach uses UML2 sequence diagrams. UML2 mainly improves UML1.x sequence diagrams in by the introduction of interaction operators to compose sequence diagrams. Seq (for sequence composition), alt(for alternative composition), and loop (for the iteration of a SD) are examples of the UML2 interaction operators. The SPL behavior is specified in our approach as a collection of basic SD describing basic behaviors that concern all the product line and one combined SD. A combined SD is the name used within UML2 to call composed SD. It refers to a collection of basic SD and composes them using interaction operators.

To be useful in the SPL context, sequence diagrams should allow the expression of variability. As shown in [START_REF] Ziadi | Towards a UML profile for software product lines[END_REF], variability can be introduced in UML2 combined SD using UML extension mechanisms such as stereotypes and tagued values. This includes three mechanisms: optionality, variation and virtuality. Optionality of a SD means that this SD can be omitted in some products. Variation means that the SD defines a set of SD variants and each product should choose one and only one SD variant. Virtuality is inspired by an existing mechanism in MSC [START_REF]Message sequence charts (MSC)[END_REF]. The virtual SD will be replaced by another SD of refinement. Each product defines its SD refinement. The complete formalization of these mechanisms on the UML2 meta-model can be found in [START_REF] Ziadi | Towards a UML profile for software product lines[END_REF].

Our manipulation of SPL sequence diagrams is based on an algebraic framework for UML2 sequence diagrams [22]. Each UML combined sequence diagram is algebraically formalized as a RESD (Reference Expression for Sequence Diagrams). RESD is an expression where terms are references for basic SD and operators are SD operators (seq, alt, and loop). PL combined sequence diagram is formalized as a PL-RESD (Product Line-RESD). PL-RESD extends RESD by the introduced variability construction (optional, variation, and virtual). In what follows, we only present definitions of RESD and PL-RESD. Section 5 illustrates them on a concrete example.

Definition 1. A reference expression for sequence diagrams (noted RESD hereafter) is an expression of the form:

<RESD>::=<PRIMARY> ( "alt" <RESD> | "seq" <RESD>)* <PRIMARY>::=EØ | <IDENTIFIER> | "("<RESD>")" "loop" "(" <RESD> ")" <IDENTIFIER>::= (["a"-"z","A"-"Z"]| ["0"-"9"])* seq, alt and loop are the SD operators mentioned above. EØ is the empty expression that defines a sequence diagram without interaction.

Definition 2. A reference expression for PL-sequence diagrams (noted PL-RESD hereafter) is an expression of the form:

<PL-RESD>::=<PRIMARY-PL>("alt" <PL-RESD> | "seq" <PL-RESD>)* <PL-PRIMARY>::= EØ |<IDENTIFIER> | "("<PL-RESD>")" | "loop" "(" <RESD-PL> ")" | "optional" <IDENTIFIER> "[" <RESD> "]" | "variation" <IDENTIFIER> "[" <RESD> ","( <RESD>)* "]" | "virtual" <IDENTIFIER> "[" <RESD> "]" optional, variation and virtual are constructions that correspond to the three variability mechanisms introduced above.

Deriving Product-Specific Behavior

Deriving product-specific behaviors is realized within PLiBS in two steps. First, variability is resolved by deriving the PL-RESD into a set of RESD, one for each product. Then state machines are generated by transforming product sequence diagrams given as an RESD into a composition of UML2 state machines.

PLiBS process 1:

The first PLiBS process (cf. Figure 1) consists in generating the combined sequence diagram, in the form of an RESD, of each product from the PL-RESD. As mentioned previously, the PL-RESD is defined by a set of variability constructions. To derive a product-specific RESD, some decisions (or choices) associated with these variation points are needed. For example, each product should choose among the presence or not of all optional SD. A mechanism is needed to capture decisions that are made for a specific product. In our approach, we call this mechanism Instance Decision Model(IDM). Each IDM captures decision resolutions for one product.

Definition 2. An Instance of Decision Model (noted hereafter IDM) for a product P is a set of pairs (namei, Res), namei designates a name of an optional, variation or virtual part in the PL-RESD and Res is its decision resolution related to the product P. Decision resolutions are defined as follows:

o The resolution of an optional part is either TRUE or FALSE.

o For a variation part with E1, E2,E3.

. as expression variants, the resolution is i if Ei is the selected expression. o The resolution of a virtual part is a refinement expression E.

The first step is formalized through abstract interpretation of a generic SPL expression in the IDMi context, where IDMi is the Instance of Decision Model related to a specific product:

E Product = [ ] [ ] E SPL IDM
Interpretation of the E SPL is based on the interpretation of each variability mechanism. Interpreting an optional expression for example, means deciding on its presence or absence in the product-specific expression E Product . This can be formalized as follows:

[ ] [ ] E] [ name optional IDMi =

PLiBS process 2 :

The obtained product expressions from PLiBS process 1 are expressions without variability, i.e. expressions that only compose basic SDs by interaction operators: alt, seq, and loop. The second PLiBS process (cf. Figure 1) of our derivation approach aims at generating UML2 state machines for objects in each derived product. State machines synthesis out of a collection of sequence diagrams has received a lot of attention in the context of single product development. This allows fostering a better traceability between the requirements (depicted by sequence diagrams) and detailed design (depicted by state machines). In our approach, product sequence diagrams are translated into state machines using the method that we proposed in [START_REF] Ziadi | Revisiting statecharts synthesis with an algebraic approach[END_REF]. Our synthesis method generates state machines from all basic sequence diagrams in the product line and then composes them to obtain a full state machine for each object. To realize this composition, our method formalized three state machines operators (for sequence, alternative, and iteration composition). The composition is then defined using a correspondence between interaction operators and state machine operators. For example, if two basic SD are sequentially composed in the RESD, so the two generated state machines from these two basic SD are sequentially composed to obtain the full state machine. Interested readers can refer to [START_REF] Ziadi | Revisiting statecharts synthesis with an algebraic approach[END_REF] for a full description of our synthesis method.

THE PLiBS TOOL

PLiBS (Product Line Behavior Synthesis) is an Eclipse-based tool that implements the approach presented in Section 2. PLiBS is entirely implemented in Java and it uses the EclipseUML tool [START_REF]EclipseUML tool home[END_REF]: a UML tool integrated in the Eclipse platform. The EclipseUML tool is firstly used within PLiBS to specify PL UML2 sequence diagrams and secondly to display the produced UML2 state machines. This Section presents our extensions to

E if (name,TRUE) ∈ IDMi EØ if (name,FALSE)∈ IDMi
the EclipseUML to specify PL sequence diagrams, describes the PLiBS architecture and its main components. It finally discusses the implementation choices we made.

PL Sequence diagrams specification

Using PLiBS, PL sequence diagrams are specified using the EclipseUML tool [START_REF]EclipseUML tool home[END_REF]. Unfortunately, this tool only allows specifying basic sequence diagrams (see Figure 2) and no means to specify combined SD (i.e.; SD with interaction operators). To go beyond this limit, we propose a set of conventions to specify in the EclipseUML tool the main concepts of combined SD. This includes conventions to specify references to basic SD, interaction operators (sequence, alternative, and loop), and variability in PL SD.

Reference (ref)

Refence A combined SD in the PLiBS is specified as an EclipseUML SD including references. Reference to a basic SD is made by a "self message" event coupled with a note containing the name of the referenced basic SD. Figure 5 shows an example of a combined SD with a set of references. The self message and the note containing the name "Deposit" for example specifies that this combined SD refers to a SD called "Deposit".

Sequence (seq)

The sequence between basic SD is implicitly specified by the order of appearance of these basic SD references. In the combined SD of Figure 5, the basic SD Deposit is referenced before the SD CreateAccount. This is equivalent to the expression Deposit seq CreateAccount.

Alternative (alt)

The EclipseUML tool introduces a "switch" mechanism that can be specified on the lifeline of objects in sequence diagrams. We propose to reuse this mechanism to specify the alt operator, each "case" sub-statement represent a particular operand of the alt operator. In Figure 3. three operands are given for the alternative node. In each operand, a reference to a basic SD can be added (see Figure 5.)

• Loop

The loop operator is introduced by a "do…while" or a "while" statement as shown below (see Figure 4)

Variability

As presented in Section 2, our extensions of UML2 sequence diagrams for variability, includes three mechanisms: optionality of interactions, variation and virtuality. Within the PLiBS tool, we propose three new keywords, one for each variability mechanism, which are displayed in UML notes associated with references in a PL combined SD. A reference to an optional sequence diagram is introduced with the optional keyword and the name of the SD follows between square brackets (see Figure 5). Variant SD references are introduced with the variation keyword. All variants appear between square brackets, each SD name separated by a comma. A virtual basic SD is specified in the same way as for optional SD (we only replace optional keyword by the virtual one). The combined SD of Figure 5 illustrates the specification of optionality. The SD SetLimit is optional; this is specified in the note associated with the SD SetLimit by the expression:

optional settingLimit [SetLimit].

PLiBS architecture

Figure 6 shows the overall architecture of PLiBS. This includes six components:

PL-RESD parser. Is a parser for PL-RESD. The PL-RESD syntax is presented is Section 2.

Basic SD parser. Is a parser for basic sequence diagram syntax (the syntax used within PLiBS to describe basic SD is close to the MSC specification [START_REF]Message sequence charts (MSC)[END_REF]).

Main Components

There are two main components implementing the core functionalities in the PLiBS tool. The AE Derivation and the UML2 state machine synthesis components. Next paragraphs present these two components.

Algebraic Expression Derivation component

Description: This component uses a kind of a rewrite mechanism to implement the derivation of PL Algebraic Expression (AE). Based on instance decision models, the PL-RESD is specialized to obtain product-specific expressions. The component displays the PL-RESD obtained from the EclipseUML-PLiBS Interface component (see Figure 7). For decisions on variability, the AE derivation component displays to the user a UI that describes all variation points and their possible decisions. The user uses this UI to define here decision model instance.

UML2 state machine synthesis

Description: This component implements the PLiBS process 2 presented in Section 2. It implements the algorithm that generates UML2 state machines from basic sequence diagrams as formalized in [START_REF] Ziadi | Revisiting statecharts synthesis with an algebraic approach[END_REF]. It also implements state machines operator in order to obtain the full state machines [START_REF] Ziadi | Revisiting statecharts synthesis with an algebraic approach[END_REF]. Figure 9 shows the UI associated with this component. In the first panel, it displays the product-specific expression obtained from the AE Derivation component. The second panel contains the specification of all basic SD. The component generates the full state machine specifying the complete behavior of the selected object in the context of the product.

INPUT: the product-specific RESD, a specification of all basic SD.

OUTPUT: a UML2 state machine for each object participating in one or more basic SD.

Discussion

The architectural choices that we made to implement PLiBS give two main advantages. First, the two components implementing the PLiBS core functionalities are independents from the EclipseUML tool. This facilitates integrating new UML tools. It is only sufficient to develop the component interface associated with the new UML tool. Second, the separation between PL expression derivation and UML2 state machines processes allows using PLiBS in the context of the single product development. In this context, the user only uses the UML2 state machine synthesis component.

Beyond implementing the main aspects of our approach, PLiBS lacks of PL constraints checking. Indeed, in addition to variability, the PL architecture is defined with a set of constraints. PL constrains mainly specify dependencies between variation points (requires or mutual exclusion are examples of these constraints). In [22], we formalized PL contrains as OCL meta-level constraints. In the future it will be interested that PLiBS allow specifying and checking this kind of constraints. This can be realized by integrating in the PLiBS tool a checker of OCL meta-level constraints. The basic SD Deposit for example is SD to deposit an amount on a specific account. Figure 2 shows the specification of this basic SD.

ILLUSTRATION: THE BANKING SPL

The E BPL illustrates two variability mechanisms: optionality and variation.

• Since some products of the BPL do not support overdrawing, optionality is added to the basic SD SetLimit (SetLimit is the basic SD that specifies the interactions between object for adding limits on account). In addition, since exchange calculation is an optional functionality in the BPL, basic SD SetCurrency (is the basic SD for adding currencies on account), ConvertToEuro and ConvertFromEuro are defined as optional (these two last basic SDs specify exchange calculations).

•

There are two SD variants when withdrawing from an account: withdraw with balance and limit checking, and withdraw with balance checking only. The SD Withdraw is defined with the variation mechanism. The two SDs WithdrawWithLimit and WithdrawWithoutLimit are basic SD variants.

From the E BPL and using the PE derivation component, four product expressions are derived, one for each banking product.

The two expressions E BS1 and E BS1 below are respectively expressions obtained for the product BS1 and BS2 respectively. Using the UML2 State machine synthesis component, state machines can be synthesized for all objects participating in interactions. Figure 10, shows the state machine generated for the Bank object.

Product

CONCLUSION & PERSPECTIVES

In this paper, we presented the PLiBS tool: an Eclipse-based tool for software product line behavior engineering implemented in the context of the Families project [START_REF]FAMILIES project[END_REF]. PLiBS allows software product line behavior specification using UML2 SD and implements a two-process approach to derive product behaviors. The first process is based on model specialization through algebraic expression interpretation and the second stage uses state machine synthesis. Within the PLiBS architecture the interface to the EclipseUML is independent from the core implementation. This facilitates integrating new UML tools. It is only sufficient to develop the component interface associated with the new UML tool. In addition, the separation in two independent components between PL expression derivation and UML2 state machines processes allows using PLiBS in the context of the single product development (without considering of variability). In this context, the user only uses the UML2 state machine synthesis component.

UML state machine are useful for code generation. Some tools such as Rhapsody [START_REF]Rhapsody[END_REF] allow generating code from them. We currently working on integrating in PLiBS a code generator. This gives a good way for prototyping the derived products by generating code from product-specific state machines.

The PLiBS tool suffers from some disadvantages. It actually uses ad-oc conventions and notations to specify UML2 SD. This is due to the lack expressiveness of the EclipseUML sequence diagrams. In addition until now PLiBS do not support PL constraints checking. As a perspective, we want integrate an OCL checker. This allows specifying and checking PL constrains as formalized in [START_REF] Ziadi | Towards a UML profile for software product lines[END_REF]22].

Figure 2 .

 2 Figure 2. Basic sequence diagrams specification in PLiBS.

Figure 3 .

 3 Figure 3. Alternative specification in PLiBS. • Loop

Figure 4 .

 4 Figure 4. Loop definition in PLiBS.

Figure 5 .

 5 Figure 5. A portion of the Banking Product Line Combined SD including variability.

EclipseUML-

  PLiBS interface. It extracts from the PL sequence diagrams, specified in the EclipseUML tool, the PL algebraic expression and the description of all basic SD. These outputs respectively represent inputs of the AE derivation component and the Basic SD parser. It implements the PLiBS process 1 (cf. section 2). Subsection 3.3 describes this component in more detail. RESD parser. Is a parser for RESD. The RESD syntax is presented is Section 2. UML2 state machine synthesis component. It implements the PLiBS process 2 (cf. section 2). This component is described in subsection 3.3 .

Figure 6 .

 6 Figure 6. The PLiBS architecture

Figure 8 Figure 7 .Figure 8 .

 878 Figure 7. PL-RESD as displayed by the AE derivation component

Figure 9 .

 9 Figure 9. UML state machine synthesis

Figure 5 ,

 5 Figure 5, shows the portion of the combined SD for the BPL as specified in PLiBS. The E BPL expression, presented above, represents the PL-RESD extracted for the BPL SD thanks to the EclipseUML-PLiBS interface. It refers to the eleven basic SD.The basic SD Deposit for example is SD to deposit an amount on a specific account. Figure2shows the specification of this basic SD.

Figure 10 .

 10 Figure 10. The synthesized state machine for the Bank object in the context of the BS4 product

Software Product Line level

	SPL Behavior Specification		Variability mechanisms
		Decisions on variability
						for Product1
	PliBS 'user							PliBS Process 1	PliBS Process 1	PliBS Process 1
	UML2 sequence diagrams	UML2 sequence diagrams	UML2 sequence diagrams
	requestPassword badPassword badBankPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD.. requestPassword badBankPassword badPassword :User :ATM:Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD1 requestPassword badBankPassword badPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD2 requestPassword badBankPassword badPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD1	requestPassword badPassword badBankPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD.. requestPassword badBankPassword badPassword :User :ATM:Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD1 requestPassword badBankPassword badPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD2 requestPassword badBankPassword badPassword :User :ATM:Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD1	requestPassword badPassword badBankPassword :User :ATM :Consortium :Bank sd SD.. sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 requestPassword badBankPassword badPassword :User :ATM :Consortium :Bank sd BadPassword M3 M1 M2 :O1 :O2 :03 :O4 sd SD1 requestPassword badBankPassword badPassword :User :ATM :Consortium :Bank sd SD2 sd BadPassword M3 M1 M2 :O1 :O2 :03 requestPassword badBankPassword badPassword :User :ATM:Consortium :Bank M3 M2 M1 :O1 :O2 :03 :O4 :O4 sd BadPassword sd SD1
					PliBS Process 2		PliBS Process 2	...	PliBS Process 2
	UML2 state machines		UML2 state machines	UML2 state machines
	B ank i n B S1 pr od uct							B ank i n B S1 prod uct
								/ w it hdr awO kM essage ( )
									/ w i th dr aw ( )	/ wi t hdr aw O k ()
								suff i ci ent B al ance ( )
	B ank i n B S1 prod uct							/ ver i f yBal ance ( am ount ) / ver i f yL i m i t ( am ount ) B ank i n B S1 pr od uct
	/ w i thdr awO kM essage ()			/ w i thdr aw ( )	/ wit hd r aw O k ()		i n suf f i cient B alance () thdr aw OkM essage ( ) / w i	/ w i thdr aw ( )	/ wi thd r awO k ( )
								w i t hdr a wF rom Accou nt (a ccI D, a moun t )
		suff i ci en t Bal an ce ( )						suf fi ci en t Bal an ce ( )
	/ ver i f yB al ance ( am ou nt ) / ver i f yLi m i t ( am ou nt )					wi t hd raw Fa i l l ed Message ( ) / ver i f yB al ance ( am ou nt ) / ver i f yLi m i t ( am ou nt )	B ank i n B S1 prod uct
	B ank i n B S1 pr od uct						B ank i n B S1 pr od uct
	w i t h dr aw F r om Account (accI D , am ount )	i nsuf f i ci ent Bal ance ( ) / w i t hdr aw O kM essage ( )			cr eat eA ccount ( cust I D , ba l ) w i t h dr aw F rom Account ( accI D , am ount ) / cr ea t e ( cu stI D)	/ depo si t ( bal )	i nsuf f i ci ent Bal ance ( )	/ w it hdr awO kM essage ( ) / w it hdr awO kM essage ( )	/ w i t h dr aw ( ) / w i t h dr aw ( )	/ wi t hdr aw O k () / wi t hdr aw O k ()
						/ wi t h draw ( )	/ w i t hdr aw Ok ( )		suf f i ci ent B al ance ( ) suf f i ci ent B al ance ( )
		w i t hdr aw Fai l l edMe ssa ge ( )		suf f i ci ent B al ance ( )		/ i nsuf fi ci en t Message ( )	w i t hdraw Fail l edM e ssa ge ( )	/ ver i f yBalance ( am ount ) / ver i f yBalance ( am ount )	/ ver i f yL i m i t ( am ount ) / ver i f yL i m i t ( am ount )
		/ ver i f yBal ance ( amount )	/ veri f yL i mi t ( amount )
								de posi tO nA cco unt ( accI D, am o unt )
	cr eateA ccount ( cust I D , bal )	/ creat e ( cust I D)	/ de posi t ( b al )				cr eat eA ccount ( cust I D , bal )	/ creat e (cust I D)	/ de posi t ( b al )	i n suf f i ci ent B al ance ( ) i n suf f i ci ent B al ance ( )
					i n suf fi ci entB al ance ( )		/ depo si t ( am o unt )
	/ i nsuf fi ci entM essage ( )	w it hdr a wF r omAccou nt ( a ccI D , a m oun t )				/ insuf f ici ent Message ( )	wi t hd r aw Fa i l l ed Message ( ) wi t hd r aw Fa i l l ed Message ( )
				wi thd r awFa i l l ed M essage ()		/ set Lim i t ( )
	dep osi tO nAccou nt (a ccI D, am oun t )						dep osi t OnAccou nt ( a ccI D, am oun t )
	/ deposi t ( am ou nt )	creat eA ccount ( cust ID , ba l )	/ cr ea t e ( cu st I D)	/ depo si t ( bal )		/ deposi t (am ou nt )	cr eat eA ccount (cust I D, ba l)	/ cr ea t e ( cu st I D)	/ depo si t ( bal )
		/ se t Lim i t ( )							/ se t Lim i t ( )
		/ i nsuf f i ci en t M essage ()						/ i nsuf f i ci en t M essage ( )
		de posi t O nA cco unt ( accI D , am o unt)					de posi t O nA cco unt ( accI D , amo unt )
		/ depo si t ( amo unt )							/ depo si t ( am o unt )
									/ set Li m i t ( ) / set Li m i t ( )
					/ set Li m i t( )				/ set Li m i t ()
	Product 1		Product 2	Product n

UML sequence diagrams with

Variability mechanisms (Stereotypes & taggued values) cr eateA ccount ( cust I D , ba l ) / cr ea t e ( cu stI D) / depo si t ( bal ) / i nsuf fi ci en tM essage ( ) de posit O nA cco unt ( accI D, amo unt ) / depo si t ( am o unt ) w i t hdr a wF r om Accou nt ( a ccI D, a moun t ) / ver i f yB al ance ( am ount ) / ver i f yL i m i t ( am ount ) suf f i ci ent B al ance ( ) / w i th dr aw ( ) / wi t hdr aw O k ( ) / w it hdr awO kM essage ( ) i n suf f i ci ent B al ance ( ) wi t hd r aw Fa i l l ed Message ( ) / set Lim i t ( ) B ank i n B S1 pr od uct cr eateA ccount ( cust I D , bal ) / creat e ( cust I D) / de posi t ( b al ) / i nsuf fi ci entM essage ( ) dep osi tO nAccou nt (a ccI D, am oun t ) / deposi t ( am ou nt ) w i t h dr aw F r om Account (accI D , am ount ) / ver i f yB al ance ( am ou nt ) / ver i f yLi m i t ( am ou nt ) suff i ci en t Bal an ce ( ) / w i thdr aw ( ) / wit hd r aw O k () / w i thdr awO kM essage () i nsuf f i ci ent Bal ance ( ) w i t hdr aw Fai l l edMe ssa ge ( ) / se t Lim i t ( ) B ank i n B S1 prod uct creat eA ccount ( cust ID , ba l ) / cr ea t e ( cu st I D) / depo si t ( bal ) / i nsuf f i ci en t M essage () de posi t O nA cco unt ( accI D , am o unt) / depo si t ( amo unt ) w it hdr a wF r omAccou nt ( a ccI D , a m oun t ) / ver i f yBal ance ( amount ) / veri f yL i mi t ( amount ) suf f i ci ent B al ance ( ) / wi t h draw ( ) / w i t hdr aw Ok ( ) / w i t hdr aw O kM essage ( ) i n suf fi ci entB al ance ( ) wi thd r awFa i l l ed M essage () / set Li m i t( ) B ank i n B S1 pr od uct cr eateA ccount ( cust I D , ba l ) / cr ea t e ( cu stI D) / depo si t ( bal ) / i nsuf fi ci en tM essage ( ) de posit O nA cco unt ( accI D, amo unt ) / depo si t ( am o unt ) w i t hdr a wF r om Accou nt ( a ccI D, a moun t ) / ver i f yB al ance ( am ount ) / ver i f yL i m i t ( am ount ) suf f i ci ent B al ance ( ) / w i th dr aw ( ) / wi t hdr aw O k ( ) / w it hdr awO kM essage ( ) i n suf f i ci ent B al ance ( ) wi t hd r aw Fa i l l ed Message ( ) / set Lim i t ( ) w it hdr a w F r omAccou nt ( a ccI D , a m oun t ) / ver i f yBal ance ( amount ) / veri f yL i mi t ( amount ) suf f i ci ent B al ance ( ) / wi t h dr aw ( ) / w i t hdr aw O k ( ) / w i t hdraw O kM essage ( ) i n suf fi ci ent B al ance ( ) wi t hd r awFa i l l ed M essage ( ) / set Li m i t () B ank i n B S1 pr od uct cr eat eA ccount ( cust I D , ba l ) / cr ea t e ( cu stI D) / depo si t ( bal ) / i nsuf fi ci en t Message ( ) de posi tO nA cco unt ( accI D, am o unt ) / depo si t ( am o unt ) w i t hdr a wF rom Accou nt (a ccI D, a moun t ) / ver i f yBal ance ( am ount ) / ver i f yL i m i t ( am ount ) suff i ci ent B al ance ( ) / w i th dr aw ( ) / wi t hdr aw O k () / w it hdr awO kM essage ( ) i n suf f i cient B alance () wi t hd raw Fa i l l ed Message ( ) / set Lim i t ( ) B ank i n B S1 prod uct cr eat eA ccount ( cust I D , bal ) / creat e (cust I D) / de posi t ( b al ) / insuf f ici ent Message ( ) dep osi t OnAccou nt ( a ccI D, am oun t ) / deposi t (am ou nt ) w i t h dr aw F rom Account ( accI D , am ount ) / ver i f yB al ance ( am ou nt ) / ver i f yLi m i t ( am ou nt ) suf fi ci en t Bal an ce ( ) / w i thdr aw ( ) / wi thd r awO k ( ) / w i thdr aw OkM essage ( ) i nsuf f i ci ent Bal ance ( ) w i t hdraw Fail l edM e ssa ge ( ) / se t Lim i t ( ) B ank i n B S1 pr od uct cr eat eA ccount (cust I D, ba l) / cr ea t e ( cu st I D) / depo si t ( bal ) / i nsuf f i ci en t M essage ( ) de posi t O nA cco unt ( accI D , amo unt ) / depo si t ( am o unt ) w it hdr a w F r omAccou nt ( a ccI D , a m oun t ) / ver i f yBal ance ( amount ) / veri f yL i mi t ( amount ) suf f i ci ent B al ance ( ) / wi t h dr aw ( ) / w i t hdr aw O k ( ) / w i t hdraw O kM essage ( ) i n suf fi ci ent B al ance ( ) wi t hd r awFa i l l ed M essage ( ) creat eA ccount ( cust ID , ba l ) / cr ea t e ( cu st I D) / depo si t ( bal ) / i nsuf f i cien t M essage ( ) de posi t OnA cco unt ( accI D , am o unt ) / depo si t ( am o unt) wi t hdr a wF r omAccou nt ( a ccI D , a m oun t ) / veri f yBal ance ( am ount ) / ver i f yL im i t ( am ount) suf f ici ent B al ance ( ) / w i t h dr aw () / w i thdr awO k ( ) / w i t hdr aw OkM essage ( ) i n suff i ci entB al ance ( ) wi thd r awFa i l l ed M essage () / set Li m i t( ) B ank i n B S 1 pr od uct creat eA ccount ( cust ID , bal) / cr eat e ( cust I D ) / de posi t ( b al ) / i nsuf f i ci ent M essage ( ) dep osi t O nAccou nt ( a ccI D, am oun t) / deposi t ( amou nt ) wi t h dr aw F r omAccount ( accI D , am ount ) / ver if yB alance ( am ou nt ) / ver i f yLim i t ( am ou nt ) suf f i ci en t B al an ce ( ) / w i t hdr aw ( ) / wi t hd r aw Ok ( ) / w i t hdraw O kM essage ( ) i nsuf fi ci entBal ance ( ) w it hdr awFai l l edM e ssa ge () / se t Li mi t ( ) B ank i n B S 1 pr od uct cr eateA ccount ( cust I D , ba l ) / cr ea t e ( cu stI D) / depo si t ( bal ) / i nsuf fi ci en t Message ( ) de posi tO nA cco unt ( accI D, am o unt ) / depo si t ( am o unt ) w i t hdr a wF r om Accou nt ( a ccI D, a moun t ) B ank i n B S1 prod uct creat eA ccount ( cust ID , ba l ) / cr ea t e ( cu st I D) / depo si t ( bal ) / i nsuf f i cien t M essage ( ) de posi t OnA cco unt ( accI D , am o unt ) / depo si t ( am o unt) wi t hdr a wF r omAccou nt ( a ccI D , a m oun t ) / veri f yBal ance ( am ount ) / ver i f yL im i t ( am ount) suf f ici ent B al ance ( ) / w i t h dr aw () / w i thdr awO k ( ) / w i t hdr aw OkM essage ( ) i n suff i ci entB al ance ( ) wi thd r awFa i l l ed M essage () / set Li m i t( ) B ank i n B S 1 pr od uct creat eA ccount ( cust ID , bal) / cr eat e ( cust I D ) / de posi t ( b al ) / i nsuf f i ci ent M essage ( ) dep osi t O nAccou nt ( a ccI D, am oun t) / deposi t ( amou nt ) wi t h dr aw F r omAccount ( accI D , am ount ) / ver if yB alance ( am ou nt ) / ver i f yLim i t ( am ou nt ) suf f i ci en t B al an ce ( ) / w i t hdr aw ( ) / wi t hd r aw Ok ( ) / w i t hdraw O kM essage ( ) i nsuf fi ci entBal ance ( ) w it hdr awFai l l edM e ssa ge () / se t Li mi t ( ) B ank i n B S 1 pr od uct cr eateA ccount ( cust I D , ba l ) / cr ea t e ( cu stI D) / depo si t ( bal ) / i nsuf fi ci en t Message ( ) de posi tO nA cco unt ( accI D, am o unt ) / depo si t ( am o unt ) w i t hdr a wF r om Accou nt ( a ccI D, a moun t )

Product level Figure 1. Our approach for modeling and deriving behaviors of software product lines.

Table 1 . The Banking PL Members.

 1

	To illustrate the PLiBS use, we present the example of a
	Banking Product Line (BPL). It is a set of products providing
	simple functionalities to clerks in the banking domain. It
	provides four main functionalities:
	•	Creation of accounts (F1) Customers are able to open
		simple accounts but must do so with a minimum balance.
		Account can have an associated limit specifying to what
		extent a customer can overdraw money.
	•	Money deposit on accounts (F2) Customers can deposit
		an amount of money on their accounts.


Jim Steel
email: jim.steel@irisa.fr

Jean-Marc Jézéquel
email: jezequel@irisa.fr

Dr Lionel J Briand

J.-M Steel

Jézéquel

On model typing

Keywords: MDA, MOF, Metamodelling, Type systems, Typing, Model transformation

Where object-oriented languages deal with objects as described by classes, model-driven development uses models, as graphs of interconnected objects, described by metamodels. A number of new languages have been and continue to be developed for this modelbased paradigm, both for model transformation and for general programming using models. Many of these use single-object approaches to typing, derived from solutions found in object-oriented systems, while others use metamodels as model types, but without a clear notion of polymorphism. Both of these approaches lead to brittle and overly restrictive reuse characteristics. In this paper we propose a simple extension to object-oriented typing to better cater for a model-oriented context, including a simple strategy for typing models as a collection of interconnected objects. We suggest extensions to existing type system formalisms to support these concepts and their manipulation. Using a simple example we show how this extended approach permits more flexible reuse, while preserving type safety.

Introduction

From the perspective of the data structures involved, model-driven computing can be seen as a progression from object-oriented computing. Models are, in essence, composed of objects linked together using first-class bidirectional relationships, where the structure of the objects and the relationships between them are typically defined by a MOF, or MOF-like, metamodel. The presence of these relationships has the effect that model structures are much more tightly coupled than object structures.

Given this heritage, it is hardly surprising that the majority of approaches to developing languages for manipulating models have adopted formalisms based on those found in object-oriented programming languages.

The study of languages for manipulating these model structures is active. In 2001, the OMG issued an RFP soliciting languages for defining model transformations, as mappings between models. In response, many languages have been developed, using variously logic-based [START_REF] Gerber | Transformation: the missing link of MDA[END_REF], pattern-based [START_REF]QVT-Merge Group: Revised submission for MOF 2.0 Query/Views/Transformations RFP[END_REF], and graph-transformation [START_REF] Sendall | Combining generative and graph transformation techniques for model transformation: an effective alliance?[END_REF] approaches. Concurrently, a number of efforts are being undertaken to develop or extend programming languages to better deal with models as data structures [START_REF] Muller | Weaving executability into object-oriented meta-languages[END_REF].

The vast majority of these efforts have chosen to use type systems developed for use within object-oriented development. However, as discussed in [START_REF] Edwards | A type system for object models[END_REF] and mentioned in [START_REF] Steel | Model-based test driven development of the tefkat model-transformation engine[END_REF], the use of such type systems in a modeloriented context renders programs somewhat brittle with respect to changes in the metamodel, often failing in response to changes that ought not to affect their operation.

Most important, however, is that these systems do not truly allow the user to specify their transformations or programs in terms of models and types of models, but rather in terms of objects within models. This is counterintuitive to the user.

To resolve this, we discuss necessary extensions to object-oriented typing to deal with the relationships defined in MOF metamodels. Using this extended notion of object typing, we propose a definition of a model type, including a definition of substitutability of model types and a discussion of reflection and inference of model types.

In Sect. 2, we provide a background on typing and models and the role of typing in model-driven engineering, including a motivating example. Following this, in Sect. [START_REF] Bierman | First-class relationships in an object-oriented language[END_REF] we present a definition of model types with a rule for model type substitutability, based on intuitive concepts from model-driven engineering and building upon research from object-oriented type systems. In Sect. [START_REF] Blanc | Model bus: Towards the interoperability of modelling tools[END_REF] we show how a language and type system supporting these concepts might be built as an extension of existing formalisms. Section 5 discusses several further issues related to model typing, including reflection and type inference. Section 6 discusses a number of related works from the domains of both MDE and type systems.

Background

Generally speaking, a type can be understood as a set of values on which a related set of operations can be performed successfully. Once types have been defined, it is possible to use them in operation specifications of the form: if some input of type X is given, then the output will have type Y. Type safety is the guarantee that no run-time error will result from the application of the operation to the wrong object or value. A type system is a set of rules for checking type safety (a process usually called type checking since it is often required that enough information about the typing assumptions has been given explicitly by the designer or programmer, so that type checking becomes mostly a large bookkeeping process).

Type checking is said to be static when it is performed without program execution (typically at compile-time or bind-time). It aims at ensuring once and for all that there is no possibility of interaction errors (of the kind addressed by the type system). Not all errors can be addressed by type systems, especially since one usually requires that type checking is easy; e.g., with static type checking it is difficult to rule out in advance all risks of division-by-zero errors.

Type systems allow checking substitutability when services are combined: by comparing the data types in a service interface, and the data types desired by its caller, one can predict whether an interaction error is possible (e.g., producing a run-time error such as "Method not understood"). Conformance is generally defined as the weakest (i.e., least restrictive) substitutability relation that guarantees type safety. Necessary conditions (applied recursively) are that a caller must not invoke any operation not supported by the service, and the service must not return any exception not handled by the caller. Conformance has a property called contravariance: the types of the input parameters of a service must vary (as either supertypes or subtypes) in the opposite direction to those of its result parameters.

Example

We consider as a motivating example a simple model transformation that takes as input a state machine and produces a lookup table showing the correspondence between the current state, an arriving event, and the resultant state. The input metamodel for this transformation is presented in Fig. 1. The output metamodel, not shown, can be assumed to be a simple database language, but in any case we will focus on the conformance of the input type. The choice of which language is used to implement the transformation, and even of which paradigm of language to use, is immaterial. Also immaterial is the choice as to whether the input and output types of the transformation are derived (inferred) or explicitly declared. (This choice is discussed further in Sect. 5).

Having given this metamodel as the nominal input for the transformation, we consider that there are a number of variants of state machines whose instances might also be interesting as potential inputs to the transformation.

Initially, we might consider changing the multiplicity of the "initial" reference from 0..1 to 0..*, for state machines with multiple start states (Fig. 2), or from 0..1 to 1..1, mandating that each state machine have exactly one start state (Fig. 3). Alternatively, we might apply the composite pattern by adding an inheritance of State by StateMachine, for composite state machines (Fig. 4). Finally, we might consider the addition of a FinalState class as a new subclass of State (Fig. 5).

The question is, then, does the initial transformation written for models conforming to Figure 1 still work with models conforming to these variant metamodels?

Objects, and their types

Although research is ongoing into the fine details, the basic notions of objects and the type systems that describe them are by now reasonably well-understood Fig. 5 With final states [START_REF] Abadi | A Theory of Objects[END_REF]. As mentioned briefly above, the main difference between the objects seen in classical object-oriented systems and the objects used within models is the presence of (potentially) bidirectional relationships.

In MOF 1.x, these relationships were defined as binary associations, which in turn contained association ends, which specified characteristics such as the upper and lower bounds, uniqueness and orderedness of the association in a given direction. Navigability was specified by the addition of references.

In MOF 2.0, relationships are defined as a pair of references, each of which defines the details formerly kept by association ends. These references may link to another reference, thus forming a bidirectional relationship. This change entails a subtle change of expressivity but, in effect, yields the same type of relationships.

Models and metamodels

The MOF specifications, unlike those of UML, have never included a formal definition of either a model or a metamodel. By convention, and intuitively, the latter has usually been used as a synonym for a MOF package. In many MOF 1.x implementations, a model was defined as a "package instance", a term not defined in the specifications, but an intuitive concept that could contain objects instantiated from any class within a given MOF package. While intuitive, these definitions were somewhat limiting for situations where cross-"model" references were common.

MOF 2.0 has introduced the notion of an extent, and made explicit the fact that extents may contain objects instantiated from classes from different packages. This recognises the increasing abundance of models which reference other models; these are intuitively, and may now be considered as, single models. However, this leaves us without a firm idea of a metamodel, since we can no longer be guaranteed that all objects within an extent will possess a type contained by a single package. Beyond these conventions, there are two general approaches to defining a concept of a model. The first, that taken by UML, is to designate some class as being a root node for the model, meaning that the model then consists of an instance of that class and all objects contained by (or perhaps reachable from) this root instance. However, this does not work in the case of models which lack a single root element, as is common in cases such as models containing tags or models of, for example, collaborative processes [START_REF]Object Management Group: Enterprise collaboration architecture (ECA). OMG Document no[END_REF]. The alternative and more general approach, the one evident as Extent in MOF 2.0, is to define a model as just a set of objects.

Taking this second definition, one intuitive choice for the type of a model is the set of the object types of all the contained objects. The details of such a definition are given in the next section.

Typing in model-driven engineering

The application of typing in model-driven engineering is seen at a number of levels.

At a fine-grained level, languages that manipulate and explore models need to be able to reason about the types of the objects and properties that they are regarding within the models. For this level of granularity, an object-based approach to typing is probably more natural and appropriate.

From an architectural perspective, there is also a need to reason about the types of artifacts handled by the transformations, programs, repositories and other model-related services. It is at this level that an appropriate type system should allow us to reason about the construction of coherent systems from the services available to us. While it is possible to define the models handled by these services in terms of the types of the objects that they accept, we argue that this is not a natural approach, since these services intuitively accept models as input, and not objects.

Having established that services might accept and produce models, it follows that they should specify a type for these models. Furthermore, having established these type declarations, it is also useful to find a semantic for substitutability that allows the maximum possible flexibility and reuse, while still assuring that the services do not receive models whose elements they do not understand.

For example, the sample transformation described in Sect. 2.1 can be said to accept state machines as input, and should accept as many of the noted variants as possible, provided that at no point the transformation attempts an action on the model that is not possible.

Model types and model type substitutability

In this section we provide a simple structure for the type of a model and discuss the conditions under which one model type may be substituted for another. This includes an analysis of the dependence of model typing upon object typing, and the extensions necessary for object typing to function correctly in this new context. We demonstrate the application of model types using the example presented earlier.

Model types and type checking

The previous section loosely describes a model type as the set of object types for all the objects contained in a model. However, this is a definition based on reflection, and the aim of model types is rather targeted at transformation or model-based programming languages, where reflection will not be the dominant manner of determining types. Therefore, we need to redefine our model type more basically.

So what structures do we have? Normal MOF reflection upon an object yields a MOF class. While literature on type systems, such as [START_REF] Lalonde | Subclassing = subtyping = is-a[END_REF], suggests that a type is not the same thing as a class, the terminology used by MOF is somewhat misleading. Since MOF is a signature language, i.e., unable to specify behaviour, a MOF class is in fact more analogous to an object type than to a class in type system terminology. We therefore content ourselves to define a model type as a set of MOF classes (and, of course, the references that they contain).

In the example presented in Sect. 2.1, the model type required for our transformation is in essence the metamodel shown in Fig. 1. In fact, the only significant difference between model types and metamodels is the structuring provided by packages and relationships between packages.

Having established the structures with which we will type models, the question remains: under what conditions may one model type, i.e., set of object types, be considered conformant, or substitutable, for another? Quite simply, each object type in the required set must be "understood" by the candidate set. Clearly, this returns to a situation of object type conformance.

Object-type conformance

As mentioned earlier, type systems for object-based languages are reasonably well-understood, and are increasingly being implemented in the most popular object-oriented programming languages. Typically, the relation used for conformance of one object type to another is subtyping.

Subtyping, as described briefly in Sect. 2, requires that the operations defined on two object types show covariance of their return types and contravariance of their parameter types. If we consider each MOF property to be a pair of accessor/mutator methods this means that subtyping for MOF classes requires invariance of property types.

Unfortunately, one of the strong motivating cases for a polymorphic notion of model types is to allow transformations to keep working as metamodels evolve over time. One of the most common evolutions seen in metamodels is the addition of a property to a class. In this case, any reference to such a class will vary its type. More formally, the addition of the attribute will likely cause a covariant property type redefinition somewhere in the metamodel.

For example, consider a comparison of the basic statechart metamodel in Fig. 1 with the composite statechart metamodel in Fig. 4. As a result of adding the inheritance link, the StateMachine class in the Composite metamodel has evolved to have two more properties: name of type String, and stateMachine, pointing towards a possible containing StateMachine. In isolation, the addition of these attributes might seem to preserve a subtype relationship between the two StateMachine classes. However, this would mean that the property Composite::State.stateMachine represents a covariant redefinition of Basic::State.stateMachine. This is a problem, since property types must be invariant in order to preserve subtyping. Furthermore, the interdependence between the three classes in the metamodels that results from having bidirectional references means that any addition of an attribute would break subtyping for every class in the metamodel.

Nonetheless, from the point of view of a program written to manipulate a Basic state machine, the addition of attributes should make no difference. The lack of a subtyping (or subsumption) relationship between the classes only poses a problem from the point of view of an individual class. For instance, a composite State cannot be added to a Basic state machine, since an operation on the composite State may attempt to access the "name" or "containingState" property of the Basic state machine, resulting in a type error. However, provided that we specialise the classes in parallel, and ensure that instances of Basic classes and Composite classes do not mix, then there should be no problem.

As it turns out, there is another relationship discussed in type systems for comparison of object types: matching [START_REF] Bruce | Polytoil: a type-safe polymorphic object-oriented language[END_REF]. An object type T matches another T (denoted T < # T), iff every method in T also occurs in T with the same signature. The matching relation is weaker than subtyping; in particular it does not enjoy subsumption, i.e., objects of a matching type are not guaranteed to conform to the matched type. However, as Bruce shows in [START_REF] Bruce | Polytoil: a type-safe polymorphic object-oriented language[END_REF][START_REF] Bruce | Semantics-driven language design: Statically type-safe virtual types in object-oriented languages[END_REF] and through the PolyTOIL and LOOM/LOOJ languages, using this relation between groups of types allows for a more flexible, but still statically type-safe, notion of re-use when dealing with the parallel specialization of inter-related object types. This comes with the caveat that matching classes are never used in the context of heterogenous collections. Notably, in the context of models, type-safety depends on models remaining homogenous with respect to a set of object types.

Changes for MOF object structures

The presence of relationships, in whichever form, defined between classes has little effect on the overall approach on the typing of objects. The structure of an object type remains the same. Indeed, if one considers a relationship as a mutually dependent pair of references, they do not differ fundamentally from the properties seen commonly in object-oriented systems. There is, of course, a stronger prevalence of cyclic dependencies between the conformance of classes. For example, consider a class C1 in a relationship A1, consisting of two references R1 and R2, with another class C2. For a class C1 to be considered a match of C1, it must participate in a relationship A1 with a class C2 that is a match of C2, which fact depends on the original comparison of C1 and C1.

One of the more significant differences with the object structure of MOF is the presence of multiplicities: upper and lower bounds, uniqueness and orderedness. In order for a MOF property to be considered conformant, not only must its type be a match, but also its multiplicity. For example: -does a multi-valued property conform to a singlevalued property?

-does an optional property conform to a mandatory property? -does a set-valued property conform to a bag-or sequence-valued property?

In Sect. 4, we present a simplified language which does not consider orderedness or uniqueness, which issues we leave for later resolution, but does provide matching rules based on subsumption of multiplicity bounds.

Model-type conformance

Bruce further defines in [START_REF] Bruce | Semantics-driven language design: Statically type-safe virtual types in object-oriented languages[END_REF] the < # relation between two type groups as a function of the object types which they contain. This is precisely what we need for determining whether a required model type may be satisfied by a provided model type. Specifically, Bruce states that:

Type group TG < # TG iff for each type MT in TG there is a corresponding type with the same name in TG such that every method in TG.MT also occurs in TG .MT with exactly the same signature as in TG.MT.

We may generalise this to model types by saying that: Model Type M < # M iff for each object type C in M there is a corresponding object type with the same name in M such that every property and operation in M.C also occurs in M .C with exactly the same signature as in M.C.

Towards a type system for models

In this section we describe a formalism for reasoning about models and model types. To do this we propose a basic language for defining transformations as series of simple CRUD (Create, Read, Update, and Delete) operations on objects and models. The first section presents a grammar for this language, including a simplified version of the MOF structural concepts and a number of simplified operators for manipulating them. Following that, we describe a number of rules for typechecking a program written using the language. These rules and their explanation rely heavily on the work presented by Bruce and Vanderwaarts in [START_REF] Bruce | Semantics-driven language design: Statically type-safe virtual types in object-oriented languages[END_REF].

Grammar of types and terms

Figure 6 shows the major structural concepts as defined by MOF. A class is defined with a name, a set of superclasses, and sets of property and operation definitions. Properties have names and types, and may be linked as opposites in order to approximate associations. Operations are named and have typed parameters and a return type. Multiplicities are not present as such, but to capture the important distinctions, we allow properties, parameters and operations to be typed as sets, and to be specified as optional or not. 1Transformations in this language take a single model as a parameter and manipulate it in-place. This represents a significant simplification of the approach taken by most transformation languages, notably in that there is no output model, and only one input model. This is done to avoid complications which come about from having multiple model types interacting within a single transformation which, while possible, is less easily understood.

The parameter type of a transformation is a model type, which is a collection of object types. Model types are also valid types elsewhere in the language (variables, expressions, etc.), but in the interests of explanation we will focus on their use as transformation parameter types.

The grammar elements for declaring model types and transformations are shown in Fig. 7.

For the body of transformation, we provide a basic set of types and terms corresponding to a simple expression language (Fig. 8). There are variables, assignments, invocations of operations and transformations, and conditional/iteration statements, etc. The only operator that might be considered unusual is the >< operator, which filters a model by a given class to return a list of all objects of that type found within the model.

The filtering of a model to retrieve all instances of a type is an operation that is used frequently in model transformations. 2 However, few existing languages propose it as an operator, instead proposing the functionality through a library function (e.g., allInstances() or all_of _kind()). Having a clear concept of a model type allows the definition of the operator with a much more accurate type signature.

We do not provide an expression language here for the bodies of operations, but it might be assumed to be the same as that of transformations. We keep them separate only for reasons of explanation.

The signatures that result from a program in this language are shown in Fig. 9. A class definition is a tuple ({c 1 , . . . , c k }, P, O), where {c 1 , . . . , c k } is a sequence of superclasses, P is a map of property names to types (with booleans for optionality and multi-valuedness) and opposite properties (in order to form associations), and O is a map of operation names to definitions. An operation definition is a tuple of the return type and a map of parameter names to types.

A transformation is a tuple (x, L, m, tb), where x is the parameter, L is a map from local variable names to their types, m is the parameter's model type, and tb is the transformation body.

Language semantics

The semantics of the language is largely the same as that presented in [START_REF] Bruce | Semantics-driven language design: Statically type-safe virtual types in object-oriented languages[END_REF]. The notable exception is that, in that work, the authors present the semantics of their virtual types as a generalisation of the semantics of their MyType operator (i.e., the recursive type), which is absent from the language presented here. While this may seem a gross difference, the semantics and proof of virtual types presented relied upon MyType only as an explanatory aid, and its absence does not fundamentally affect the workings of virtual types. As a result, our language here might be seen as supporting mutually recursive types, but not singly recursive types.

Also absent in the language presented here is any discussion of the internal state of objects, i.e., of instance variables. (Instance variables are not to be confused with our properties, which are instead considered to function as pairs of accessor/mutator methods). Once again, for the purposes of defining the semantics, the matter of internal state may be considered as being treated in a similar manner to [START_REF] Bruce | Semantics-driven language design: Statically type-safe virtual types in object-oriented languages[END_REF].

Thus, following the semantics of virtual types from LOOM, it can be considered that each of the types used within the body of a transformation in association with the model type is virtual. Thus, the transformation is As in LOOM, the semantics of a transformation body at runtime involve an effective substitution of the model types with the matched types. That is, types within a transformation function as virtual types. For example, the invocation of an operation resolves not to the declared type, but to the actual class provided as a match to the declared type. Similarly for references to properties, and for the creation of new instances from classes.

The major structural addition in the language shown here is the ability to type terms using a model type, thus permitting appropriately-typed variables to function as models (as described in Sect. 2.3). Semantically, these variables then function as collections, whose elements are effectively typed as the union of the types declared in the model type.

Selected type-checking rules

In this section we present a number of interesting type checking rules that derive from the grammar and semantics of the language. These do not comprise a full type system; they are rather provided to illustrate the extensions that are implied for the extension of an existing type system in order to treat models and model types. The object type matching rule, and in turn the matching rules for properties, operations and parameters, modified to account for multiplicities, are shown in Fig. 10. There are two considerations here. First, collections are treated differently in the language than singletons, since they are subject to set addition and removal operators. As a result, multi-valued properties Fig. 11 Selected type-checking rules for model types: model types (or operations, or parameters) cannot conform to single-valued, nor vice-versa. The mandatory property, somewhat similar to MOF's lower bounds, obeys subsumption, which in this simplified case is reduced to a nor operator.

These rules represent only a small change from those commonly seen in type system definitions in order to support polymorphism (more specifically, matchbounded polymorphism). The notable change is the treatment of multiplicities.

Figure 11 shows a number of rules that have been added in order to treat models and their types.

Matching between two model types is determined by ModelTypeMatch, provided that both are valid model types, and that there exists a pairwise matching of the object types (following the description given in Sect. 3.4.

There are three rules shown for operators dealing with model-typed variables, i.e., models.

TSTransInv checks that the expression used as a parameter to transformation invocation is modeltyped, and that model type is a match to the declared parameter type.

TSModelAdd permits an element to be added to a model using the += operator, provided that the model's type is a valid extant model type containing the object type of the element to be added.

TSModelFilter ensures that an object type c used as a filter on a model x is indeed present in the model type m of the variable, and that the return type of such an operation is a collection of the filtering object type, i.e., set < c >.

There are a number of other rules implied by the presence of model types and model-typed expressions in the language, which are not presented here in the interests of brevity. These include basic rules for model type matching, including reflexivity and transitivity, and conformance of all model types to the Top model type, {Object}. There are also a number of well-formedness rules to ensure, for example, that a model type includes the transitive closure of object types referred to as types of properties, operations or parameters.

Application to the examples

If we apply the ModelTypeMatch rule to the example metamodels provided in Sect. 2.1, we are able obtain the model type matching relation shown in Table 1.

The relation shows clearly that all of the variants barring those with multiple start states are acceptable for transformations written against a Basic state machine metamodel. We can see that the addition of new classes (FinalState), the tightening of multiplicity constraints (Mandatory), and the addition of new attributes (indirectly with Composite State Charts, via the added inheritance relationship) have not broken model-type matching. However, multiple start states clearly pose a problem should a transformation attempt to navigate the initialState property to obtain a single State object.

It is notable also that Composite state charts are found to be subtypes of simple state charts, although the reverse might have been more intuitive. (A simple state chart might be mistaken for a composite state chart that does not use composition.)

In the other sense, basic state charts do not match any of the variants, nor do any of the variants match each other. The effect of insisting on name equivalence when matching object types may be seen in the non-conformance of basic state charts to those with final states; applying a name-independent structural conformance, these model types would be equivalent, and thus would match.

Further considerations

Having considered the general idea of types for models and presented an approach for verifying the conformance of model types, we now proceed to discuss two related issues, those of model type reflection and model type inference.

Model topologies

The approach presented above for typing objects within the context of a metamodel is based loosely on a structural, rather than a nominative approach to subtyping. We do, however, require that matching object types in a model type preserve the same name, unlike the structural conformance used, for example, in ML or Ruby.

One of the issues that might arise one adopt a name-independent structural conformance approach is that model types that match with respect to individual object-type comparisons nonetheless do not resemble one another. For example, one can imagine a single bloated object type providing a match for all object types required in a metamodel, by including the union of properties and operations from all of the required types.

To resolve this, a matching of model types might additional enforce certain rules pertaining to the preservation of the identity of classes when assessing conformance of relationships. These rules might include:

1. A reflexive relationship may not be matched by a non-reflexive relationship. 2. A non-reflexive relationship may not be matched by a reflexive relationship.

One can imagine that a more general solution might lead to some sort of topological analysis of the relationships in a metamodel. In practice, however, the number of properties attached to object types makes relevant applications for such an analysis rare.

Model type reflection

Reflection is one of the key features of model-driven engineering. The ability to ask an object about what features it provides allows for the creation of generic tools that work regardless of the metamodel from which the object was instantiated. Many services such as XML and textual serialization and deserialization, model repositories, and code generators, already make extensive use of object reflection.

Having added an idea of a model type, it is clearly necessary to consider the problem of model type reflection. That is, if a user provides a model to a service, it should be possible to determine the type of the model by looking at the types of the objects that it contains.

The problem that arises when determining the model type of a model is that there is a need to consider object types that are not instantiated by the model itself. For example, consider a basic state machine that contains a single state but no transitions (uninteresting though such a model might be). By simply taking the object types of all objects in the model, the Transition type would not be included in the model type, making the model ineligible for a transformation written to manipulate basic state machines. There is a difference between the absence of an instance in the model and the absence of the type in the model type.

One solution might be to compute a transitive closure of all types referenced as types of properties, operations or parameters, which would certainly suffice for finding the Transition class for a transitionless state chart. However, there will arise other cases where the navigabilities of the references makes types unreachable by navigation.

As a general problem, this requires a form of existential quantification, which is something not available in current MDE tools. In lieu of this, one alternative would be to use bounded existential quantification, such as searching for all referring types within a given set of packages, e.g., those already containing object types obtained from object reflection.

Model type inference

A closely related issue to model-type reflection is that of model-type inference.

In the example transformation language presented in Sect. 4, model types for transformation parameters were declared explicitly. There are, however, two alternatives for determining the types of, for example, operation parameters. In manifest typing, as is commonly seen in languages such as Java and C#, for example, types are defined by the user. By contrast, in languages such as ML, types are inferred from the code written by the user.

One can imagine that a similar approach could be used by a model transformation language. A transformation or program whose definition constructs models from a limited set of classes might be able to determine its output model type from the statements creating the objects. Similarly, a parameter type might be determined by examining which properties or operations were accessed, or what types were used as filters.

Obviously, this approach, of building a model type based on its usage, has a lot in common with the reflection problem discussed above, and one would imagine that, having determined the classes used in the definition, similar techniques might be used to determine more accurately the complete model type.

While model typing and model type reflection are problems that can be considered largely independent of the choice of model transformation or programming language, model type inference is likely not. Inference on transformations defined using a rule/pattern-based language such as XMorph [START_REF] Duddy | Declarative transformation for object-oriented models[END_REF] will require a different solution to inference on programs defined using a more imperative language such as MTL [START_REF] Muller | Weaving executability into object-oriented meta-languages[END_REF].

Related work

The formalism presented above is based heavily on the work done by Bruce et al on type groups, in particular with respect to the type-safe specialization of interrelated types. However, although Bruce introduces the notion of type groups in order to type objects whose types are inter-related, he does not allow terms in his language to be typed by type groups. That is, his language does not introduce the concept of a collection of interrelated objects, or a model.

Although in this paper we have based our approach on type groups, there exist other approaches [START_REF] Bruce | Some challenging typing issues in objectoriented languages[END_REF] to the problem of parallel specialization of inter-related object types, including "family polymorphism" [START_REF] Ernst | Family polymorphism[END_REF]. Although family polymorphism could potentially serve as an alternative basis for model typing, its formalism is less developed than that of type groups. Also, like type groups, family polymorphism does not consider the problem of typing graphs or collections of inter-related objects as terms in the language.

In [START_REF] Edwards | A type system for object models[END_REF], the authors present a system for checking the type compatibility of constraints on object models expressed in Alloy, a language similar in purpose to the combination of OCL and MOF. They propose an algorithm using bounding types and base types to determine whether an expression has meaning with respect to a given object model. Since this approach is based on the UML class diagram metamodel, which bears significant structural similarity to that of MOF, this algorithm would apply straight-forwardly to MOF metamodels. However, the approach they present does not go so far as to encapsulate models nor their types, and thus does not present any notion of polymorphism, since it relies on an interpretation of the constraints with any new object model.

In [START_REF] Bierman | First-class relationships in an object-oriented language[END_REF], the authors present an extension to Java to provide for first-class relationships between classes, including a formal definition for the resultant type system. Their proposal includes a notion of relationship subtyping based on set membership, which bears a resemblance to the idea of association subsetting presented in the UML 2.0 Infrastructure. Although we have not chosen to model MOF relationships in the same way in this paper, the formalisms they define might present an alternative to the reductionist view we have taken here.

One aspect of MOF that has not been greatly discussed in this paper is the meta-class hierarchy. In [START_REF] Tobin-Hochstadt | Fundamentals of Object-Oriented Languages[END_REF], the authors present a type system for a metaclass system, as an extension of a Java-like language. An interesting future effort might be to evaluate the possibility of integrating the typing considerations they discuss with MOF's meta-level functionality, as provided by MOF's reflection module.

Having formalised a concept of model and model type, there are a number of domains to which the ideas may be applied. Obviously, having defined a transformation language here, the most obvious choice is to incorporate the ideas into an existing language such as Kermeta [START_REF] Muller | Weaving executability into object-oriented meta-languages[END_REF] or Tefkat [START_REF] Duddy | Model transformation: A declarative, reusable patterns approach[END_REF].

From an architectural point of view, the problem of organising models, transformations, programs and other development artifacts to form coherent model-driven systems is a field just beginning to attract attention. In [START_REF] Blanc | Model bus: Towards the interoperability of modelling tools[END_REF], the authors discuss a model bus, for describing model services and mediating access to them including automation of coercion of models to ensure compatibility. In [START_REF] Bézivin | On the need for megamodels[END_REF], the idea is presented of a megamodel, a system or registry of models and the relations that exist between them, most significantly those of conformance and representation. Such approaches would benefit from a type system to govern which models may be associated with which others.

Conclusion

The lack of proper mechanisms for typing operations on models such as model transformations leads to brittle and overly restrictive reuse characteristics. In this paper we have proposed a simple extension to objectoriented typing to better cater for a model-oriented context, including a simple strategy for typing models as a collection of interconnected objects. Using a simple example we have shown how this extended approach permits more flexible reuse of model transformations accross various meta-models, while preserving type safety. We have proposed a simple system for checking the conformance of model types, independently of any given transformation language. A prototype implementation, based on and extending the formalisms presented here, has been integrated into the Kermeta modeloriented programming language/environment, implemented on the Eclipse/EMF platform, presented in this paper. This will help to validate the approach for largerscale model-driven systems, and to inform the application of model-typing principles to other contexts, such as Model-Bus tool interoperability or Q/V/T transformation languages.

Fig. 1 Fig. 2 Fig. 3 Fig. 4

 1234 Fig. 1 Simple state machine metamodel

Fig. 6 Fig. 7

 67 Fig. 6 Language grammar: MOF structural concepts

Fig. 8 Fig. 9

 89 Fig. 8 Language grammar: expressions and statements

Fig. 10

 10 Fig. 10 Selected type-checking rules for model types: object-type matching

Table 1

 1 Model type conformance relation for state machine variants matches →

This is an equivalent formalism to that used in the ECore modeling language, from the Eclipse Modeling Framework[START_REF] Budinsky | Eclipse Modeling Framework Eclipse Series[END_REF].

Indeed, many rule-based languages, such as[START_REF] Duddy | Model transformation: A declarative, reusable patterns approach[END_REF], are built around some sort of filter functionality.

Author's biography

Jim Steel is a PhD student at the INRIA/Irisa laboratory at the university of Rennes, and has been working in the field of model-driven engineering and metamodelling since 1997. He graduated with a B.InfTech(Hons 1) from the University of Queensland in 1999, with his honours thesis dealing with the generation of human-usable textual notations for MOF meta-models, which work later served as the basis of the OMG standard. After graduating, he worked for four years as a research scientist with the Pegamento project at the Distributed Systems Technology Centre (DSTC), in Brisbane, Australia. During this time he participated in numerous standards for model-driven engineering, including HUTN, the UML Profile for EDOC, and MOF2.0 QVT. He also participated in the development of prototypes including the TokTok notation generator and the Tefkat model transformation engine.

Prof. Jean-Marc Jezequel received an engineering degree in Telecommunications from the ENSTB in 1986, and a Ph.D. degree in Computer Science from the University of Rennes, France, in 1989. He first worked in the Telecom industry (at Transpac) before joining the CNRS (Centre National de la Recherche Scientifique) in 1991. Since October 2000, he is a Professor at the University of Rennes, leading an INRIA research team called Triskell. His interests include model-driven software engineering based on object-oriented technologies for telecommunications and distributed systems. He is the author of the books "Object-Oriented Software Engineering with Eiffel" and "Design Patterns and Contracts" (Addison-Wesley 1996 and 1999), and of more than 90 publications in international journals and conferences. He is a member of the steering committee of the MODELS/UML conference series. He also served on the editorial boards of IEEE Transactions on Software Engineering and on the Journal on Software and System Modeling: SoSyM and the Journal of Object Technology: JOT.