Keywords: Composants logiciels, modèle de composants, spécification formelle, architecture logicielle, modèle de composants Fractal, langage de spécification Alloy

Une spécification formelle du modèle de composants

Fractal en Alloy Résumé : Ce rapport contient une spécification formelle du modèle Fractal dans le langage de spécification Alloy. Le rapport couvre tous les éléments de la spécification (informelle) de référence du modèle Fractal. Il fournit une spécification du modèle Fractal réellement indépendante des langages de programmation et il résoud les ambiguités de la spécification de référence.

Introduction

Motivation The Fractal component model [START_REF] Bruneton | The Fractal Component Model and its Support in Java[END_REF] is a programming-language-independent component model, which has been introduced for the construction of highy configurable software systems. The Fractal model combines ideas from three main sources: software architecture, distributed configurable systems, and reflective systems. From software architecture [START_REF] Shaw | Software Architecture: Perspectives on an Emerging Discipline[END_REF], Fractal inherits basic concepts for the modular construction of software systems, encapsulated components, and explicit connections between them. From reflective systems, Fractal inherits the idea that components can exhibit metalevel activities and reify through controller interfaces part of their internal structure. From configurable distributed systems, Fractal inherits explicit component connections across multiple address spaces, and the ability to define meta-level activites for runtime reconfiguration. The Fractal model has been used as a basis for the development of several kinds of configurable middleware, and has been used successfully for building automated, architecture-based, distributed systems management capabilities, including deployment and (re)configuration management capabilities [START_REF] Abdellatif | J2EE Packaging, Deployment and Reconfiguration Using a General Component Model[END_REF][START_REF] Caromel | Peer-to-Peer and Fault-Tolerance: Towards Deployment-Based Technical Services[END_REF][START_REF] David | A Multi-stage Approach for Reliable Dynamic Reconfigurations of Component-Based Systems[END_REF][START_REF] Flissi | A Generic Deployment Framework for Grid Computing and Distributed Applications[END_REF], self-repair capabilities [START_REF] Bouchenak | Architecture-Based Autonomous Repair Management: An Application to J2EE Clusters[END_REF][START_REF] Sicard | Using Components for Architecture-Based Management: The Self-Repair Case[END_REF], overload management capabilities [START_REF] Bouchenak | Autonomic Management of Clustered Applications[END_REF], and self-protection capabilities [START_REF] Claudel | Self-protection for Distributed Component-Based Applications[END_REF].

The Fractal model is currently defined by an informal specification [START_REF] Bruneton | The Fractal Component Model[END_REF]. The specification only briefly mentions the general foundations that constitute the Fractal model per se, and focuses mostly on default meta-level capabilities (or controllers, in Fractal parlance). The specification has been successfully implemented in different languages and environments, notably in Java and C, without giving rise to serious issues, which is a testimony to its consistency. However, there are aspects of the specification that remain decidedly insufficiently detailed or ambiguous. The present report attempts to correct these deficiencies by developing a formal specification of the Fractal component model which makes explicit the underlying general component model constituting the foundation of Fractal; which clarifies a number of ambiguities in the informal Fractal specification; and which identifies places where the informal Fractal specification may be overconstraining.

Beyond ensuring the consistency of the Fractal model, a formal specification for the Fractal model can serve several purposes:

• to provide a more abstract, programming-language-independent specification of the Fractal model;

• to allow a formal verification of Fractal designs;

• to provide the basis of a formal architecture description language for Fractal;

• to allow a formal specification and verification of Fractal tools;

• to allow a rigorous comparison with other component models.

The latter is important because the Fractal specification aims to define a very general component model (e.g., meta-level capabilities in Fractal are not fixed, nor is the semantics of composition realized by composite components), from which more specialized component models can be derived and combined. A formal specification can INRIA thus help in assessing whether a component model constitutes a proper refinement or specialization of the Fractal model.

Alloy The specification in this report is written in Alloy 4 [START_REF]Alloy Analyzer Web Site[END_REF][START_REF] Jackson | Alloy: A Lightweight Object Modelling Notation[END_REF][START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF], a lightweight specification language based on first-order relational logic. Alloy is interesting because of its simplicity and because of the straightforward usage of its analyzer, which acts essentially as a model checker and counter-example generator, and which enables rapid iterations between modelling and analysis when writing a specification (very much akin to debugging a specification). For a detailed introduction and motivation of Alloy, we refer the interested reader to the book [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF]. An online tutorial for Alloy is also available on the Alloy Analyzer Web site [START_REF]Alloy Analyzer Web Site[END_REF].

Presentation The report is written in a litterate programming style: the specification is presented in its entirety, the (informal) commentary on the formal specification being interspersed with excerpts of the Alloy code. All assertions (Alloy facts) and theorems (Alloy assertions) have been checked with the Alloy analyzer, checking for the existence of finite models in the first case, and for the absence of counter-examples in models below a certain size in the second case. We do not introduce Alloy nor the Fractal model. Hopefully, the commentary running along the Alloy code excerpts will suffice.

Organization The report is organized as follows. Section 2 discusses related work. Section 3 details the Alloy specification of the core Fractal concepts. Sections 4 to 8 detail the Alloy specification of the different elements of the Fractal model, including the naming and (distributed) binding framework which is an integral part of Fractal (Section 4), the optional component controllers (meta-level functions) defined in the informal Fractal specification (Sections 5 and 6), the notion of component factory and bootstrap conditions for a Fractal system (Section 7), and the optional type system (Section 8). Section 9 shows that the overall specification is consistent, i.e., that there exists a model for a component that combines all the features specified in Sections 3 to 8. Section 10 contrasts the formal specification presented in this report with the informal one, highlighting areas (and motives) of divergence between the two. Section 11 concludes the report with a mention of future work.

Related work

There have been several approaches to the formalization of component-based software and component models. Representative samples are provided by the two books [START_REF] Leavens | Foundations of Component-Based Systems[END_REF][START_REF] Liu | Mathematical Frameworks for Component Software -Models for Analysis and Synthesis[END_REF]. The two bodies of work closest to ours are: the co-algebraic approach developed by Barbosa, Meng et al. [START_REF] Barbosa | State-based Components Made Generic[END_REF][START_REF] Barbosa | On the Semantic of Componentware: A Coalgebraic Perspective, volume 2 of Component-Based Software Development[END_REF][START_REF] Meng | A Coalgebraic Semantic Framework for Component-based Development in UML[END_REF][START_REF] Meng | Components as Coalgebras: The Refinement Dimension[END_REF], and the formal specification in Alloy of Microsoft COM component model developed by Jackson and Sullivan [START_REF] Jackson | COM Revisited: Tool-Assisted Modelling of an Architectural Framework[END_REF], following work by Sullivan et al. on the formal specification of the COM model in Z [START_REF] Sullivan | Analysis of a Conflict between Aggregation and Interface Negotiation in Microsoft's Component Object Model[END_REF].

Although the presentation we give is relational, the notion of component or kell we develop in this report is essentially coalgebraic in nature since a kell can be understood primarily as a set of transitions. Whereas Barbosa et al. develop a categorical framework, we prefer to adopt a simpler set-based approach: while we lose the benefit of dealing in the same way with multiple forms of behavior (e.g., probabilistic, timebased, etc.) as in [START_REF] Barbosa | State-based Components Made Generic[END_REF], the intuition is in our view better aided by a set-based presentation, and it is easier to understand for it directly generalizes the well-known notion of transition system. The COM specification presented in [START_REF] Jackson | COM Revisited: Tool-Assisted Modelling of an Architectural Framework[END_REF] focuses on the structural aspects of the COM model, and notably on the definition of its query interface and aggregation mechanism. While the Component controller in the Fractal specification provides much the same functionality as the query interface in COM, the Fractal model does not exhibit the COM-specific difficulty arising in the interplay between query interface and aggregation highlighted in [START_REF] Sullivan | Analysis of a Conflict between Aggregation and Interface Negotiation in Microsoft's Component Object Model[END_REF], and possesses several forms of meta-level behavior (so-called controllers and controller interfaces). Thus, our work deals with a richer component model than the COM one, and deals in particular with the specification of meta-level behavior that subsumes and extends that of the COM model. A recent work [START_REF] Simonot | Modélisation formelle du contrôle en Fractal[END_REF] presents a first-order relational logic formalization of the Fractal component model. The consistency of a part of this specification is proven manually while the consistency of our specification is checked by the Alloy Analyser. Moreover, this work deals only with certain structural aspects of the Fractal specification, while the present report covers the whole informal Fractal specification. Especially, AttributeController, ContentController, SuperController, NameController, GenericFactory, Factory, and TypeFactory interfaces are not formally specified in [START_REF] Simonot | Modélisation formelle du contrôle en Fractal[END_REF].

Foundations

This first part of the specification captures the underlying core of the Fractal model: a very general notion of component, called kell (a remote reference to the biological cell). At this level of abstraction, the notion of kell first emphasizes two facts:

• A kell has entry points, called gates. The notion of gate is an abstract form of the notion of interface in the Fractal specification. A gate constitutes a named point of interaction between a kell and its environment. The set of gates of a kell constitutes its sole means of interaction with its environmenti.e., a kell is a unit of encapsulation.

• A kell may have subcomponents, called subkells. All transitions in a kell may act on the set of subcomponents, and modify it in arbitrary ways. This flexibility is key to allow different semantics for composition, and to support different kinds of meta-level operationsi.e., operations operating on the internal structure and behavior of components.

The first primitive sets in the Alloy specification of the core Fractal model are given below 1 . A gatei.e., an element of the set Gate -is an entry point to communicate with a kell. The declaration above stipulates that a gate has an identifier 3 . A kelli.e., an element of the set Kell -is defined as having an identifier, given by the feature kid, a set of gates, given by the feature gates, and a set of sub kells, given by the feature sc. The fact that a kell has an identifier is necessary (e.g., for management purposes) to manifest a notion of identity that persists throughout state changes. The Alloy fact named GatesInKellHaveUniqueIds expresses an invariant on kells 4 , namely that gates belonging to a kell have distinct identifiers. called signatures in Alloy, hence the keyword sig for introducing them. Note also the module declaration: in Alloy, specifications can be broken down into modules, which can then be imported for use in other modules using a declaration of the form: open moduleX as X, where X is some local name used, in the current module, as an abbreviation for the imported module. 2 Keyword extends in Alloy indicates that a primitive set is declared as a subset of another one (and that it will form, with other subsets similarly declared, a partition of the set it extends). 3 In Alloy, a declaration of the form gid:Id can be read as declaring a feature, or instance variable, of the class Gate; formally, it declares a binary relation gid : Gate → Id between the set of gates, Gate, and the set of identifiers, Id. 4 This invariant takes the form of a simple first-order logical formula, where the keyword all denotes the universal quantifier ∀, where a declaration such as c:Kell denotes an arbitrary element c of the set Kell (likewise, i:c.gates denotes an arbitrary element i of the set of gates of the kell c -the dot notation c.gates is the standard notation for accessing a feature, or attribute, of an instance of a class). In a more classical logical notation, the GatesInKellHaveUniqueIds formula would read:

∀c ∈ Kell, ∀i, j ∈ gates(c), gid(i) = gid(j) =⇒ i = j RR n°6721
These elements provide the basic structure of a kell but do not explain how it behaves. This is captured by the definition of the set TKell below, a subset of Kell5 , which endows kells with transitions. Transitions are defined below as 4-tuples that comprise a set of initial kells (feature tsc), a set of input signals (feature sin), a set of output signals (feature sout), and a set of residual kells (feature res). Intuitively, the initial set of kells of a transition corresponds to subkells of the kell to which the transition belongs (the set of subkells on which the transition acts). The set of residual kells are the kells produced by the transition. The kell to which the transition belongs may or may not belong to the residual of the transition. This allows us to model component factories, as in the Fractal specification, i.e., component that can create other components, or operations that delete or transform the target component. Effectively, this means that a kell can be seen as some sort of generalized Mealy machine (a labelled transition system, whose labels denote input and output signals handled during a transition). Signals are defined below as records of arguments (feature args), with a target gate (feature target), i.e., the gate at which a signal is received (if it is an input signal) or emitted (if it is an output signal), and an operation name (feature op). In object-oriented terms, a signal looks very much like a reified method invocation. Signal arguments belong to the set Arg defined above as the union of four sets: identifiers, values, gates and kells. This means in particular that signal may carry gates (much as in the π-calculus messages may carry channel names 6 ), and kells. The latter capability is not explicitly reflected in the Fractal specification, but is required to model mobile agents and strong mobility, as well as deployment, checkpointing and reconfiguration capabilities 7 . The fact SignalsTargetGates expresses the invariant that all target gates in signals appearing in transitions of a kell c are gates of c.

Discussion

This completes the specification of the core Fractal model. As can be seen the core is very small, and it merely asserts that components are higher-order Mealy machines, that can be hierarchically organized. This core model allows a number of seemingly unusual, or unexpected, features:

• We allow kells to have no gates, and thus only internal behavior. As a result, the following assertion 8 is not valid:

assert AllKellsHaveGates { all c:TKell | some c.gates }

In contrast, the following assertion is valid:

assert NoGateImpliesInternalActions { all c:TKell | (no c.gates) implies (no c.transitions.(sin + sout) ) }
It asserts that if a kell has no gate, then its transitions are merely internal as they involve no exchange of signals with the environment.

• We allow component structures with sharingi.e., a kell may be a subkell of two different kells. Thus, the following assertion to the contrary is invalid:

assert SharingIsImpossible { all c1,c2:Kell | no cs:Kell { cs in c1.sc & c2.sc and (not c1 = c2) and (not c1 in c2.sc) and

(not c2 in c1.sc) } }
Component sharing is an original feature of the Fractal model, which as been found useful to model situations with resource sharingi.e., where components at different places in a component hierarchy need access to the same resource, such as a software library, or an operating system service.

(i.e., no operation will transform a gate into another with the same identifier). Having a gate identifier or a gate itself as an argument are thus strictly equivalent, but allowing gates as signal arguments simplifies the specification. 7 Alternatively, one could model this through marshalling and unmarshalling operations, allowing to transform a kell into a value, and vice versa. The above specification of arguments makes this higher-order character of signals and of the kell model explicit. 8 An assertion in Alloy is written exactly like a fact, except for the use of the assert keyword to declare it. An invalid assertion is detected by the Alloy Analyzer when it generates a finite model that contradicts it (a counterexample). The Alloy keyword some denotes the existential qualifier. Thus, some c:Kell | P where P is some predicate, asserts the existence of some kell c verifying P. By extension, some s, where s is a set, asserts that s is not emptyi.e., that there is some element in s.

• We allow component structures that are not well-foundedi.e., where a kell may appear as a subkell of itself, or as a subkell of some of its subkells, etc. Thus, the following assertion to the contrary is invalid 9 :

assert ContainmentIsWellFounded { all c:Kell | (not c in c. * sc) }
This may seem counterintuitive, however this is not really different from allowing recursive procedure calls, and we therefore do not enforce it at the level of abstraction of the core model. The Fractal specification explicitly disallows this (ContainmentIsWellFounded would be written as an invariant -an Alloy fact), but this feature could be interesting to model recursive component structures. This is one occurrence where the present formal specification relaxes the constraints from the informal Fractal specification.

• We allow components to have a varying number of interfaces during their lifetimei.e., kells to have a varying number of gates in the course of their execution. Thus, the following assertion to the contrary is invalid: • In contrast to most other component models (see e.g., [START_REF] Lau | Software Component Models[END_REF] for a discussion of recent ones), we do not need to introduce a notion of connector or binding to mediate the communication, or reify the communication paths, between components. Sharing, containment (i.e., the kell-subkells relationship) and the fact that each component or kell institutes its own composition semantics suffice to make explicit communication channels in a component structure, and to define their semantics.

The specification of kells as Mealy machines has however one major drawback as an Alloy specification. Because transitions make explicit the state changes that a kell may go through, specifying state changes in the present specification amounts to require that certain facts hold, which would take the form of closure properties, such as "kells of this kind -and the kells that appear in the residues of their transitions -must have transitions of this sort". For instance, we would require all kells that support the Component gate to have certain transitions implementing the Component operations, and all the kells in the residues of their transitions to be kells of a similar kind. Closure properties of this kind are unfortunately instances of so-called generator axioms that may lead to a state explosion in models of the specification, which makes them impossible to analyze using the model checking approach of the Alloy Analyzer. This problem is an instance of the unbounded universal quantifiers problem discussed in Section 5.3 of [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF], and needs to be avoided if we want to exploit the Alloy Analyzer in assessing the consistency of the specification. Our approach in this specification is to not describe explicitly the set of transitions logically associated with a kell. Instead, we will define Alloy predicates that describe state changes on certain kells, but refrain from imposing that these state changes appear as explicit transitions in the supporting kells. In effect, for the purposes of this specification, we will deal only with elements of the Kell set, and will not consider elements of the TKell set. In the following sections, we adopt this approach: all properties and predicates considered will deal apply to elements of Kell. Before moving to the specification of the (optional) default meta-level capabilities of the Fractal model, we gather here a number of declarations used in the rest of the specification. The distinction between Client and Server is here merely a primitive type distinction, which governs bindings between gates: to bind two gates together, one must be a dual of the other. The denominations Client and Server merely reflect that duality. The predicate isoKell can be interpreted as a strong identity predicate, whereby two kells are strongly identical if they have the same identifier, the same gates and the same subkells (they may differ in their internal state).

Naming and binding

The naming and binding part of the specification captures the notions necessary for the construction of distributed configurations. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 2.2.

The first concept is that of name. A name is merely an entity that is used to refer to another one. A name comes equipped with a reference to its naming context (feature A name can also be pickled (or marshalled) to make it persistent or to communicate it between different machines. This is obtained through the combination of the pack feature and of operations encode and decode10 , defined as follows: The feature exported in a naming context identifies the association between names in the context and their referents 11 .

Two key invariants, given below, apply to names and contexts 12 . The first one merely asserts that names appearing in a context correctly refer to this context. The second one clarifies the fact that referents cannot be names that belong to the context (they can be names that belong to other contexts, though, thus allowing referral chains to be constructed across multiple contexts). The main operation supported by a naming context is the export operation. Operation export returns a new name n for referent r in context nc. The name n is a valid name for referent r in the context nc. The naming context nc can for instance be a network context where remotely accessible interfaces are given names of a special form (e.g., URLs for a Web service context). Note that a name can be exported as well. This is necessary to handle names across different naming contexts. A referent that is already a name in the target context cannot be exported. Operation export is specified below 13 . The following assertions highlight the fact that name resolution within a single naming context can be partial. To be complete, name resolution must typically take place across several naming contexts. However, we also allow partial name resolution across several naming contexts. This takes care of situations were name resolution cannot be carried out in full (e.g., in disconnected situations) or need not be carried out in full (e.g., when no access to a referenced interface or component is attempted). A binder is a naming context that can resolve names and establish connections (bindings) towards entities referred to by resolved names. A binding is created typically by a bind operation. The creation of a binding results in the creation of a component that provides a (local) interface which corresponds to (e.g., is a proxy to) the resolved name. A binder records the association (bindings) between resolved names and the (local) interfaces they refer to. Binders are specified below. The bind operation is specified below, together with some self-explanatory properties.

Basic introspection

The component controller in Fractal supports basic introspection capabilities: discovering all the interfaces associated with a component and their type. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 3.

Our formal specification of the component controller begins with the declaration of the Type signature, with its subtype relation, noted sstypes. At this level of abstraction, the only property recorded of the subtype relation is that it constitutes a partial order 14 . The specification of the above operations provide examples of ambiguities that arise in the informal Fractal specification (in fact, in any informal specification), and which are difficult to weed out without a formal model. In fact, [START_REF] Bruneton | The Fractal Component Model[END_REF] leaves unspecified the exact postconditions of operations. Here we strike a middleground between a strong form which would require that the target compkell be left untouched, i.e., that would specify c = c1 in place of our isoCKell[c,c1], and a very weak form which would only require c.kid = c1.kid. The strong form would forbid any kind of side-effect to such meta-level operations (such as setting a counter or updating a log of such operations), whereas the very weak form would make these introspection operations essentially useless (since the obtained information would be obsolete as soon as it is obtained).

module
We specify below operations associated with an Interface gate. The informal Fractal specification does not define operations for the AttributeController interface. However, the informal specification defines a convention for defining application-specific attribute controllers. We now give an example of how to formalize this convention. This example component provides both getter and setter operations for a foo property. We define two signatures: ExampleAttributeController as a subset of Attribute Controller gates, and ExampleKell as a subset of ackells containing the foo field and where the attribute controller is an ExampleAttributeController gate. We specify below the getter and setter operations for the foo property.

Binding control

The BindingController interface in Fractal supports the binding of client interfaces of a component to server interfaces. The effect of this binding is to allow the components that are connected via these bound interfaces to communicate. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.3.

In our case, we do not specify the exact effect of binding a client and a server gate, since the semantics of this binding typically depends on the enclosing component where it takes place. However kells providing a BindingController gate record which client interfaces are bound (feature bindings in an instance of BCKell). Notice the different constraints that apply:

• a client gate is bound at most to a single server gate (lone multiplicity in bindings feature declaration);

• client gates must be gates of the hosting kell (fact ClientsInBindingCntrlAreBCKellGates);

c1.comp = c2.comp implies c1 = c2 c1.kid = c2.kid implies c1 = c2 } } assert CCKellsHaveCompAsIdsInSubComps { all c:CCKell | all c1,c2:c.subcomps { c1.kid = c2.kid <=> c1.comp = c2.comp } }
As mentioned previously, the Interface interface contains the operation isInternal, which returns true if an interface i is an internal interface or false if it is an external interface. We now define an equivalence predicate on cckells. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, the same ContentController gate, the same internal interfaces, and the same subcomponents. We then define the set LFKell that offers a LifecycleController gate. The feature ctrls identifies the set of "control" gatesi.e., those gates whose operations are not inhibited when in the Stopped state. We define first an equivalence predicate between kells with LifecycleController gates. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, the same LifecycleController gate, the same macro-state, and the same control gates. We specify below the operations attached to LifecycleController gates. Operation getState returns the macro-state s of the kell hosting the target LifecycleController gate lfc. Operation start places the kell c hosting the target LifecycleController gate lfc into the Started macro-state. Operation stop places the kell into the Stopped macro-state. This may imply all sorts of changes in c, hence the weak constraint on the resulting kell c1: it has the same identifier than c, and the same LifecycleController interface, and it is in the Started or Stopped macro-state respectively.

Factories

The Fractal model has two notions of component factories: a generic one, and a specific one. A generic factory is able to create arbitrary components from a type, a description of their content, and a description of their membrane (or set of controllers). A factory is only able to create components of a certain type. We specify these notions formally below. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 5.

We first define the notion of factory. By definition, a factory is a component, hence a kell, that exhibits a Factory interface. A factory is specific to a component type, a controller description, and a content description. The notions of controller description and content description are just defined as simple signatures ControllerDesc and ContentDesc, with no further constraint 16 . We define first an equivalence predicate between kells with Factory gates. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, the same Factory gate, the same instance type, the same controller and content descriptions.

isSubInterfaceTypeOf[it1, it2] and isSubInterfaceTypeOf[it2, it3] implies isSubInterfaceTypeOf[it1, it3] } } assert IsSubComponentTypeOfIsReflexive { all ct:ComponentType { isSubComponentTypeOf[ct, ct] } } assert IsSubComponentTypeOfIsTransitive { all ct1, ct2, ct3:ComponentType { isSubComponentTypeOf[ct1, ct2] and isSubComponentTypeOf[ct2, ct3] implies isSubComponentTypeOf[ct1, ct3] } }

Consistency

We have developed in the previous sections a formal specification of the Fratal component model. It mirrors the informal specification pretty truthfully (see Section 10 for a list of the differences between the two), and it has been written in a modular fashion, keeping the different controllers as independent from one another as possible, again following the philosophy of the informal specification. One may wonder however, whether the combination of all these different features in a single component may not give rise to inconsistencies. The following simple predicate, which asserts the existence of a component supporting all the different controllers defined in the present specification, can be shown to have an instance (and hence to be consistent). Specifically, the command listed below produces a kell which is an element of all the different sets listed below (ACKell, etc.). Note that a lesser scope (e.g., a scope of 9 instead of 10 in the command) is not enough to obtain a model. We discuss in this section the main differences between the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF] and the present formal one. We also comment briefly on the use of Alloy and of the Alloy Analyzer.

Differences with the informal specification

Foundations The first difference with the informal specification is the elucidation of the core concepts found in the Foundations (Section 3). The informal specification only refers to them in passing, yet making them explicit is key to highlighting the generality of the Fractal model. In particular, they enable us to define precisely the general notion of behavior that can be expected from Fractal components. In formalizing these foundations, we have also clarified features of the Fractal model and on purpose relaxed certain constraints that appear in the informal specification. We list them below. Note that we flag explicitly each feature mentioned as an extension or as a clarification.

• [ extension ]

We allow component graphs (corresponding to the subcomponent relation) to be arbitrary graphs. This means that we can have structures with sharing, but also non-well-founded structures, such as components which are in their own subcomponents. Non-well-founded structures are explicitly ruled out by the informal specification. We believe this to be an unnecessary restriction as non-well-founded structures can be usefule.g., in modelling reflective component structures.

• [ clarification ] We allow components to be passed by value in operations. This feature is not discussed in the informal specification, but the heavy Java bias of the IDL used in the informal specification does not explicitly cater for it.

• [ clarification ] We allow components to have a varying number of interfaces during their lifetime. This feature was not explicitly disallowed in the informal specification, but the Julia reference implementation does not support it.

General and specific differences We list below enhancements which the formal specification brings to the informal one, and a difference between the two specifications:

• [ clarification ] Pre and post-conditions of operations on the different interfaces defined in the specification are made explicit. For instance, the post-conditions on operations of the Component interface specify that the target component identity, gates (interfaces) and subcomponents must remain unchanged (through the use of the isoKell predicate). The informal specification is not explicit on these conditions.

• [ clarification ] The present specification clarifies the admissible effects of operations not only through operations pre-and post-conditions but also by highlighting valid and invalid assertions. Witness for instance the different commutation properties and invalid assertions listed for side-effects of the ContentController and LifecycleController interfaces. The informal specification does not contain such a breadth of details on operations.

• [ clarification ] The subtyping relation used in basic introspection and typing is specified as being a partial order on types. The informal specification does not enforce this constraint. However, having a notion of subtyping that is not a partial order makes little sense.

• [ clarification ] The present specification enforces the unicity of the Component interface of a component, if it exists. We do not enforce the unicity of other kinds of controller interface. The unicity of the Component interface highlights the fact that it acts as an identity for a component. The informal specification is ambiguous on the unicity of controller interfaces.

• [ clarification ] The getInterfaces operation in basic introspection (Section 5) returns all the external interfaces of the target component. The informal specification is evasive on that subject. We believe this form is preferable for introspection purposes.

• [ difference ] The informal specification distinguishes between three kinds of bindings. We have left out this distinction in the formal specification, since it is essentially a classification with no operational import.

Modularity of the specification

The Fractal model and its informal specification promote a philosophy of separation of concerns, including between meta-level capabilities. The Alloy module system and Alloy's set-based inheritance features allowed us to follow this design philosophy, and to specify the Fractal model in a very modular way. Each of the module of our Alloy specification imports at least the foundations module (Section 3), since this module defines the core concepts common to all other modules, and at most the component module (Section 5), which provides basic introspection capabilities. The table below summarizes the dependencies between modules. This report can be seen as a vindication of the modularity claim of the Fractal specification. However, we have highlighted that there exists one dependency that breaks this modularity between controllers: the Interface interface contains an isInternal operation related to internal interfaces. We therefore think that this operation should be removed from the next version of the Fractal specification to preserve orthogonality between the different component controllers.

Using Alloy

Alloy fulfills its promise (discussed in [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF]) of providing a fast specification development / specification debugging loop, thanks to the fully automatic character of the Alloy Analyzer. Coupled with a fast learning curve due to its first-order, set-based character, a well-thought out syntax, and extremely useful model visualization features in the Alloy Analyzer, developing specifications with Alloy is a very streamlined, and even enjoyable, process. The surprising amount of bugs (trivial or not), that were weeded out from the specification thanks to this rapid feedback loop, especially during the early stages of its development, is a testament to the efficacy and efficiency of the lightweight specification approach advocated by the Alloy designers.

Our use of Alloy is mostly classical. We have adopted an operational style for the specification of the different Fractal controllers, since this was both closer to the informal specification and the most natural style for the specification of mostly serverlike behavior. We have made an abundant use of invalid assertions in order to signal possibly unexpected side effects or behavior of operations. Because of the purposedly weak semantics for operations adopted in the Fractal specification (which we have kept in the present work), we find these negative assertions to be invaluable to debunk misconceptions about the specification.

The one limitation of Alloy for our specification exercise is in the specification of mathematically oriented structures such as our notion of transition for the specification of component behavior. Unfortunately, we have had to eschew the use of transitions to characterize the behavior of components: this would have led us to systematically introduce closure conditions (see the discussion in Section 3); this would have, in turn, led to an explosion in the size of our models. For the most part, this does not constitute a hindrance, since we can capture the intended semantics of component operations using standard Alloy predicates. In one instance, however (the specification of the LifecycleController operations), the specification of the intended semantics could only be achieved by an explicit characterization of a component behavior in terms of transitions. For this kind of specification, dealing with conditions on mathematical structures, a higher-order theorem prover such as Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions[END_REF] is probably much more suited.

Conclusion

We have presented in this report a comprehensive formal specification of the Fractal component model, that covers all the elements of the original informal reference specification of the Fractal model. The formal specification is written in Alloy, a simple and natural (for object-oriented modellers) formal specification language. We have used the Alloy Analyzer to check the consistency of the model, its key invariants, and several properties. Compared to the informal one, the formal specification given in this report has several advantages:

• It provides a formal description of the foundations of the Fractal component model, which are only alluded to in the informal specification.

• It is more liberal than the informal one in a number of aspects (e.g., allowing components to be passed by value in operations).

• It provides a truly language-independent specification of the Fractal component model.

• It removes ambiguities from the informal specification, notably in the specification of the post-conditions of the controller operations.

We have concentrated in this report on providing a formal equivalent of the full informal Fractal specification, just leaving aside a formal specification of the notion of normal, export, import binding and of template (which will be covered by future work on a new Fractal ADL). We plan to extend this work in several directions, however:

• Using this specification as a basis for the development of a new ADL for Fractal, with a formal semantics.

• Extending this specification to cover concepts and constraints related to the handling of component packages and the specification of distributed deployment processes.

• Extending this specification to describe, formally and abstractly, meta-level and aspectual capabilities of current Fractal implementations, including the specification of component-based membranes [START_REF] Seinturier | A Component Model Engineered with Components and Aspects[END_REF].

• Using this specification for showing formally how several component models can be understood as Fractal personalities or Fractal specializations.

sig

  TKell in Kell { transitions: set Transition } sig Transition { tsc: set Kell, sin: set Signal, sout: set Signal, res: set Kell } fact TransMayNotHaveDifferentSubComps { all c:TKell | all t:c.transitions | t.tsc = c.sc } The invariant TransMayNotHaveDifferentSubComps ensures that the initial kells associated with each transition of a given kell c are indeed the subkells of c.

  sig Signal { target: Gate, operation: Op, args: Id -> set Arg } sig Arg in Id + Val + Gate + Kell {} fact SignalsTargetGates { all c: TKell | c.transitions.(sin + sout).target in c.gates }

  assert NumberOfGatesInKellDoesNotVary { all c:TKell | all t:c.transitions | all cr:TKell { (cr in t.res and cr.kid = c.kid) implies (cr.gates = c.gates) } }

  open util/relation as RR open fractal/foundations as FF sig Name { context: Id, pack: NamePickle } sig NamePickle { unpack: Name, context: Id } RR n°6721

fact

  PackUnpackIdempotent { all n:Name | n.pack.unpack = n } pred encode(n:Name, p:NamePickle, n1:name) { n1 = n p = n.pack } pred decode(nc:NamingContext, p:NamePickle, n:Name, nc1:NamingContext) { nc1 = nc p.context = nc.nid and p.unpack.context = nc.nid implies n = p.unpack } assert DecodingYieldsSameNameThanEncoded { all p:NamePickle, n:Name, nc:NamingContext { encode[n,p] and nc.nid = n.context implies decode[nc,p,n] } } Names exist only within contexts. Contexts are primarily associations between names and referentsi.e., entities which are refered to by names. Making contexts explicit allows us to define different systems of names and to have them coexist and cooperate without the need to rely on a global naming authority to disambiguate independently created names. Contexts are defined as follows: sig Referent in Gate + Name {} sig NamingContext { nid: Id, exported: Name -> lone Referent }

fact

  NameRefersToContext { all nc:NamingContext | all n:dom[nc.exported] | n.context = nc.nid } fact InContextNamesNotExported { all nc:NamingContext | all n:ran[nc.exported] | n.context != nc.nid }

  one sig NamingException extends Val {} pred export(nc1, nc2: NamingContext, r: Referent, n:Name + NamingException) { let A = not (some s:Referentr | n->s in nc1.exported), B = (not r.context = nc1.nid) { (A and B) implies nc2.exported = nc1.exported + n -> r and nc1.nid = nc2.nid else n in NamingException and nc1 = nc2 } } One may verify a number of properties in relation to operation export. Here are a few self-explanatory ones: assert ExportReturnsNewNameOrOldMap { all nc,ncc:NamingContext, r:Referent, n:Name | export[nc,ncc,r,n] implies let A = (not n in dom[nc.exported]), B = (n.(nc.exported) = r), C = (not r.context = nc.nid) { (A or B) and C } } assert ExportNameBelongsToContext { all nc,ncc:NamingContext, r:Referent, n:Name | export[nc,ncc,r,n] implies n.context = nc.nid } assert ExportExceptionLeavesContextUnchanged { all nc,ncc: NamingContext, r:Referent, n:NamingException | export[nc,ncc,r,n] implies nc = ncc }

assert

  ExportClosureIsJustExport { all nc:NamingContext | nc.exported = ˆ(nc.exported) } assert ExportClosureEndsInInterfaceOrNotInContextName { all nc:NamingContext, n:Name, r:Referent | r in n.(nc.exported) implies (r in Gate) or (r in Name and r.context != nc.nid) }

sig

  Binder extends NamingContext { bindings: Name -> lone Gate, } fact BindingNamesBelongToContext { all b:Binder | all n: dom[b.bindings] | n.context = b.nid } fact BindingsAndExportedDomainsDisjoint { all b:Binder | no (dom[b.bindings] & dom[b.exported]) }

  pred bind(b,b1:Binder, n:Name, i:Gate + NamingException) { b.nid = b1.nid n -> i in b.exported implies b = b1 else i in Gate implies b1.bindings = b.bindings + n -> i else i in NamingException and b = b1 } assert BindExceptionLeavesBinderUnchanged { all b,b1:Binder, n:Name, i: NamingException | bind[b,b1,n,i] implies b = b1 } assert BindReturnsNewInterfaceOrFromExported { all b,b1:Binder, n:Name, i:Gate | bind[b,b1,n,i] implies n -> i in b.exported + b1.bindings } Finally, one can prove a correct interplay between export and bind, namely that bind returns a local (in-context) gate referred to by a previously exported name. assert BindReturnsPreviouslyExportedReferent { all b,b1:Binder, n:Name, i:Gate | INRIA export[b,b1,i,n] implies bind[b1,b1,n,i] }

sig

  CKell in Kell { comp: Component } getInterface returns the gate i whose identifier iid is passed as argument to the operation. In the process, compkell c becomes compkell c1. Operation getCType returns the component type ct of compkell c. // Operations from the Component interface pred getInterfaces(c:CompKell, o:Component, is: set Interface, c1:CompKell) { o = c.comp is = c.gates isoCKell[c,c1] } pred getInterface(c:CompKell, o:Component, iid:Id, i:Interface + NoSuchInterfaceException, c1:CompKell) { o = c.comp isoCKell[c,c1] i in c.gates implies iid = i.gid else i = NoSuchInterfaceException } pred getCType(c:CompKell, o:Component, ct: ComponentType, c1:CompKell) { o = c.comp ct = o.ctype isoCKell[c,c1] }

  pred getFoo(c:ExampleACKell, ac:ExampleAttributeController, r:Val, c1:ExampleACKell) { c.actrl = ac r = c.foo isoACKell[c,c1] } pred setFoo(c:ExampleACKell, ac:ExampleAttributeController, v:Val, c1:ExampleACKell) { c.actrl = ac c1.foo = v isoACKell[c,c1] } Finally we give a consistency property on these two operations. assert GetFooAfterSetFoo { all c,c1: ExampleACKell, v:Val | setFoo[c, c.actrl, v, c1] implies getFoo[c1, c1.actrl, v, c1] }

sig

  ContentController extends Server {} sig CCKell in Kell { cctrl: ContentController, internals: set Gate, subcomps: set CKell } fact ContentControllerInCCKellIsExternalGate { all c:CCKell | c.cctrl in c.gates } fact InternalsAreNotExternalsInCCKells { all c: CCKell | no (c.internals & c.gates) } fact SubcompsAreSubComponentsInCCKells { all c: CCKell | c.subcomps in c.sc } fact InternalsIdsAreDistinct { all c:CCKell | all g,g1:c.internals | g.gid = g1.gid implies g = g1 } fact CCKellsHaveDistinctComponentsInSubComps { all c:CCKell | all c1,c2:c.subcomps {

/

  / Operation from the Interface interface pred isInternal(c:CompKell, i:Interface, c1:CompKell) { c in CCKell and i in c.internals isoCKell[c,c1] }

  pred isoCCKell(c:CCKell, c1:CCKell) { isoCKell[c,c1] c.cctrl = c1.cctrl c.internals = c1.internals c.subcomps = c1.subcomps } We specify below the different operations attached to a ContentController gate. Operation getInternalInterfaces returns the set of internal interfaces of the cckell hosting the target ContentController gate. Operation getInternalInterface returns the internal gate whose identifier iid is passed as argument. Operation getSubComponents returns the set scc of subkells accessible via the ContentController gate. Operation addSubComponent adds a sig LFState extends Val {} one sig Started extends LFState {} one sig Stopped extends LFState {}

sig

  LifeCycleController extends Server {} sig LFKell in Kell { lfctrl: LifeCycleController, state: LFState, ctrls: set Gate } fact LFCtrlIsACntrlGate { all c:LFKell | c.lfctrl in c.ctrls } fact CtrlGatesAreInGates { all c:LFKell | c.ctrls in c.gates } fact LFStateIsStoppedOrStarted { all c:LFKell | c.state in Started + Stopped }

  pred isoLFKell(c:LFKell, c1:LFKell) { isoKell[c,c1] c.lfctrl = c1.lfctrl c.state = c1.state c.ctrls = c1.ctrls }

/

  / Operations from the LifecycleController interface sig LFReturn in Ok + IllegalLifeCycleException {} pred getState(c:LFKell, lfc:LifeCycleController, s:LFState, c1:LFKell) { c.lfctrl = lfc s = c.state isoLFKell[c,c1] } pred start(c:LFKell, lfc:LifeCycleController, r:LFReturn, c1:LFKell) { c.lfctrl = lfc r = IllegalLifeCycleException implies isoLFKell[c,c1] else c.state = Started implies r = Ok and isoLFKell[c,c1] } } assert StopPreservePreviousGates { all c,c1:LFKell { stop[c,c.lfctrl,Ok,c1] implies c1.gates = c.gates } } 7 Instantiation

module fractal/foundations sig Id {} sig Val {} sig Op extends Id {} The

  above declarations introduce three primitive sets: Id, Val, and Op. They correspond to the set of identifiers, base values, and operation names respectively. Identifiers are just primitive forms of names or references. Base values represent values of some (unspecified) data types, such as integers, booleans, strings, etc. At this level of abstraction, the exact forms base values can take is of no import, hence their specification as just atoms2 .The general notions of interface and component in the core Fractal model are given below. They are called, respectively, gate and kell.

	sig Gate {
	gid: Id
	}
	sig Kell {
	gates: set Gate,
	sc: set Kell,
	kid: Id
	}
	fact GatesInKellHaveUniqueIds {
	all c:Kell | all i,j:c.gates | i.gid = j.gid implies i = j
	}

  The next signatures declare the Component gates and the Interface gates. A Component gate is a server gate which also records the type of the component it belongs to. An Interface gate records its type, as well as the Component gate of the component it belongs to. As noted in the informal Fractal specification, this setting is similar to that adopted by the Microsoft COM model, with Component corresponding to the COM IUnknown interface.A ckell is now defined as a kell with one gate which is an instance of Component (its other gates can be arbitrary gates). The fact CKellsHaveComponent constraints ckells to have only one Component gate.

	sig Component extends Server {
	ctype: ComponentType
	}
	sig Interface in Gate {
	owner: Component,
	itype: InterfaceType,
	}

fractal/component open util/relation as RR open fractal/foundations as FF open util/graph[Type] as GG sig Type extends Val { sstypes: set Type } fact SubTypingIsPartialOrder { GG/dag[sstypes] } sig ComponentType extends Type {} sig InterfaceType extends Type {}

  Operation getOwner returns the Component gate associated with the compkell c that hosts the target Interface gate i. Operation getName returns the identifier of the target Interface gate i. Operation getType returns the interface type it of the target Interface gate i.

	// Operations from the Interface interface
	pred getOwner(c:CompKell, i:Interface, o:Component, c1:CompKell) {
	i in c.gates
	o = i.owner
	isoCKell[c,c1]
	}
	pred getName(c:CompKell, i:Interface, iid:Id, c1:CompKell) {
	i in c.gates
	iid = i.gid
	isoCKell[c,c1]
	}
	RR n°6721

as FC sig ContentDesc extends Val {} sig ControllerDesc extends Val {} sig Factory extends Server {} sig FKell in Kell

	module fractal/instantiation
	open fractal/foundations as FF
	open fractal/component {
	fg: Factory,
	insType: ComponentType,
	ctrlDesc: ControllerDesc,
	cntDesc: ContentDesc
	}
	fact FactoryInFKellIsExternalGate {
	all c:FKell | c.fg in c.gates
	}

RR n°6721

In Alloy, primitive sets are just sets of atomsi.e., elements which have no internal structure (and are not sets -atoms are sometimes called urelements in the logic litterature, e.g., as in[START_REF] Barwise | Vicious Circles[END_REF]). Primitive sets are INRIA

In Alloy, in denotes the subset relation, or the set membership relation, + denotes set union, & denotes set intersection, -denotes set difference, # denotes set cardinality.

Note that in the π-calculus, channels, i.e., communication capabilities, are just names. Strictly speaking we could have avoided to include gates as possible arguments to signal, by just relying on identifiers. However, we have been careful in the specification to ensure that gates remain immutable, in contrast to kells INRIA

In Alloy, * r of some relation r denotes the reflexive and transitive closure of r, while ˆr denotes its transitive closure.INRIA

Alloy allows the definition of first-order predicates, whose declarations start with keyword pred and are optionally followed by the list of the predicate arguments. Operations, that perform state changes in a system can be defined as predicates with some arguments corresponding to the initial state, i.e., the state prior to the execution of the operation, and other arguments corresponding to the final state, i.e., the state resulting from the execution of the operation. For a discussion on how to model state changes in Alloy, we refer the reader to Chapter 6 of[START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF].

In Alloy, a declaration of the form exported: Name -> lone Referent denotes an injective binary relation between the set Name and the set Referent. The keyword lone is an example of a relation multiplicity. In our case, it signifies that a given name is to be associated with one, and only one, referent. Of course, two distinct names can have the same referent.

[START_REF] Claudel | Self-protection for Distributed Component-Based Applications[END_REF] Defined in the Alloy module util/relation, the function dom returns the domain of a binary relation and ran returns the range of a binary relation.INRIA

Note the use of the Alloy construct let A = ... { S }, which just declares a variable A to stand as a denotation for some value, denotation which is then used inside the statement S. Note also the use of a nested implication of the form C1 implies F1 else F2, which is equivalent to (C1 and F1) or ((not C1) and F2). Note, finally, the keyword one which precedes the declaration of the NamingException value: it just signifies that the set NamingException is a singleton. In Alloy, set elements are essentially identified with singletons.RR n°6721

Note the use of the Alloy utility module graph and the predicate dag from this module.RR n°6721

In Alloy, ˜r of some binary relation r denotes the transpose of r, forming a new relation by reversing the order of atoms in each tuple.INRIA

Merle & Stefani

A future version of the Fractal model should improve on this, by defining in particular how these descriptions themselves can be manipulated, e.g., for the purpose of specifying deployment processes, and what constraints apply to them.RR n°6721

Before specifying the different operations that are attached to Component and Interface, we first define an equivalence predicate on compkells. Roughly, isoCKell indicates that two compkells have the same identifier, the same subcomponents, and the same gatesi.e., their internal and external structures (but not necessarily their exact states) are the same. By virtue of the above CKellsHaveComponent invariant, two equivalent compkells have the same Component gate. We give below the different operations attached to a Component gate. Operation getInterfaces returns the set of gates is of a compkell c, given its Component interface o.

In the process, compkell c becomes compkell c1, which is required to be equivalent to ci.e., have the same gates, the same identifier, and the same subkells. Operation The informal Fractal specification also defines the operation isInternal into the Interface interface. However for a better separation of concerns between the specification of controllers, this operation is defined later in Section 6.3. This is due to the fact that internal interfaces are managed by ContentController.

Configuration

Attribute control

The AttributeController interface in Fractal allows to configure properties of a component. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.2.

We specify below kells with AttributeController gatesi.e., elements of ACKell or ackells. Before specifying the operations attached to BindingController gates, we define an equivalence predicate between kells with a BindingController gate. Two such kells are equivalent if they have the same identifier, the same gates, the same subkells, the same client gates and the same BindingController gate.

We specify below the different operations associated with BindingController gates. Operation list returns the set of client gate identifiers of the kell hosting the target BindingController gate; in the process, the hosting kell c evolves into kell c1. Operation lookup returns the server gate i that is bound to the client gate whose identifier iid is passed as argument. Operation bind binds the client interface whose identifier cid is passed as argument to the server gate si passed as argument. Finally, operation unbind unbinds the client gate whose identifier cid is passed as argument. We give below a number of properties that assess the mutual consistency of the different BindingController operations. Predicates getClient, getBoundClient, and getBoundServer are just abbreviations for some simple conditions. The last two properties UnbindAfterBind Possible and BindAfterUnbindPossible are commutation conditions on the bind and unbind operations.

Content control

The ContentController interface in Fractal allows to introspect the internal structure of a component in the form of its so-called internal interfaces and of its subcomponents. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.4.

We specify below kells with ContentController gatesi.e., elements of CCKell. Internal gates appear only as a set of gates, which are not gates for interaction with the environment (i.e., the exterior) of a kell. There are no further semantics associated with this notion of internal gate, since it typically varies with each kell (internal gates typically allow to explicitly connect subkells to some inner functionality of their parent kell). Making explicit internal gates allows to control, through the ContentController gate, the internal connections between a parent kell and its subkells. Instances of CCKell also provide access to (in general, a subset of) their subkells (feature subcomps in the CCKell signature). Notice that CCKell is defined as a subset of CKelli.e., each instance of CCKell has both a ContentController gate and a Component gate. All subkells of a kell in CCKell, or cckell, are ckellsi.e., they all have a Component gate. The following GetSubCompFailsAfterRemove property does not hold. Because of the weak conditions on removeSubComponent, it may well be that a component with the same Component gate icc exists as a subcomponent of a component from which a component with Component gate icc has just been removed. The following assertions are not valid eitheri.e., adding or removing a component do not imply that all previous subkells, subcomponents, gates, and internal interfaces are preserved.

Super control

The SuperController interface in Fractal allows to introspect the super components of a component, i.e., the components that contain a component. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.4.

We specify below kells with SuperController gatesi.e., elements of SCKell. Instances of SCKell provide access to (in general, a subset of) their super components (feature supercomps in the SCKell signature) 15 . All super components of a kell in SCKell, or sckell, are ckellsi.e., they all have a Component gate. We now define an equivalence predicate on sckells. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, the same SuperController gate, and the same super components.

Name control

The NameController interface in Fractal allows to associate a name to a component. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.4.

We specify below kells with NameController gatesi.e., elements of NCKell. Instances of NCKell, or nckells, provide access to a name (feature name in the NCKell signature).

Lifecycle control

The LifecycleController interface in the Fractal model provides basic capabilities to control the execution of a component. The execution of a component from the point of view of this LifecycleController is abstracted as evolving between two macro-states, Started and Stopped. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 4.5.

We specify first these two macro-states. We give some consistency properties on these three operations.

Unfortunately, in this instance, the exact semantics of the Started and Stopped states, and hence of the start and stop operations, can only be given by reference to the behavior of the hosting kell. We specify below this semantics, exploiting the notion of transition. Essentially, the Stopped state is defined as one where no transition involving signals targetting non control gates is possible. We define an equivalence predicate between kells with GenericFactory gates. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, and the same GenericFactory gate.

Bootstrap

The informal Fractal specification specifies a bootstrap condition for any Fractal system: that there exists some generic factory accessible through some well-known name. We capture the first part of this bootstrap condition very simply: it merely mandates the existence of a generic factory. Operation getBootstrapComponent returns the GenericFactory interface associated with a generic factory component.

Typing

Fractal defines a simple type system for components and component interfaces, i.e., ComponentType and InterfaceType respectively, and its associated type factory. We follow here the informal Fractal specification [START_REF] Bruneton | The Fractal Component Model[END_REF], Section 6.

Role, contingency and cardinality

We specify first the notion of role, contingency, and cardinality as abstract set signatures (i.e., Role, Contingency, and Cardinality respectively) and define their possible values as singleton subsetsi.e., server and client roles, mandatory and optional contingencies, singleton and collection cardinalities.

Component and interface types

We then define both ComponentType and InterfaceType sets. A component type is a set it of interface types. An interface type is made of a name, a signature, a role, a contingency, and a cardinality. Each interface type of a component type has a distinct name. We specify below operations attached to the InterfaceType interface. Operation getItfName returns the name of an interface type. Operation getItfSignature returns the signature of an interface type. Operation isClientItf returns true if the role of an interface type is equals to client and false if it is server. Operation isOptionalItf returns true if the contingency of an interface type is equals to optional and false if it is mandatory. Operation isCollectionItf returns true if the cardinality of an interface type is equals to collection and false if it is singleton. We now define an equivalence predicate between tfkells. Two such kells are equivalent if they have the same identifier, the same subkells, the same gates, and the same TypeFactory gate. We specify below operations attached to the TypeFactory gates. Operation createItfType returns an interface type it with the name n, the signature s, the role r, the contingency co, and the cardinality ca. Operation createType returns a component type ct composed of the set its of interface types.