Rabéa Ameur-Boulifa

Ludovic Henrio

Eric Madelaine

Alexandra Savu

Behavioural Semantics for Asynchronous Components

Keywords: Behavioural specication, software components, asynchronous communications, futures Spécications comportementales, composants logiciels, communications asynchrones, futures

Software components are a valuable programming abstraction that enables a compositional design of complex applications. In distributed systems, components can also be used to provide an abstraction of locations: each component is a unit of deployment that can be placed on a dierent machine. In this article, we consider this kind of distributed components that are additionally loosely coupled and communicate by asynchronous invocations. Components also provide a convenient abstraction for verifying the correct behaviour of systems: they provide structuring entities easing the correctness verication. This article aims at providing a formal background for the generation of behavioural semantics for asynchronous components. We use the pNet intermediate language to express the semantics of hierarchical distributed components communicating asynchronously by a request-reply mechanism. We also formalise two crucial aspects of distributed components: reconguration and one-to-many communications. This article both demonstrates the expressiveness of the pNet model and formally species the complete process of the generation of a behavioural model for a distributed component system. The behavioural models we build are precise enough to allow verication by nite instantiation and model-checking, but also to use verication techniques for innite systems.

Introduction

Ensuring the safety of distributed applications is a challenging task. Not only the network and the underlying infrastructure are not reliable, but already without failures, applications are more complicated to design because of the multiple execution paths possible. To ensure the safety of distributed applications, we propose to use formal methods to be able to verify the correct behaviour of distributed applications. In order to verify properties of programs, it is necessary to choose a programming abstraction that is convenient enough to program, but also that provides enough information to be able to check the properties of the program. We adopt a programming model that is expressive enough to program complex distributed applications but with some constraints enabling the behavioural verication of these application. Component models provide a structured programming paradigm, and ensure a very good re-usability of programs. Indeed in component applications, dependencies are dened together with provided functionalities by means of provided/required ports; this improves the program specication and thus its re-usability. Several eective distributed component models have been specied, developed, and implemented in the last years [START_REF]The Common Component Architecture (CCA) Forum home page[END_REF][START_REF]CORBA Component Model Specication, omg headquarters edition[END_REF][START_REF] Beisiegel | SCA service component architecture, assembly model specication[END_REF][START_REF] Baude | GCM: a grid extension to Fractal for autonomous distributed components[END_REF] ensuring dierent kinds of properties to their users. Component models have been chosen as the target programming model for many developments in formal methods, mostly because additionally to the valuable software engineering methodology they ensure, components also provide structural informations that facilitate the use of formal methods: the architecture of the application is dened statically.

However, dening statically the exact structure of the application is sometimes too restrictive. Indeed, especially in a distributed setting, applications must evolve at runtime in order to adapt to changes in the execution environment or to provide improved functionalities. Some component models keep a trace at runtime of the component structure and their dependencies. Knowing how components are composed and being able to modify this composition at runtime provides great adaptation capabilities: the application can be adapted by changing some of the components taking part in the composition or changing the dependencies between the involved components. Recongurations consist in changing at runtime the component structure, by adding or removing components in the system, or by changing the way components are bound together. In distributed systems, reconguration can also be used at runtime to discover services and use the most ecient service available. Also, as some distributed components will naturally migrate from one location to another, they will change their execution environment and may have to adapt to the new execution platform they are moved to. Concerning formal verication, keeping trace of the component structure when building the model of the application not only allows us to build the model in a compositional manner, but also allows us to encode reconguration procedures and to verify the properties of the system when some recongurations occur.

In this work, we focus on one distributed component model, the GCM (Grid Component Model [START_REF] Baude | GCM: a grid extension to Fractal for autonomous distributed components[END_REF]). This component model originates from the Grid computing community, it is particularly targeted at composing large-scale distributed applications. Its reference implementation GCM/ProActive relies on the notion of active objects, and ensures that, during execution, each thread is isolated in a single component. Because of active objects, components that usually structure the application composition also provide the structure of the application at runtime, in terms of location and thread (a single applicative thread manipulates the state of the component).

We call this kind of components asynchronous components because they are loosely coupled entities communicating by an asynchronous request-reply mechanism. All those aspects facilitate the use of formal methods for ensuring safe behaviour of applications, but they also require specic developments to produce a formal model of an application built from such components.

This article formalises the construction of a behavioural model for ProActive/GCM components. It describes formally how we can generate a behavioural model in terms of parameterised Networks of synchronised automata (pNets) [START_REF] Barros | Behavioural models for distributed fractal components[END_REF] from the description of the architecture of a GCM/ProActive application and the description of the behaviour of each service method implemented by the programmer. In other words we formalise the automatic construction of the behavioural model for communication, management, and composition aspects.

Our behavioural models are parameterised: they can be viewed as a structured composition of labelled transition systems (LTS) that can use parameters/variables. Each pNet is either formed of other pNets or is a single LTS. Parameters can be used as local variables inside a LTS; but they can also be used to dene families of pNets of variable size, and to specify the way events occurring in dierent pNets are synchronised. Once the parameterised behavioural model generated, we can for example generate a nite instance of the model that can be checked against correctness formulas using a model-checking tool. But our behavioural model is richer than what can be checked by nite-state model-checkers and other verication techniques could also be used.

For specifying the interaction between the service methods, we generate behavioural models encoding the following features: Futures: futures are frequently used in active object languages, they are place-holders for results of asynchronous invocations, called requests here. We encode in our models the mechanisms for dealing with futures (Section 4.1.5) and the transmission of futures references between components (Section 5.1).

Component composition: from an ADL (architecture description language), we generate the synchronisations corresponding to the communications that can occur between the dierent components. We distinguish two cases: primitive components which are the leaves of the composition tree and composite components that are built from other components.

Primitive components: at the leaves of the hierarchy, from the denition of the service methods, we specify a component able to receive requests and serve each of them one after the other. When a request service terminates, a reply is sent back to the component that emitted the request. The crucial parts composing the model of a primitive component are: the request queue, the handling of communications for sending requests and replies, the futures and their management (Section 4.1).

Composite components (composites, for short): as our component model is hierarchical, a component can be built from the composition of other components; as composites are instantiated at runtime, it is necessary to specify their behaviour in our model too (see Section 4.2). Each composite is in fact implemented as an active object and thus the internal structure of a composite is very similar to the one of a primitive component.

Reconguration: as stated earlier, reconguration plays a major role in distributed systems. This article also provides a behavioural model for recongurable components (Section 5.2). To enable the verication of component reconguration, we rely on an extended ADL dening all the congurations that will be taken into account in our model.

One-to-many communications: distributed systems often rely on some form of multicast communications between one emitter and a set of registered receivers. For encoding such cases, the GCM component model denes multicast interfaces. We also formalise the generation of models for these patterns of communication in Section 5.3. This article is built upon previous works of the authors. The denition of pNets has already been formalised in [START_REF] Barros | Behavioural models for distributed fractal components[END_REF]; in this article we provide a more concise and simpler denition so that this article is self-contained. Concerning the modelling of component features, modelling of primitive Inria and composite components, and of binding controllers has been described in [START_REF] Barros | Behavioural models for distributed fractal components[END_REF]; [START_REF] Cansado | Transparent rst-class futures and distributed component[END_REF] provides a study of behavioural models for rst-class futures; multicast communications were modelled in [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF][START_REF] Boulifa | Behavioural models for group communications[END_REF]. Compared to those previous works, this article rst proposes a model aggregating all those features of the GCM component model. More important, this article fully formalises the modelling process, which is a necessary step for the automatic generation of behavioural models for component systems. Also this article is the rst one to propose a model for handling of futures in composite components. Overall this article builds upon the individual use-cases studied in our previous works to fully formalise the generation of behavioural models for asynchronous components.

Our behavioural specication is particularly adapted to the reasoning on GCM components but our approach is also applicable to other component and programming models. The component structure of GCM is quite similar to the one of Fractal [START_REF] Bruneton | The fractal component model and its support in java. Software Practice and Experience, special issue on Experiences with Auto-adaptive and Recongurable Systems[END_REF] and SCA [START_REF] Beisiegel | SCA service component architecture, assembly model specication[END_REF]; the runtime behaviour of components uses active objects/actor-like computations, which is similar to Creol [START_REF] Johnsen | Creol: a types-safe object-oriented model for distributed concurrent systems[END_REF], AmbiantTalk [START_REF] Dedecker | Ambient-oriented programming in ambienttalk[END_REF], and JCobox [START_REF] Schafer | JCoBox: Generalizing active objects to concurrent components[END_REF]. The generation of behavioural models for those frameworks can be adapted from the results of this article. Consequently, this article also shows that the pNets formalism is adapted to the behavioural specication of systems using those framework.

This article is organised as follows. Section 2 gives a brief overview of the GCM component model dened in [START_REF] Baude | GCM: a grid extension to Fractal for autonomous distributed components[END_REF] and its implementation inside the ProActive library; it also gives the abstract syntax we use for the denition of component systems and denes the set of components we consider as well-formed in Section 2.3. Section 3 provides a denition of the pNets formalism [START_REF] Barros | Behavioural models for distributed fractal components[END_REF]. Then Sections 4 and 5 contain the main contribution of the paper; they present respectively the basic behavioural model for GCM components and more complex features, namely rst-class futures, recongurations, and one-to-many interfaces. This paper concludes with an example of building the model of a use-case in Section 6, a comparison with related works in Section 7 and a conclusion. Appendices describe the semantics of pNets, a summary of main behavioural semantic functions, and some details on the model of the example use-case. [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF] The Grid Component Model: GCM GCM has been proposed in the CoreGrid Network of Excellence, it is an extension of the Fractal component model [START_REF] Bruneton | An open component model and its support in java[END_REF][START_REF] Bruneton | The Fractal Component Model[END_REF] to better address large-scale distributed computing. GCM builds above Fractal and thus inherits its hierarchical structure, the enforcement of separation between functional and non-functional concerns, its extensibility, and the separation between interfaces and implementation.

Figure 1 shows the basic component structure provided by GCM. It introduces most of the terminology used to describe GCM components and their composition. Interfaces are annotated with the type of their methods. Among the notions presented in the gure only multicast interfaces interfaces are specic to GCM.

Fractal does not impose any granularity for the components, but the existence of composite bindings and some of the features of the model suggest a rather ne grained implementation: a primitive component should contain a small number of objects. Overall, the GCM has been conceived with a granularity that is somehow in the middle between small grain Fractal components and coarse grain component models, like CCM where a component is of a size comparable to an application or a service. Somehow, GCM has been conceived thinking of components of the size of an MPI process, though it can be used to dene much ner or coarser grain components. In ProActive/GCM the primitive components (and the composite ones too) have this intermediate size: they contain an activity, i.e. an active object, its dependencies, a request queue, and a thread. Somehow, this paper relies on the fact that components are used as structuring enti- ties that specify the dierent threads of the applications and the set of objects manipulated by each of those threads. It is very interesting and convenient to use formal methods to check the properties of GCM applications, as the component structure gives crucial informations on the concurrency that occurs at runtime. GCM and Fractal come with an ADL (architecture description language) providing a textual (XML-based) way of describing component assembly. Such a description of the application architecture (either textual or graphical) is the starting point of our work. Starting from the architecture description and the description of the behaviour of each component, we build a formal description of the behaviour of the whole application.

2.1

A reference implementation for GCM ProActive/GCM is a reference implementation of the GCM component model. It is based on the ProActive Java library and relies on the notion of active objects. It is important to note that each component corresponds at runtime to an active object and consequently each component can easily be deployed on a separate JVM and can be migrated. Of course, this implementation relies on design and implementation choices relatively to the purely structural denition provided by the model. One of the main advantages of using active objects to implement components is their adaptation to distribution. Indeed, by nature active objects provide a natural way to provide loosely coupled components. By loose coupled components, we mean components responsible for their own state and evaluation, and only communicating via asynchronous communications. Asynchronous communications increase and automate parallelism; and absence of sharing eases the design of concurrent systems. Additionally, loose coupling reduces the impact of latency, and limits the interleaving between components. Finally, independent components also ease the autonomic management of component systems, enabling systems to be more dynamic, more scalable and easily adaptable to dierent execution contexts. That is why we think that a distributed component system should rely on such loosely coupled asynchronous components. That is thus the reason why we think active objects are particularly adapted to implement a distributed component model. Inria

Informal semantics of asynchronous components

This section describes briey an informal semantics of GCM/ProActive components. The general principle is that interaction between components is limited to communications, and more precisely to a request/reply mechanism. A more formal and general semantics can be found in [START_REF] Henrio | An asynchronous distributed component model and its semantics[END_REF].

Communications The basic communication paradigm we consider is asynchronous message sending: upon a communication the message is enqueued at the receiver side in a queue. To prevent shared memory between components, messages can only transmit parameters which are copied at the receiver side; no object or component can be passed by reference. This communication semantics is similar to messages in an actor model. We call requests messages sent between components. References to components cannot be passed as request parameters.

We call our component model asynchronous because communication does not trigger computation on the receiver side immediately, it just enqueues a request. To allow for transparent asynchronous requests with results, we use transparent rst-class futures. The promise for a reply to a request is created automatically when the request is sent, we call it a future. For accessing the value of a future, the caller must wait until the request is treated and the result sent. When the request is nished, the result is automatically sent to replace all the references to the corresponding future. Futures are said to be rst-class if they can be transmitted between components.

Component behaviour The primitive components encapsulate the business code. They generally serve requests in the order they arrived, providing answer for all the requests they receive. They can call other components by emitting a request on one of the client interfaces.

In ProActive/GCM, each component is mono-threaded: a single request is served at a time and no internal concurrency occurs inside a component. However, a component always accepts the reception of a future value or of a request.

While primitive components contain the application logic, composite components have a predened behaviour because they are only used as composition tools and the programmer expects them to only transmit the requests according to the specied composition. Composites serve requests in a FIFO order, delegating requests to the bound components or to the external ones. Globally, a request emitted by the client interface of a primitive component will be sent unchanged to the server interface of the primitive component that is bound to it, following one or several bindings (several bindings are used when the bounding of a composite is crossed). A composite performs no computation: it only delegates requests.

Collective interfaces GCM components mostly use three kinds of interfaces: singleton, multicast, and gathercast. Singleton interfaces are used to perform one-to-one communications as described above; a singleton client interface must be bound to a single server interface. Multicast interfaces allow one component to be bound to several others, with a congurable communication semantics; in general, a call from a multicast client interface is broadcasted to all the server interfaces bound from it. Gathercast interfaces are somehow symmetrical to multicast ones; they allow many components to be bound to a server interface and come with a synchronisation pattern: when all the client interfaces bound to a gathercast interface have emitted a request, those requests are collected and transmitted as a single one to the component having the gathercast interface.

Components featuring the semantics dened above are loosely coupled; they are better adapted to a distributed setting and easier to program safely by the limited concurrency they RR n°8167 allow. However, the semantic of such components rely on several notions, like for example request queues and futures, that have to be specied when building a behavioural model for those components. This article species how those notions can be formally dened as pNets, and how those denitions can be used to build the behavioural model of a component-based application.

Component Denition

This section denes a hierarchical structure for representing components, we dene a syntax for describing the dierent elements of a GCM component assembly. We also dene a set of auxiliary functions that will help us manipulate the component structure, and nally we dene what component systems we consider to be well-formed, these are the systems for which we are able to build a behavioural model.

The denitions below rely on several predened structures. Type represents a type, we have several kind of names (even if there is no need to distinguish them strictly): Name is an interface name, CName and C are component names, MName is a method name.

Syntax and Notations

In the following denitions, we extensively use indexed structures (maps) over some countable indexed sets. The indexes will usually be integers, bounded or not. Such an indexed family is denoted as follows: a i∈I i is a family of elements a i indexed over the set I. Such a family is equivalent to the mapping (i →a i ) i∈I . To specify the set over which the structure is indexed, indexed structures are always denoted with an exponent of the form i ∈ I (arithmetic only appears in the indexes if necessary). Consequently, a i∈I i denes rst I the set over which the family is indexed, and then a i the elements of the family.

For example a i∈{3} is the mapping with a single entry a at index 3; exceptionally, such mappings with only a few entries will also be denoted (3 →a) in the following. When this is not ambiguous, we shall use abusive vocabulary and notations for sets, and typically write indexed set over I when formally we should speak of multisets, and still better write x ∈ A i∈I i to mean ∃i ∈ I. x = A i . An empty family is denoted [] (it can be dened as a i∈∅ i ).

Let ⊎ (disjoint union) be a union operator on indexed sets requiring that the two sets are indexed over disjoint sets, we do not worry here on set re-indexing that could be performed to avoid collisions. The elements of the union are thus accessed by using an index of one of the two joined families.

Interfaces

Let SItf be the description of a service interface, it is characterised by the interface name, the interface cardinality and the signature of one or more service methods. In the same way, CItf is the description of a client interface, containing one or more client methods. We use Itf to range over interfaces that can be either client or server ones.

SItf ::= (Name, Card, MSignature i∈I i ) S

CItf ::= (Name, Card, MSignature i∈I i ) C

(2)

Itf ::= SItf | CItf (3)
Concerning cardinalities, client interfaces can be either singleton (which means the client interface of the current component is bound to one server interface of another component), or Inria multicast (meaning that the client interface is bound to more than one components through service interfaces on these components). In GCM, interfaces can also be of cardinality gathercast but this case is not treated in this article.

Card ::= singleton | multicast A method signature, MSignature, consists of a method name, an argument type 1 , and a return type:

MSignature ::= MName : Type → Type A method denition consists of a MSignature and the behaviour of this method, which is a pNet (pNets will be dened in Section 3). M i range over method denitions. Signature(M i ) returns the signature.

Components

From those denitions we dene components, which can be either primitive or composite ones.

Comp 1 it is not restrictive to consider methods with a single arguments as we have no restriction on type complexity

::= CName < SItf i∈I i , CItf j∈J j , M k∈K k > | CName < SItf i∈I i ,

RR n°8167

Figure 1 shows a composite component containing two inner composite components. For example (A.C1, This.M) is one of the bindings of this component. The interface M is a multicast interface, it can emit two kinds of requests: m1 and m2, with the types dened in the gure.

We dene a function Interfaces that given a component returns the indexed set of its interfaces, and a function Name that returns the name of its argument that can be a component, a method, or an interface.

Membrane and internal interfaces

In Fractal and GCM, the frontier of a composite component is called a membrane and can intercept incoming calls; it deals with the component management; additionally GCM provides the capacity to specify the content of a membrane as a component composition. Roughly, for each server interface of a composite component accessible from the outside, there is an internal client interface. Here we chose to have no membrane and not specify explicit internal interfaces, more precisely the membrane has no content and the internal interfaces match exactly the external ones. For each interface declared in the composite component denition, a symmetric internal interface is created with the same name and a symmetric role (server or client) as illustrated in Figure 3. By convention, a server interface of cardinality multicast stands for a single server interface, associated with an internal multicast interface. We rst dene an auxiliary function that takes the symmetric of an interface. It takes an interface and returns the same interface with a symmetric role:

Symm : Itf → Itf Symm(Name, Card, MSignature i∈I i ) S = (Name, Card, MSignature i∈I i ) C Symm(Name, Card, MSignature i∈I i ) C = (Name, Card, MSignature i∈I i ) S
We then rely on an auxiliary function Get that returns the interface inside a composite component that corresponds to a qualied name.

Get : QName × Comp → Itf Inria k ∈ K Name(Comp k ) = CN Itf ∈ Interfaces(Comp k ) Name(Itf) = IN Get(CN.IN, CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l >) = Itf i ∈ I SItf i = (IN, Card, MSignature l∈L l )S Get(This.IN, CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l >) = Symm(SItf i ) j ∈ J CItf j = (IN, Card, MSignature l∈L l )C Get(This.IN, CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l >) = Symm(CItf j ) 2.3.5
Well-formed components

In our semantics, we only want to deal with components that are correctly formed, for this we dene a predicate WF that indicates whether a component is well-formed. We suppose there is a sub-typing relation , and that this relation is classically extended to method signatures, and to families of method signatures. In practice, WF is slightly more restrictive than what could be expected of a correct component denition, or what can be found in [START_REF] Henrio | A framework for reasoning on component composition[END_REF]; this is because we prevent bindings from having the same component as source and destination, and we prevent two bindings originating from the same multicast interface from having the same destination component. Building the behavioural models in those two cases is slightly more complicated; we will come back on this restriction and how to overcome it in Section 5.4. We rst dene the predicate UniqueItfNames that takes a set of server interfaces and a set of client interfaces and returns true if no two of these interfaces have the same name.

UniqueItfNames(SItf i∈I i , CItf j∈J j ) ⇔ 8 < : ∀i, i ′ ∈ I. i = i ′ ⇒ Name(SItf i ) = Name(SItf i ′ ) ∧ ∀j, j ′ ∈ J. j = j ′ ⇒ Name(CItf j ) = Name(CItf j ′ ) ∧ ∀i ∈ I, j ∈ J. Name(SItf i ) = Name(CItf j )
Then a primitive component is well-formed if all its interfaces have distinct names and all the interfaces declared in the server interfaces have a corresponding method denition (modulo sub-typing).

WF(CName

< SItf i∈I i , CItf j∈J j , M k∈K k >) ⇔ 8 < : UniqueItfNames(SItf i∈I i , CItf j∈J j ) ∧ ∀i ∈ I. if SItf i = (Name, Card, MSignature l∈L l )S then ∀l ∈ L. ∃k ∈ K. Signature(M k ) MSignature l
Finally a composite component is well-formed if all its sub-components are well-formed, all the bindings dened bind an existing client to an existing server interface of a compatible type2 , all sub-components have distinct names, and no two bindings start from the same client interface except if this interface is multicast. We additionally require that no binding has the same component as source and destination: there is no binding looping back directly to the same component. Finally, no two bindings can have the same multicast 3 interface as source and the same component as destination. The two last conditions of the denition are the ones specic to our model, they are not generally required by the GCM model. Our models rely on the notion of parametrized actions. We leave unspecied the constructors of the algebra that will allow building actions and expressions used in our models, let us denote Σ the signature of those constructors. Let T P be the term algebra of Σ over the set of variables P . We suppose that we are able to distinguish inside T P a set of action terms (over variables of P ) denoted A P (parametrized actions), a set of expression terms (disjoint from actions) denoted E P , and, among expressions, a set of boolean expressions (guards) denoted B P . For each term t ∈ T P we dene fv(t) the set of free variables of t. For α ∈ A P we also suppose that there is a function iv(α) that returns a subset of fv(α) which are the input variables of α, i.e. the variables newly dened by reception of their value during the action α.

WF(CName

< SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l >) ⇔ 8 > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > : UniqueItfNames(SItf i∈I i , CItf j∈J j ) ∧ ∀k, k ′ ∈ K. k = k ′ ⇒ Name(Comp k ) = Name(Comp k ′ ) ∧ ∀k ∈ K. WF(Comp k ) ∧ ∀(Src, Dst) ∈ Binding l∈L l . ∃Name, Name ′ , Card, Card ′ , M, M ′ , MSignature l∈M l , MSignature ′l∈M ′ l . `Get(Src) = (Name, Card, MSignature l∈M l )C ∧ Get(Dst) = (Name ′ , Card ′ , MSignature ′l∈M ′ l )S ∧ MSignature ′l∈M ′ l MSignature l∈M l ∧ Card = Multicast ⇒ ∄Dst ′ . Dst ′ = Dst ∧ (Src, Dst ′ ) ∈ Binding l∈L l ´∧ ∀(C.CI, C ′ .SI) ∈ Binding l∈L l .C = C ′ ∧ ∀C, CI, C ′ , C ′′ , SI, SI ′ .(C.CI, C ′ .SI) ∈ Binding l∈L l ∧ (C.CI, C ′′ .SI ′ ) ∈ Binding l∈L l ⇒ C ′ = C ′′
We also allow countable indexed sets to depend upon variables, and denote I P the set of indexed sets using variables of P . There must exist an inclusion relationship ⊆ over the indexed sets of I P , with the natural guarantee that this operation ensures set inclusion when one replaces variables by their values. In practice we will mostly use intervals for which the upper bound depends on the variables of P :

I P = [1..n]
where n is an integer.

For example the actions of Milner's Value-passing CCS [START_REF] Milner | Communication and Concurrency[END_REF] correspond to the following algebra: terms are τ , a(x) for input actions, a(v) for output actions. Then fv(a(x)) = iv(a(x)) = {x}, whereas iv(a(v)) = ∅.

The pNets Model

The rst comprehensive denition of pNets was published in [START_REF] Barros | Behavioural models for distributed fractal components[END_REF]. The denition we give below is simpler because it does not include transducers and each hole contains a single pNet. The semantics given here is thus shorter but exhaustive; it provides a rigorous formal basis for expressing the semantics of the GCM features. In this section, we dene the structure of pLTSs, pNets and Queues, and dene their operational semantics.

A pLTS is a labelled transition system with variables; a pLTS can have guards and assignment of variables on transitions. Variables can be manipulated, dened, or accessed inside states, actions, guards, and assignments. A pLTS is formally dened as follows.

Denition 1 (pLTS) A parametrized LTS is a tuple pLT S P, S, s 0 , L, → where: Inria • P is a nite set of parameters, from which we construct the term algebra T P , with the parametrized actions A P , the parametrized expressions E P , and the boolean expressions B P .

• S is a set of states. For each state s ∈ S, variables of s are global to the pLTS.

• s 0 ∈ S is the initial state.

• L is the set of labels of the form α, e b , (x j := e j ) j∈J , where α ∈ A P is a parametrized action, e b ∈ B P is a guard, and the variables x j ∈ P are assigned the expressions e j ∈ E P . Variables in iv(α) are assigned by the action, other variables can be assigned by the additional assignments.

• →⊆ S × L × S is the transition relation.

Note that we make no assumption on niteness of S or of branching in →. pNets are constructors for hierarchical behavioural structures: a pNet is formed of other pNets, or pLTSs at the bottom of the hierarchy tree. Message queues can also appear in leaves of a pNet system. A composite pNet consists of a set of pNets exposing a set of actions, each of them triggering internal actions in each of the sub-pNets. The synchronisation between global actions and internal actions is given by a synchronisation vector: a synchronisation vector synchronises one or several internal actions, and exposes a single resulting global action.

Denition 2 (pNets) A pNet is a hierarchical structure where leaves are pLTSs (or queues dened below): pNet pLT S | Queue(M) | P, L, pNet i∈I i , SV k∈K k where

• P is a nite set of parameters, from which we construct the term algebra T P , with parametrized actions A P .

• L ⊆ A P is the set of labels of global actions of the pNet.

• I ∈ I P is the set over which sub-pNets are indexed, I = ∅.

• pNet i∈I i is the family of sub-pNets.

• SV k∈K k is a set of synchronisation vectors (K ∈ I P ). ∀k ∈ K, SV k = α j∈J k j → α ′ k . Each synchronisation vector veries: α ′ k ∈ L, J k ∈ I P , ∅ ⊂ J k ⊆ I, and ∀j ∈ J k . α j ∈ Sort(pNet j ).
For each pNet, we dene a function sort (Sort : pNet → A P ). The sort of a pNet is its signature: the set of actions that a pNet can perform, that is to say the set of labels of its transitions, more formally:

Sort( P, S, s 0 , L, → ) = L Sort( P, L, pNet i∈I i , SV k∈K k ) = L
A pNet composes sub-pNets and expresses by its synchronisation vectors how the dierent sub-entities are synchronised. SV k = α j∈J j → α ′ k means that each of the sub-pNets can performs synchronously the action α j ; this results in a global action labels α ′ k . When I = [1.

.n] we denote the pNet as P, L, pNet 1 , . . . , pNet n , SV , and each synchronisation vector as: α 1 , . . . , α n → α. In that case, elements not taking part in the synchronisation are denotedas in: -, -, α, -, -→ α.

RR n°8167

Queues We also dene a particular pNet called Queue(M); it models the behaviour of a FIFO queue. It can be considered as an innite pLTS with a set of actions depending on the chosen term algebra and of the set of enqueue-able elements M ⊆ T P . We suppose that the term algebra has two specic constructors ?Q and !Serve4 such that for all set of variables P , ∀m i ∈ M. !Serve_m i ∈ A P ∧ ?Q_m i ∈ A P . Then the queue pNet oers the following actions:

L = {?Q_m i |m i ∈ M} ∪ {!Serve_m i |m i ∈ M}.
The behaviour of a queue is only FIFO en-queueing/de-queueing of messages.

Sort(Queue(M)) = {?Q_m i |m i ∈ M} ∪ {!Serve_m i |m i ∈ M}
Whenever pNets will be encoded by (ultimately nite) automata structures for model-checking, pNet Queues will naturally be represented by nite automata. However, in order to be able to address more general approaches, and in particular specic model-checking algorithms for unbounded channels, we need to keep a high-level representation of Queues. From these abstract Queues, we will be able to generate both regular representation (for unbound queues), and nite representation (for explicit-state model-checking).

More notations We dene a constructor for a pNet made of an indexed family of pNets.

← -------→ P, P N i∈I i takes a family of pNets indexed over a set I ∈ I P , and a parameter set P , and produces a global pNet. The synchronisation vectors for this family will be expressed at the level above, consequently we export all the possible synchronisation vectors that the family could oer, only some of them will be used.

← ------→ P, PN i∈I i P, V, PN i∈I i , {α j∈J j → α j∈J j |α j∈J j ∈ V} where V = {α j∈J j | J ⊆ I ∧ ∀j ∈ J. α j ∈ Sort(PN j )}
This supposes that the elements of V belong to the term algebra and more precisely are action terms.

If all the elements of the family are identical, then we simply write ← -----→ P, PN I .

In fact, the denition of pNets shown here is a simplied version of pNets [START_REF] Barros | Behavioural models for distributed fractal components[END_REF] that is convenient for providing a concise formal denition of both pNets themselves and the component specication in terms of pNets. Especially concerning families of pNets, it is not reasonable, in practice, to dene all the possible synchronisation vectors inside a family. In [START_REF] Barros | Behavioural models for distributed fractal components[END_REF], we dened a version of pNets where the families are attened in the enclosing pNet and only the used synchronisations are instantiated. Though more ecient in practice this notation was more complex, that is why a simpler denition is presented in this paper. Section 6 will show an optimised instantiation of the produced pNet structure and synchronisation vectors.

An operational semantics for pNets is given in Appendix A.

Assumptions on the term algebra

Let us consider several aspects of the term algebra we might use in the description below, those aspects are not related to the pNets semantics but rather to the way we use it.

In our term algebra, we have three basic kinds of actions: input actions of the form ?a(x 1 , ..., x n ) where x i are input variables, output actions of the form !a(v 1 , .., v n ), where v i are values (expressions), and synchronised actions of the form a only used for observation purposes. Our actions can also be parameterized by one or several arguments thus they can be of the form a(arg) or a(arg, p).

In order to express synchronisation vectors of families of pNets, we must allow families of actions to be considered as actions themselves. More precisely, if a and a i are actions, then actions can be of the form i →a to allow the sub-pNet at index i to perform an action, also we use i ∈ I →a i to express the family of actions a i∈I i triggering a synchronous action on all the sub-pNets indexed in I, or i →a, j →b to synchronise two elements of the family.

Synchronised actions (prexed neither by ! nor by ?) are not meant to be used anymore for synchronisation purposes, they should just be visible at the top-level of the pNet hierarchy. Consequently, we dene an operator that takes an indexed set of pNets and returns the synchronisation vectors that should be included in the parent pNets to allow the visibility of synchronised actions:

Observe(pNet i∈I i ) = {(i →α)|i ∈ I ∧ α ∈ Sort(pNet i ) ∧ α synchronised action}
In the following, those synchronisation vectors dedicated to observation will be implicitly included as synchronisation vectors of all our pNets. This means that for all pNets written in the following of this paper, Observe(pNet i∈I i ) is considered to be included in the set of synchronisation vectors of the considered pNets (where pNet i∈I i is the set of sub-pNets of the new pNet). In this paper, we do not use explicitly internal action (τ transition). If the action algebra contains τ transitions, then we would use weak bisimulation notions to deal eciently with the pNets. More precisely, upon composition of pNets, a sub-pNet will be allowed to perform additional (invisible) τ transitions. In other words, τ would behave similarly to the synchronised actions dened above. [START_REF] André | Composing Components with Shared Services in the Kmelia Model[END_REF] Behavioural semantics for GCM components This section denes formally the behavioural semantics for the component model dened in Section 2.3. It shows how to build pNets from the specication of a hierarchy of components. We organise this section as follows. We rst give a behavioural semantics for primitive components including simple future proxies, and the behaviour and synchronisation of the dierent elements of the primitive component. We then describe the behavioural semantics for composite components, which compose the semantics of their sub-components synchronising the request and replies of the sub-components between themselves and with the external components. For that, we will need to dene a new kind of future proxies for handling the delegation mechanism that occurs in the composite components.

Term algebra The term algebra we use is a set of parameterised actions; actions will typically be of the form Serve_m for m a method label as dened below. Parameters will be either values (method parameters denoted arg or computed results denoted val), or future identiers (denoted either p, or f , or d). We suppose a set P is given, it is the set of all parameters potentially used in the dierent pNets; it will be used in all the pNets expressed in the rest of this paper.

In all this document, we use, as action parameters, two variables arg and val that (implicitly) range over the set of values, this set of values being purposely undened. In an object-oriented language, those values should be an abstraction of objects (potentially containing other objects). It could be dened depending on the type of the value but we will not consider this aspect here. In our previous works, the abstract domain for values could be reduced to a few elements in order to generate a nite instantiation of the pNet and verify its behaviour by model-checking techniques.

We rely on a predened set Labels, the set of action labels that can be used in our pNets, it should depend on the term algebra (it is possible to generate this set from the labels used in each pNet).

Labels for identifying methods

Inside our actions, we need identiers for methods that are more precise than simple method names. We dene thus MethodLabels as a set of method labels, where a method label encompasses a method name, a signature, and the interface the method belongs to, plus possibly other meta-informations. Most of the following can be read as if MethodLabels were just method names, however at some specic points and to disambiguate dierent methods, the other informations encoded in MethodLabels are also necessary. m i range over such method labels.

A function MethLabel : Itf → P(MethodLabels) is dened, where MethLabel(Itf i ) returns the set of MethodLabels corresponding to the methods of interface Itf i . MethLabel is also dened for sets of interfaces (union of method labels for each interface). Conversely, for a given method label m, Itf(m) returns the interface of the method.

Behavioural semantics

The behavioural semantics of components is expressed under the form Component . It relies on the use of several auxiliary functions for expressing the semantics of specic parts of the components: the behaviour of the service of one request (for a primitive component), the behaviour of the body of the component serving requests one after the other, a proxyManager for managing the available future proxies, the behaviour of each future proxy, and nally a delegation behaviour used when a composite component delegates the service of a request to another component. The signature of all these functions is summarised in Appendix B.

Semantics of primitive components

Primitive components are the leaves of the hierarchy; they contain the applicative code from which more complex components, and thus more complex behaviours can be built. This section gives a behavioural semantics for GCM primitive components, able to receive requests, to serve them in a FIFO order by executing a service method, and to send requests to the external world. Additionally to the global structure of a primitive component and the synchronisation of its sub-entities, this section denes pLTSs describing the behaviour of a FIFO service policy, of proxies for handling futures, and of managers for pools of future proxies. Considering the features we model, we think that our work provides a reliable basis for the behavioural specication of asynchronous components communicating by asynchronous requests and futures. This section also shows that pNets provide a convenient abstraction for modelling this behaviour.

Illustrative Example

We rst illustrate and explain the structure of the behavioural semantics of primitive components based on the component shown in Figure 2. Figure 4 illustrates the structure of the pNet expressing the semantics of the component. It illustrates both the global structure of the pNets represented by boxes, and the synchronisation vectors represented by arrows (an ellipse is used when a synchronisation vector involves more than two processes). Note that the direction of an arrow is purely conventional, but goes, as much as possible, from an emission action to a reception action, intuitively following the data ow.

A primitive component can receive incoming requests (?Q_m i ) that are stored in the Queue pNet and then served by the Body pLTS. The service consists in triggering a Call_m i to the !R_m i action is emitted with the right future identier d and result value val.

Inria M1 M3 PM m5 PM m4 Body ... Call m*(arg) !R m1(f id1, val) !R m2(f id2, val) !R m3(f id3, val) Primitive Example 1 !R m*(f id * ) !R *(val) ?Q m3(f id3, arg) ?Q m2(f id2, arg) ?Q m1(f id1, arg) ?R m5(p5, val) ?R m4(p4, val) !Q m5(p5, arg) !Q m4(p4,
The service method can call external components through client interfaces. Each method of each client interface is equipped with a proxy manager PM_m i on which the caller can perform a GetProxy. Upon request, a fresh future proxy Proxy_m i is allocated and returned by a New_m i action that acts as a response to the GetProxy; there is a family of future proxies for each method of each client interface. Then the outgoing call is emitted with the reference to the corresponding proxy sent as parameter (!Q_m i ). Finally when a result is computed the reply ?R_m i is received by the adequate proxy and the result can be accessed by GetValue_m i actions performed by some service methods. Then, service methods can emit Recycle actions that are sent to the adequate proxy and proxy manager.

pNets and Synchronisation Vectors

This section formalises and generalises the principles depicted in the previous section. Primitive components encode the business code of the application. Consequently, the behaviour of primitive components include the behaviour of service methods: those methods represent the code written by the programmer, it is the only part for which we do not specify the generation of the behavioural model. We suppose that for each service method m l , for a set of methods M k∈K k dened by the component, m l , M k∈K k service provides a pNet expressing the behaviour of this service method. Concerning the rest of the behaviour of a primitive component below, it is computed by the rules shown in this section.

RR n°8167

m l∈L l = MethLabel(SItf i∈I i ) Q = Queue(m l∈L l ∪ NF) B = m l∈L l , NF body ∀l ∈ L. SM l = m l , M k∈K k service ∀j ∈ J. let m n∈N n = MethLabel(CItf j ) in for all n ∈ N let F n = ← ----------→ P, m n N proxy in P j = ← ------→ P, F n∈N n and PM j = ←----------------→ P, m n n∈N proxyManager SV = SV S (m l∈L l ) ∪ SV C (CItf j∈J j , L) CName < SItf i∈I i , CItf j∈J j , M k∈K k > = P, Labels, Q, B, ← -------→ P, SM l∈L l , ←-------→ P, PM j∈J j , ←-----→ P, P j∈J j , SV
Note that P and Labels are xed sets dened globally above. The pNet corresponding to a primitive component is made of:

A queue able to receive incoming requests: it can enqueue a request on a method label of one of the server interfaces, we use here a pNet queue constructor. The queue is also given a set of method labels NF, it contains the set of non-functional requests that can be accepted by the component; we will use this set in Section 5.2 and 5.3. For the moment, NF = ∅.

A body that will serve all the requests that can reach the queue, it will delegate the treatment of the request to the service methods

← -------→ P, SM l∈L l
, the body constructor is also given the set NF.

Service methods: there is one service method for each method label of a server interface, it encodes the business logic of the component.

A family PM of proxy managers indexed both over the set of client interfaces and over the methods of those interfaces: those managers are responsible for allocating a new proxy when requested, and activating those newly created proxies.

A family P of future proxies indexed over the set of client interfaces (J), the methods of those interfaces (N), and proxy indexes, i.e. integers (N): a proxy is responsible for receiving the result of a request made towards another component; when the value of the result is needed by a service method, this method asks for the value to the adequate proxy.

Note the construct m l∈L l = MethLabel(SItf i∈I i ) that denes both the value of each method label m l and the set L over which it is indexed. This kind of constructs will be massively used in the rest of this paper.

The set of synchronisation vectors for a primitive component is built by two functions: SV S that provides the set of synchronisation vectors corresponding to the server interfaces, and SV C for the client interfaces. Each of those sets is dened as the smallest set verifying the constraints given in Table 1. Remember the synchronisation vector set also implicitly includes observation vectors dened in Section 3.3.

Let us explain briey what are the synchronisation vectors generated by the inference rules, more precisely, we focus on the synchronisation vectors for the GetProxy_m i actions, rule [P2.1]. One synchronisation vector for GetProxy_m i is generated for each l ∈ L, for each j ∈ J, and for Inria Table 1: Server and client-side synchronisation vectors for primitive components.

The synchronised sub-pNets occur in the following order:

Queue, Body, ServiceMethods, ProxyManagers, Proxies -, -, -, -→?Q_mi(d, arg), [1] !Serve_mi(d, arg), ?Serve_mi(d, arg), -, -, -→ Serve_mi(d, arg), [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF] -, !Call_mi(arg), i →?Call_mi(arg), -, -→ Call_mi(arg),

i ∈ L d ∈ N { ?Q_mi(d, arg),
[3] -, !R_mi(d), i →!R_mi(val), -, -→!R_mi(d, val)} [4] ⊆ SVS(m i∈L i ) P1 j ∈ J l ∈ L m i∈I i = MethLabel(CItf j ) i ∈ I p ∈ N { -, -, l →!GetProxy_mi, j →i →?GetProxy_mi, -→ GetProxy_mi, [1]
-, -, l →?New_mi(p), j →i →!New_mi(p), j →i →p →?New_mi → New_mi(p),

-, -, l →!Q_mi(p, arg), -, -→!Q_mi(p, arg),

-, -, -, -, j →i →p →?R_mi(val) →?R_mi(p, val),

-, -, l →?GetValue_mi(p, val), -, j →i →p →!GetValue_mi(val) → GetValue_mi(p, val),

[5] -, -, l →!Recycle_mi(p), j →i →?Recycle_mi(p), j →i →p →?Recycle_mi → Recycle_mi(p) } [6] ⊆ SVC(CItf j∈J j , L) P2 each i ∈ I.
Each synchronisation vector synchronises one action l →!GetProxy_m i5 of the sub-pNet containing the family of service methods, with one action j →i →?GetProxy_m i of the sub-pNet containing the family of proxy managers (for each interface). As each of the synchronisation vectors of families of pNets triggers the action on the indexed element of the family, this line allows one action !GetProxy_m i of one service method (indexed by l) to be synchronised with the action ?GetProxy_m i of the proxy manager indexed by i of the interface indexed by j. The action is globally visible as GetProxy_m i and will be (implicitly) observable in all the hierarchy of pNets containing this one. The set of service synchronisation vectors SV S dened in rule [P1] encodes the following synchronisations: en-queueing an incoming request [P1.1], service of a request by the body [P1.2], the body calling a service method to serve a request [P1.3], and the service method providing a result for this served request [P1.4]. In the last case the result both noties the body process and is returned to the outside of the primitive component. In all the actions, the method argument or the returned value is used as parameter, plus when necessary the identier of the concerned future (d).

The set of client synchronisation vectors SV C is dened in rule [P2]; it encodes the following synchronisations:

obtaining a new future proxy which involves a call to the proxy manager [P2.1] and another action [P2.2] for returning a fresh proxy identier and activating the corresponding future proxy, the sending of a request from a service method to an external components [P2.3], the reception of a result by the future proxy [P2.4], the access to a future value [P2.5] from a service method, the future value is stored in the future proxy, the eventual recycling of a future proxy [P2.6].

The function SV C receives as argument the set L of indexes over which service methods range. This argument is necessary because all service methods can perform some of the actions, like GetValue_m i .

Remember the interface called is encoded as part of the method label m i , consequently the index of the concerned interface can be inferred from the MethLabel of the invoked method. Note the indexing of proxy managers (by interfaces and methods) and of proxies (by interfaces, methods, and proxy identier).

Body

The body is a pLTS modelling the service of the dierent requests: for each service method, the body can dequeue a request corresponding to this method, delegate the service to the appropriate service method, wait for the computation of a result, and nally return this result before dequeueing a new request. It can be generated automatically from the set of service methods m i∈I i and the set of non-functional method m ′ k k∈K . For simplicity, we suppose here methods m ′ k have a single argument. m i∈I i , m ′ k∈K k body = P, S, s 0 , L, → where:

S = {s 0 } ∪ i∈I {s i (d, arg)} ∪ i∈I {s ′ i (d)} ∪ k∈K {s ′′ k (i)} L = i∈I {?Serve_m i (d, arg), !Call_m i (arg), !R_m i (d)} ∪ k∈K {?Serve_m ′ k (i), !m ′ k (i)} →= i∈I {s 0 ?Serve_mi(d,arg) --------------→ s i (d, arg)} ∪ i∈I {s i (d, arg) !Call_mi(arg) ----------→ s ′ i (d)} ∪ i∈I {s ′ i (d) !R_mi(d) --------→ s 0 } ∪ k∈K {s 0 ?Serve_m ′ k (i) ----------→ s ′′ k (i)} ∪ k∈K {s ′′ k (i) !m ′ k (i) ----→ s 0 }
For each method m, the body pLTS can always perform the three actions ?Serve_m, then !Call_m and then !R_m. It also includes the services of the non-functional requests, which after the ?Serve_m ′ action, only triggers a m ′ action. This body encodes a mono-threaded component behaviour where no two requests are served at the same time. This corresponds indeed to the behaviour of the ProActive/GCM framework, and more generally to the behaviour of activeobjects or actors. Allowing the body to serve multiple requests at the same time would be quite easy but the resulting behaviour would be much more complex.

Figure 5 provides a graphical denition for the pLTS of the body dened above (in the rest of this paper we will express pLTSs graphically). The graph shows a body able to serve three functional requests (m 0 , m 1 , and m 2 ) and two non-functional ones (bind_Itf(i) and unbind_Itf(i)). Those are the two kinds of non-functional requests that will be used for dealing with reconguration in Section 5.36 .

Service Methods

The behaviour for each service method is expressed by a pNet, used when serving the corresponding request. This behaviour is either obtained by source code analysis, or provided by the ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i) ?Serve_Unbind_Itf(i)

!Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i) !Unbind_Itf(i)
?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) ?Serve_Bind_Itf(i) Communicating by asynchronous requests allows each component to execute asynchronously from the others. However it is commonly necessary to obtain a result for some of those asynchronous invocations. A convenient abstraction for dealing with response to asynchronous requests is the notion of futures. Technically, a future is often implemented by a proxy that represents the result and is accessible both locally to know whether the result came back, and remotely by the invoked component that wants to return the result. We represent those notions in our behavioural models. Such future proxies have to be instantiated upon need; thus, to allocate fresh futures, we use proxy managers that will be invoked before performing an asynchronous request. Finally, we leave the opportunity for the service methods to inform the manager that a future proxy is no longer useful and can be recycled; this behaviour is also encoded in our future proxies and managers. Remember future proxies are families indexed by client interface index, method index, and future identier; proxy managers are indexed by client interface index and method index. We propose a specication of manager and future proxy in Figure 6.

!Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i) !Bind_Itf(i)
The behavioural semantics of the proxy manager is dened by the pLTS ProxyManager_m shown on the right side of Figure 6; it is denoted by m proxyManager . It maintains a list of available proxies and returns a fresh future (by a New action), or if there is no more fresh future, raises an error NoMoreProxy. Indeed, in our specication, we let future identiers be indexed by N but if one wants to perform nite model-checking, a bound should be chosen on the size of each future proxy family, and in each proxy manager, Max_Proxy should be set to the chosen bound (which could be dierent for each manager).

Each proxy has a much simpler behaviour; m proxy is dened by the pLTS Proxy_m shown on the left side of Figure 6. Once activated by a New_m action, it waits for the corresponding reply (?R_m(val)). At this point, the proxy can be accessed to know the result of the request invocation, it continuously sends the result to the service methods by a !GetValue_m(val) output action until the proxy is recycled.

The proxies in Figure 6 are endowed with a Recycle_m transition, bringing back the proxy in its initial state. This is useful when information can be computed, e.g., by static analysis techniques, that the proxy will not be used anymore, so it can be made available again in the proxy pool of the ProxyManager. The Recycle_m event should be sent by the LTS modelling a

!GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val)

?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?Recycle_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?New_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0 p:=0

[Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [Pool_Proxy(p).free=False] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] [p=Max_Proxy] !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) !Error(NoMoreProxy) [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy] [p<Max_Proxy]

p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++ p++

[Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p).free=true] [Pool_Proxy(p)

p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true

Figure 6: pLTSs for the Future Proxies and Proxy Managers service method. When such an event is received by the ProxyManager, this sets the corresponding entry in the Pool_Proxy to free. For generality, the proxy manager accepts Recycle_m transitions in every state, even if for mono-threaded GCM components, this action can only be received when the proxy manager is in its initial state.

4.1.6

Dealing with stateful components

The semantics we presented here does not allow to store a state for the components, however it is easy to add component variables in our specication. Indeed it is sucient to add an additional sub-pNet to the pNet of the primitive component that stores the value of the variables and accepts set and get actions. Those actions will be triggered by the service methods so synchronisation vectors for those setters and getters are also necessary, they relate service methods and the new sub-pNet dedicated to state management.

Such a state management pNet can also be used to express the behaviour of an attribute controller. In Fractal, an attribute is a congurable property of a component, it can be accessed and modied by setter and getter functions, exposed outside the component as a non-functional interface. The attribute controller interface is a non-functional interface exposed by the component. Attributes that can be stored and modied can be expressed in pNets by adding the getter and setter functions to the requests that can be enqueued, and by adding synchronisation vectors from the body to the sub-pNet dedicated to state management for getter and setter actions.

In the case of composite components (dened in the next section), a state management pNet can be necessary to congure the non-functional aspects (a composite component has no functional internal state). It can be expressed similarly.

Semantics of composite components

Hierarchical component models, like GCM, allow the specication of new components, based on the composition of others. Such a composition abstraction is very convenient when building large applications. We start from the hypothesis that composite components are dened statically by Inria some form of ADL (architecture description language) as dened in Section 2.3. The ADL is used to synchronise the emission and reception of communication actions between the subcomponents. Additionally, a composite has a request queue for receiving requests coming from the outside or the inside of the component, it treats each of those requests by sending it to the adequate component or emitting a request to the outside world. For this the composite has future proxies but as the requests only transit through the component, we implement special future proxies that perform future redirection: when a future proxy is created, it receives the identier for another future f ′ and when the reply will come back, it will be immediately re-sent as a reply for the future f ′ .

Illustrative Example

Figure 7 shows the pNets structure corresponding to the composite component of Figure 1. It illustrates the structure of the pNets we generate for specifying the behaviour of a composite component. We use it here to illustrate how we are able to generate behavioural models for GCM components. !Q m4(f b, arg)

!R m0(q, val)

?Q m0(f, arg) !R m0(f, val) ?Q {m1,m2,m4}(f, arg) ?R m4(f b, val) !New m0(f, q) Deleg m0 !Q m1(p, arg) !Q m2(p, arg) !Q m4(p, arg) !New m1(f a, p) !New m2(f a, p) !New m4(f b, p) ?R m1(f a, val) ?R m2(f a, val) !R m1(f a) !R m2(f a) !R m4(f b) ?Recycle m(p) !R m0(f ) C3 C4.2 C5.2 C6.1 C4.2 C6.2 C7.2 C7.1 C2.1 Serve *(f, arg) C1.1 C4.1 !GetProxy m0(f ) Q m3(f, arg) R m3(f, val) !Call m0(f, arg) Deleg m !Call m(f, arg) C2.2 !R m2(f ) C5.1 C2.2 ∀m in {m1,m2,m4} !R m0(f ) C4.1 !GetProxy m(f ) ∀m in {m1,m2,m4} !Q m2(f a, arg) !Q m1(f a, arg) !R m1(f ) !R m3(f ) ?Recycle m0(q)
Queue Queue ?Q m0(q, arg)

Figure 7: pNet for the Composite Component from Figure 1 Two sub-pNets A and B represent the behaviour of sub-components A and B. A queue pNet receives ?Q_m0(f,arg) requests where f is the future corresponding to the request and arg the value passed as argument. Serve* communications allow the body to retrieve those requests, which will then be treated by the Deleg_m0 pNet, this pNet receives Call communications from the body and delegates the request to an inner component (here, A); during this process, a future proxy is created by the proxy manager (process CPM_m0 ), the proxy (process CProxy_m0[q] ) is responsible for receiving the reply when A has nished the request treatment and for forwarding this result to the outside of the composite component: R_m0(q,val) that becomes R_m0(f,val).

Note that this proxy encodes some basic form of rst-class future: the future q corresponds to the same result as the future f.

Similarly, requests emitted by the inner components arrive in the queue (we draw two Queue boxes, but they correspond to the same element), they are then delegated to the outside world by a similar mechanism: a Deleg_m pNet delegates the call, and creates a future proxy, which will be responsible for sending back the result to the appropriate inner component. Here again the proxy manages the fact that both the future q and the future fa (or fb) represent the same result.

Finally, note the proxy structure we adopt: there is one proxy manager CPM* for each method of each interface (proxy managers are both indexed over interfaces and over methods).

Then each of those manager itself manages a family of proxies CProxy*. Performing modelchecking on those structures then requires a precise denition and optimisation of the number and size of those families.

All the communications expressed above, but also the communication channels between the dierent inner components requests Q_m3 and the corresponding replies R_m3 correspond to synchronisation vectors of the pNet of the composite. Each box is a pLTS or a family of pLTSs, except inner components that are more complex pNets.

Global structure

The semantics of a composite component is described below; the rst dierence compared to the semantics of primitive components is that it does not rely on service method specication, instead it delegates requests to sub-components, some of the sub-pNets of a composite component's pNet correspond to the behaviour of the sub-components. Like primitive components, the behaviour of composite components include a proxy manager and proxy families, but in the case of composites, we also need one future proxy family for each method of each server interface. Indeed the service of requests received on a server interface will be delegated to a sub-component, and thus a future is necessary to represent the result of such a delegated request. Note the use of the Symm function to take the symmetrical role of an interface and to transform those server interfaces into client ones. For similar reasons, the request queue can receive requests on all methods of all the interfaces of the composite component, both server and client (i.e., internal server) ones.

To delegate a request to an inner component or from an inner component to an external one, delegation methods are used, they are denoted DM. Delegation methods transform a request into another and a special proxy for future is used in order to remember the relationship between the original future and the future of the new delegated request.

m l∈L l = ] j∈J MethLabel(SItf j ) ⊎ ] i∈I MethLabel(CItf i ) Q = Queue(m l∈L l ∪NF) B = m l∈L l , NF body ∀l ∈ L. DM l = m l delegate Itf h∈H h = (CItf i∈I i ) ⊎ (Symm(SItf j ) j∈J ) ∀h ∈ H. let m n∈N n = MethLabel(Itf h ) in for all n ∈ N let Fn = ← ----------→ P, mn N proxy in P h = ← ------→ P, F n∈N n and PM h = ←----------------→ P, mn n∈N proxyManager SV = SVS(MethLabel(SItf i∈I i ), MethLabel(CItf i∈I i )) ∪ SVC(CItf j∈J j , Itf h∈H h ) ∪ SVB(Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding b∈B b > = P, Labels, Q, B, ←-------→ P, DM l∈L l , ← --------→ P, PM h∈H h , ← ------→ P, P h∈H h , ←-----------→ P, Comp k k∈K , SV
The body and the queue are similar to the ones of primitive components. The behaviour of future proxies for composite component is slightly dierent from the one of primitive ones, as illustrated in Figure 8: the process CProxy_m in the gure gives the new value of the proxy semantics m proxy . The delegation methods create those proxy to remember the identier of the future that the delegation method should serve. Consequently, the future proxy receives a future identier and will return it upon need. The future proxy thus rst receives a New action with a future identier as parameter and then emits an !R_m(f ). Such a proxy is somehow automatically recycled as, by construction, we know it is only used once.

Delegation Methods

The Deleg_m process, also shown in Figure 8 expresses the generation of delegate methods: m delegate is given by the pLTS Deleg_m. This delegation process receives a Call invocation from the body, creates a future proxy, launches a remote invocation (either to an inner or to an external component) and nishes its execution. This way the composite component can continue its execution and serve another request, but the process of the future proxy is still running in order to redirect the reply towards the right future identier. The proxyManager for composite component is not shown, indeed it is a direct adaptation of the primitive one (Figure 6): it behaves exactly the same except that the GetProxy action receives a future identier as parameter, this parameter is then passed as argument in the New emission action (it will be used by the future proxy). [C1] allows external components to enqueue a request in the queue, for each method of a server interface of the composite (given as rst argument of SV S ). Note that replies (!R_m) are not part of this rule because they depend on the bindings of the component; consequently they are treated among the binding synchronisation vectors. Rule [C2] uses a bigger set of methods as it takes into account requests of the server interfaces and the client interfaces of the composite; indeed, remember client interfaces have an associated internal server interface accessible by the sub-components Table 2: Server and client-side synchronisation vectors.

The synchronised sub-pNets occur in the following order: Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents ), and thus each l ∈ L is considered as equal to a method index k of a single interface i. Consequently, the request sending action (!Q_m k ) is always issued by the delegate method indexed by k. Rule [C4] allows delegation methods to instantiate new proxies (by calls to the proxy manager and to the future proxies). Compared to the case of the primitive component, note the additional argument f passed to the proxy manager. This future identier allows the future proxy (indexed p) to remember that the reply it will receive should be forwarded to the caller as the value for the future identier f (and not p). In other words, the proxy remembers that the future p it will receive is in fact an alias for the future f . Similarly to primitive components, there are two actions for dealing with future proxy creations: GetProxy in [C4.1], and New in [C4.2].

i ∈ L f ∈ N ?Q_mi(f, arg), -, -, -, -→?Q_mi(f, arg) ∈ SVS(m l∈L l , m ′ l l∈L ′ ) C1 (i ∈ L ∧ m = mi) ∨ (i ∈ L ′ ∧ m = m ′ i ) f ∈ N { !Serve_m(f, arg), ?Serve_m(f, arg), -, -, -→ Serve_m(f, arg), [1] -, !Call_m(f, arg), i →?Call_m(f, arg), -, -→ Call_m(f, arg) } [2] ⊆ SVS(m l∈L l , m ′ l l∈L ′ ) C2 j ∈ J m k∈K k = M ethLabel(CItf j ) k ∈ K f, p ∈ N -, !R_mn(f ), k →!Q_m k (p, arg), -, -, -→!Q_m k (p, arg) ∈ SVC(CItf j∈J j , Itf h∈H h ) C3 h ∈ H m k∈K k = M ethLabel(Itf h ) k ∈ K f, p ∈ N { -, -, k →!GetProxy_m k (f ), h →k →?GetProxy_m k (f ), -, -→ GetProxy_m k (f ), [1] -, -, k →?New_m k (p), h →k →!New_m k (p, f ), h →k →p →?New_m k (f ), -→ New_m k (p, f )} [2] ⊆ SVC(CItf j∈J j , Itf h∈H
Finally, the synchronisation vectors for the bindings of the composite component are shown in Table 3. There are three rules for building SV B . Rule [C5] deals with import bindings, i.e. bindings from the composite component's internal client interfaces to inner components. Symmetrically, [C6] concerns export bindings, from inner components to the composite component's internal server interfaces. The last rule [C7] species synchronisations due to bindings between two inner components.

The rst rule [C5] deals with import bindings. The rst premise of the rule picks an import binding, the next premises nd the concerned server interface of the composite component, Inria Table 3: Binding synchronisation vectors.

The synchronised sub-pNets occur in the following order: Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents

k ∈ K (This.SI, C.SI2) ∈ Binding b∈B b i ∈ I SI = Name(SItf i ) C = Name(Comp k ) m n∈N n = MethLabel(SItf i ) n ∈ N m ′ n = mn{ {SI ← SI2} } q, f ∈ N { -, !R_mn(f ), n →!Q_mn(q, arg), -, -, k →?Q_m ′ n (q, arg) → Q_mn(q, arg), [1] -, -, -, i →n →!Recycle_mn(q), i →n →q →!R_mn(f ), k →!R_mn(q, val) →!R_m ′ n (f, val)} [2] ⊆ SVB(Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C5 k ∈ K (C.CI, This.CI2) ∈ Binding b∈B b j ∈ J CI2 = Name(CItf j ) C = Name(Comp k ) m n∈N n = MethLabel(CItf j ) n ∈ N m ′ n = mn{ {CI2 ← CI} } p, f ∈ N { ?Q_mn(f, arg), -, -, -, -, k →!Q_m ′ n (f, arg) → Q_mn(f, arg), [1] -, -, -, j →n →!Recycle_mn(p), j →n →p →!R_mn(f ), k →?R_m ′ n (f, val) →?R_mn(p, val) } [2] ⊆ SVB(Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C6 k, k ′ ∈ K (C.CI, C ′ .SI) ∈ Binding b∈B b C = Name(Comp k ) C ′ = Name(Comp k ′ ) CItf ′ i i∈I = CItfs(Comp k ) i ∈ I CI = Name(CItf ′ i ) m n∈N n = MethLabel(CItf ′ i ) n ∈ N m ′ n = mn{ {CI ← SI} } f ∈ N { -, -, -, -, -, (k →!Q_mn(f, arg), k ′ →?Q_m ′ n (f, arg)) → Q_mn(f, arg), [1] -, -, -, -, -, (k ′ →!R_m ′ n (f, val), k →?R_mn(f, val)) → R_mn(f, val) } [2] ⊆ SVB(Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C7
and the destination of the binding, i.e., a sub-component and its client interface. The only remaining non-trivial premise is m ′ n = m n { {SI ← SI 2 } }; it replaces in m n the occurrence of the interface named SI by the interface SI 2 . Indeed, remember MethodLabels contain the name of the invoked interface, this name must thus be updated when a request/reply/. . . is transmitted from an interface to another 7 . Similar premises, renaming an interface name, will also be used in rules [C6] and [C7]. The rst item of Rule [C5.1] synchronises the emission of a request by a delegate method with the inner component bound to the concerned internal client interface. This action is also synchronised with the proxy for future that will receive the result computed by the request. The case [C5.2] concerns the corresponding reply that is issued by the inner component, this reply is sent to the outside of the composite component. Note that the inner component emits a value for future q, that is directly synchronised with the future proxy number q of the composite component; the identier of the future to be sent to the outside becomes f ; it is retrieved from the future proxy, and an action !R_m ′ n (f, val) is emitted. At the same time, a recycling action is triggered in the proxy manager.

The second rule [C6] manages export bindings, it also has one item for request emission [C6.1] and another one for reply reception [C6.2]. A request emitted by the inner component on the rst side of the binding is enqueued in the encompassing composite component (at the other side of the binding). Replies are redirected when received by the encompassing component: when the reply for future p is received, the future proxy at index p is used to retrieve the future identier f , and nally the result val is transmitted, associated with the future f , to the inner component indexed by k. At the same time, a Recycle action is triggered in the adequate proxy manager.

Rule [C7] deals with bindings between two inner components. It considers a binding between an interface of component C and an interface of component C ′ . It nds k, the index of C, and k ′ , 7 at this point, other meta-informations encoded in the method label should also be updated.

the one of C ′ ; the rule directly transfers requests [C7.1] and replies [C7.2] from one component to the other for all the methods of the client interface bound. Like in the preceding rules, the name of the interface is updated during transmission. This section presented a behavioural semantics for hierarchical components communicating by asynchronous requests which are transmitted between components, where composite components just forward requests to the adequate destination. We encode replies by means of futures, and composite components act as reply forwarders, independently from the rest of the component; this avoids some of the limitations induced by the mono-threaded nature of our components. The next section will dene more advanced features allowing more asynchronous or dynamic behaviours.

Advanced features

In this section we focus on three crucial advanced features of GCM components, which are general enough to be applicable to most other component models. First, we will introduce behavioural models for rst-class futures in order to allow for more asynchrony between components. Second, we will dene a model for binding controllers allowing for a more dynamic component model, where the bindings between components can be changed at runtime. Of course, this step supposes that (an abstract representation of the) potential bindings are known when the model is generated, or else we could not generate a full behavioural model. Usually, dynamic component reconguration also includes starting/stopping a component and adding a component inside another one. Concerning start/stop capacity, it is relatively easy to dene a life-cycle pNet that would control the rest of the pNet. For the second case, as the specication of the component must be known at model-generation time, a component that is not yet added is similar to a component that is already here but totally unbound and stopped. This is why we only focus here on the specication of dynamic component bindings. Section 5.3 species the behaviour of multicast interfaces equipped with a binding controller. Those interfaces allow the easy denition of components performing some kind of group communications: multicast are one-to-many interfaces. One-to-many interfaces are frequently used in distributed systems where one computation/information is to be sent, sometimes cut into pieces, to several destinations. Finally, Section 5.4 will informally explain how to encode bindings that involve the client and the server interface of the same component, and then overcome the main limitation introduced in the denition of well-formed components, and.

In this section, we will specify new rules for the behavioural denition of those advanced features. In practice, we build new behavioural semantics by modifying the semantics dened in the preceding section, for this we use two additional operators on pNets: : Let pNet be a pNet and A be an indexed set of labels (strings); pNet A returns a pNet similar to pNet but with restricted synchronisation vectors. The synchronisation vectors of pNet A are the ones of of pNet except all the synchronisation vectors containing an element of A as part of their global synchronisation label. For example, if m belongs to A then all the vectors containing m in their global label will be removed, in that case the global labels concerned could be: Q_m, !Q_m, ?Q_m, R_m, Serve_m, . . . . Remember that method labels contain the name of the interface that contains the method and consequently, removing a method label cannot remove an action concerning another method with the same name in another interface.

′ .SV ′ k = α j∈J k j → α ′ k where α ′ k ∈ L, J k ∈ I P , J k ⊆ I ⊎ I ′ ,
and ∀j ∈ J k ∩ I. α j ∈ Sort(pNet j ), and ∀j ∈ J k ∩ I ′ . α j ∈ Sort(pNet ′ j ). Suppose additionally that the action labels

α ′ k belong to L. pNet ⊕ pNet ′ i i∈I ′ , SV ′ k k∈K ′
extends pNet with the new sub-pNets pNet ′ i . The synchronisation vectors are kept (they do not synchronise the new sub-pNets); and the new synchronisation vectors: SV ′ k k∈K ′ are added to the ones of pNet:

pNet ⊕ pNet ′ i i∈I ′ , SV ′ k k∈K ′ = P, L, pNet i∈I i ⊎ pNet ′ i i∈I ′ , SV k∈K k ⊎ SV ′ k k∈K ′

Semantics of First-class Futures

We call rst-class futures, the futures that can be transmitted between components before their value is known: without rst-class futures, a component must wait for the result of a request and perform a GetValue before being able to send this result to another component (inside a request parameter, or inside a request result). With rst-class futures, a component can send a generalised reference to the future, i.e. a reference that uniquely represents the future in the whole component system. This way, once the result is computed it is sent to all the components that hold a (generalised) reference to the corresponding future.

In the model presented in Section 4, composite components could act as reply forwarders which corresponds to some kind of limited rst-class futures. However, a service method of a primitive component that would return a future or send a future as request parameter has to wait until the adequate reply is received. This behaviour occupies the only thread of the primitive component and can create deadlocks.

We will consider in this section only the case when a future is transmitted as the single argument of a request. The case where a single future is returned as request result is similar, and closer to the reply forwarding mechanism implemented by the composite components. The case where a future is only a part of the transmitted object requires to reason on the abstract representation of the transmitted objects, which we do not do in this paper. Overall, we consider here the minimal case which is sucient and general enough to understand the mechanism of the generation of behavioural models for rst-class futures. A general study on the dierent kind of rst-class futures, their identication and a few usage scenarios more complex than the one presented here can be found in [START_REF] Cansado | Transparent rst-class futures and distributed component[END_REF]; however, compared to [START_REF] Cansado | Transparent rst-class futures and distributed component[END_REF], the approach presented here provides a complete formal specication of the generation of behavioural models.

Principles and Illustrative example

Figure 9 is a simple scenario demonstrating the transmission of a future value as a parameter of a remote request. The principle of this scenario is the following. The component A rst invokes a request on the component B (step 1); then the result of this invocation is sent as the single parameter of a request invocation to the component C (step 2). Possibly, the component C can try to access the future received, resulting in a wait-by-necessity (step 3). When the result is computed by B, it is returned to A and then to C (step 4), which releases the wait-by-necessity.

The pNet for the scenario described above is shown in Figure 10. The gure focuses on aspects related to the transmission of the future (denoted f in the code snippet, and indexed p as a local proxy) and its update. The generalised reference to the future is denoted gf. Generalised references, gf, now belong to the set of valid request arguments (denoted by the variable arg). The local future indexed p has a slightly dierent proxy able to emit a !Forward(gf, val) action. The generalised reference for the future is computed by composition of the proxy index p, and the component holding the proxy and method label, consequently the generalised reference gf is known and can be given at proxy creation time. Upon the invocation of Q_m2, gf is sent. When the request is handled by the component C, the call to the local method is intercepted by a specic pNet FutDetect. This pNet creates a local proxy for representing gf (Proxy_F1, indexed locally by q); q then replaces gf in the invocation. This local proxy for future waits for the Forward communication coming from the remote proxy, and can then be accessed by the service method Method_m2. We have a single PM_F1 proxy manager for all the rst-class proxies (Proxy_F1), it acts as any other proxy manager except that the rst-class proxy is given the generalised reference gf when dening the semantics, and it transmits gf when creating the proxy. It thus has a similar behaviour to the proxy manager for a composite component; it does not correspond to any method name, we re-use the proxy manager semantics, giving it a pseudo Inria method name: F 1. Consequently P M _F 1 = F 1 proxyManager .

It is crucial here to distinguish the two adjustments that have to be made to two dierent future proxies. First, all the future proxies must be able to send a !Forward action for forwarding the value they received, for them we will overload the existing proxy denition proxy . Second, a new kind of proxy, Proxy_F1, needs to be created; those proxies act as a local future proxy for a proxy received as request parameter.

Primitive Components: pNets and Synchronisation Vectors

To handle rst-class futures, it is not possible anymore to consider future identiers as integers that are locally unique. Future identiers need to be global references where unicity is guaranteed globally in the system. For this, we dened generalised references, where a generalised reference identies uniquely a future proxy, it is thus dened by the tuple: component name, interface, method, future identier. Let GRef be the set of all generalised references and let gf range over GRef. We can dene a constructor of generalised references GeneralisedRef:

GeneralisedRef : CName × Itf × MethodLabels × N → GRef
In this section we dene F1 the semantics of components with rst-class futures. As shown in the illustrative example, the pNet of the primitive component must be extended with proxies for storing locally rst-class futures received as parameters, called Proxy_F1 in Figure 10 and in the rules below, and a proxy manager managing those proxies. The proxy manager for rst-class futures is very similar to the ones shown before; like for composite components it receives a future reference and transmits it upon proxy creation, except this time the reference is a generalised one. GRef gf:GRef q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat q:nat ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) ?New_m(q,gf) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) !Call_m(q) Figure 11: Proxy for a rst-class future and Future Detector machine

?
Figure 11 shows the pLTS of a rst-class future proxy (a future that can be transmitted as request parameter), and of a FutDetect process that intercepts the local service of requests with a future as parameter. On the left part of the gure, the proxy for a future that can be transmitted as request parameter is a classical one except it can also send a Forward action (with the generalised reference as parameter) to transmit the future value outside the component. FProxy_m in the gure denes the new proxy creation semantics m, gf proxy ; it is used each time a proxy for a future that can be transmitted as request parameter is instantiated. The future detector pLTS is shown on the right part of Figure 11. It creates a local proxy before delegating the call. FutDetect_m denes the pLTS denoted by m FutDetect in the following.

We introduce a set L ′ that indexes the set of methods that can receive a future; L still indexes all the service methods. The service of each service method that can receive a future as Table 4: Synchronisation vectors related to client and server interfaces of primitive components for rst class futures.

The synchronised sub-pNets occur in the following order: Queue, Body, ServiceMethods, ProxyManagers, Proxies, FutDetect, PM_F1, Proxies_F1 -, -, -, i →?Call_mi(gf), -, -→ Call_mi(gf),

i ∈ L ′ gf ∈ GRef q ∈ N j ∈ L { -, !Call_mi(gf),
[1] -, -, i →?Call_mi(q), -, -, i →!Call_mi(q), -, -→ Call_mi(q),

[2] -, -, -, -, -, i →!GetProxy_F1(gf), ?GetProxy_F1(gf), -→ GetProxy_F1(gf),

[3] -, -, -, -, -, i →?New_F1(q), !New_F1(q, gf), q →?New_F1(gf) → New_F1(q, gf),

[4] -, -, j →?GetValue_F1(q, val), -, -, -, -, q →!GetValue_F1(val) → GetValue_F1(q, val),

[5] -, -, -, -, -, -, -, q →?Forward(gf, val) →?Forward(gf, val),

[6] -, -, -, -, -, -, -, q

→!Forward(gf, val) →!Forward(gf, val)} [7] ⊆ SV F1 S (m i∈L ′ i , L) P3 j ∈ J m i∈I i = MethLabel(CItf j ) i ∈ I
Futures for requests on mi can be sent as parameter

p ∈ N gf ∈ GRef -, -, -, -, j →i →p →!F orward(gf, val), -, -, -→!F orward(gf, val) ∈ SV F1 C (CItf j∈J j , CName) P4
parameter passes by an intermediate FutDetect_m process that creates a local proxy representing the transmitted future, it is denoted FD l in the equation below:

m l∈L l = MethLabel(SItf i∈I i ) m l∈L ′ l
are the methods that can receive a future as parameter

PM_F1 = F 1 proxyManager ∀l ∈ L ′ . FD l = m l FutDetect SV F1 = SV F1 S (m l∈L ′ l , L) ∪ SV F1 C (CItf j∈J j , CName) CName < SItf i∈I i , CItf j∈J j , M k∈K k > F1 = CName < SItf i∈I i , CItf j∈J j , M k∈K k > call_m l∈L ′ l ⊕ ←-------→ P, FD l l∈L ′ , PM_F1, ← ----------→ P, Proxy_F1 N , SV F1
The new pNet extends the old one thanks to the operator ⊕ dened previously. Concerning methods that can receive a future as parameter, direct Call invocations from the body to the service methods are removed by the operator. The new synchronisation vectors are dened in Table 4.

There The new synchronisation vectors on the client side of the primitive components allow the emission of Forward actions (rule [P4]): when a future proxy of kind FProxy_m emits a Forward, this Forward is sent to the outside of the primitive component.

Table 5: Binding synchronisation vectors for rst class futures.

The synchronised sub-pNets occur in the following order:

Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents

(C.CI, C ′ .SI) ∈ Binding b∈B b C = Name(Comp k ) C ′ = Name(Comp k ′ ) CItf ′ i i∈I = CItfs(Comp k ) i ∈ I CI = Name(CItf ′ i ) gf ∈ GRef ∃mn ∈ MethLabel(CItf ′ i )
. mn can pass a future as parameter -, -, -, -, -, (k →!Forward(gf, val), k ′ →?Forward(gf, val)) → F orward(gf, val),

∈ SV F1 B (Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C8 (This.SI, C.SI2) ∈ Binding b∈B b i ∈ I gf ∈ GRef SI = Name(SItf i ) C = Name(Comp k ) ∃mn ∈ MethLabel(SItf i )
. mn can pass a future as parameter -, -, -, -, -, k →?Forward(gf, val) →?Forward(gf, val)

∈ SV F1 B (Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C9 (C.CI, This.CI2) ∈ Binding b∈B b j ∈ J gf ∈ GRef CI = Name(CItf j ) C = Name(Comp k )
∃mn ∈ MethLabel(CItf j ). mn can pass a future as parameter -, -, -, -, -, k →!Forward(gf, val) →!Forward(gf, val)

∈ SV F1 B (Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k ) C10
First-class proxies As shown in the illustrative example, the proxy of future that can be transmitted to other components is slightly dierent from the denition of Section 4.1.5: it can additionally emit a !Forward action. This action has a generalised referenced to the future as parameter, it can be computed locally as it is only formed of the local future identier, the component, and the interface which are all known when the proxy is built. As mentioned above, for futures that can be transmitted, the proxy function is enriched as illustrated in Figure 11: m, gf proxy is dened by the pLTS FProxy_m(gf) in the gure. For the other futures, the denition of Section 4.1.5 is still valid.

Composite Components: New Synchronisation Vectors

Concerning composite components, the composition of the pNets is unchanged, we only need to add new synchronisation vectors for transmitting Forward actions between components, this is specied by the new behavioural semantics:

CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding b∈B b > F1 = CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding b∈B b > ⊕ SV F1 B (Binding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k )
The three rules of Table 5 dene the transmission of forward communications. Rule [C8] deals with brother bindings: consider two components at the same level, if one forwards a future value, the other should receive it. Rule [C9] (resp. [C10]) transmits forward reception (resp. emission) along import (resp. export) bindings.

Note that each gf ∈ GRef can easily be restricted; indeed the origin of the future (component, method label) is known and the future ow can be approximated.

Semantics of Binding Controllers

By nature, GCM inherits from Fractal reconguration capabilities. The component structure is known at runtime and can be introspected and modied dynamically. Mainly, Fractal and GCM provide capabilities for adding and removing components inside a composite component, and for changing bindings between components.

In the Fractal component model and in GCM, reconguration and in particular dynamic binding/un-binding of components is specied such that it is very close to what happens in objectoriented languages. In particular, the bind/unbind operations are addressed to the component that owns the client interface to be recongured, indeed if one thinks of a component as an object, it is the object that holds the reference to the target object. It is then this client interface that must change the reference it holds. In our behavioural semantics however, the synchronisation between components is done at the higher level in the hierarchy: this approach corresponds better to the denition of pNets and to the component structure. It is also more compositional:

the behaviour of a component is totally independent from the component to which it is bound.

Here, we want to specify binding controllers that are similar to Fractal ones in order to verify real Fractal/GCM applications. For this we will have to re-introduce some form of reference in the components: for each recongurable client interface, we will dene a bind operation that receives as parameter a reference to the server interface to be bound to this client interface (in practice this parameter can be the index in the list of interfaces/components that can potentially be bound). The reference will then be passed as parameter to the request emission, and at the higher level we will use this reference to send the request to the right target.

To dene recongurable bindings, we introduce targets, denoted by t, that range over the set of qualied references to interfaces (QName). We will write t = C.SI to check whether the reference contained in the variable t is the interface SI of the component C. In practice, t should store an index among the possible bindings, and t = C.SI will check if the index t corresponds to the interface SI of the component with name C.

To deal with recongurable interfaces, a preliminary step is to know which interfaces can be recongured: those interfaces will be assigned a binding controller as explained above. Additionally, it is necessary to know statically which set of interfaces can be bound to this one in order to generate the possible behaviours of the component system. We suppose there is a set TopBinding that over-approximates the set of all bindings a component system can contain. A practical way to specify this set could be to extend the ADL with a new kind of binding, a potential binding that can be activated at runtime but is not active upon instantiation. The allowed recongurations would then only be the ones that activate a potential binding.

Principles and Illustrative Example

For encoding recongurable bindings in our behavioural specication, we follow the principles described below.

A component is endowed with a Binding Controller (BC) interface to bind and unbind its client interfaces to other components through primitive bindings.

The binding controller pLTS attached to each interface (see Figure 12) controls the bindings of a given client interface. It receives the control actions (?Bind(t) and ?Unbind) and emits status actions (!Bound(t) and !Unbound) that are used to allow the component to forward the request (!Q_m(f, arg)) to the appropriate bound interface. The target is, in a rst time attached to the request emission. Then, the encompassing composite component will use this target to synchronise the adequate components. The distinguished action (Error(Unbound)) visible from the higher levels of hierarchy is triggered whenever a request is performed over an unbound interface. We symbolise the branching between the two components by some guarded invocation 12; in the synchronisation vectors we will check in the premises of the rules whether t = S1.Itf in order to trigger the right invocation.

Inria M P5.4 P5.2 P5.3 P5.1 Queue Primitive + BC !Q m(f, t, arg) [t=S1.Itf ] Q m(f, arg) [t=S2.Itf´] Q m(f, arg) Body !Q m(f,

Recongurable Primitive Components: pNets and Synchronisation Vectors

The semantics for recongurable primitive components supposes that the set of client interfaces that can be congured is known; it is denoted CItf j∈J ′ j , it is a subset of the set of client interfaces CItf j∈J j of the component. To provide reconguration capacities inside the pNet model for a primitive component, we add a family of sub-pNets encoding the binding controller. This family has as many elements as there are recongurable interfaces. Each binding controller is dened by the pLTS shown in Figure 12: BC is a function that takes a client interface, and returns a binding controller pLTS as described in Figure 12: the process BC Itf i in the gure denes the value of Itf i BC .

Additionally, the request emission for those interfaces has to be synchronised with the status of the binding controller. For this we remove ( ) the synchronisation vectors for emitting requests on those interfaces and replace them by the new ones dened below (⊕). Finally, now that the bind and unbind requests are two new kind of non-functional requests, the set NF introduced in Section 4 is non-empty: NF = [ j∈J ′ ,t∈QName {Bind_Itf j (t), Unbind_Itf j } where CItf j∈J ′ j are the recongurable interfaces This implies that the request queue and the body of the primitive take into account binding requests.

BC is the behavioural semantics of a component equipped with recongurable interfaces. The rule below denes this semantics for primitive components:

m l∈L l = MethLabel(SItf i∈I i ) CItf j∈J ′ j are the recongurable interfaces j ⊆ J ′ m l∈L ′ l = MethLabel(CItf j∈J ′ j ) ∀j ∈ J ′ . BCj = CItf j BC SV BC = SV BC C (CItf j∈J ′ j , L) CName < SItf i∈I i , CItf j∈J j , M k∈K k > BC = CName < SItf i∈I i , CItf j∈J j , M k∈K k > (!Q_m l ) l∈L ′ ⊕ ← --------→ P, BCj j∈J ′ , SV BC
l ∈ L j ∈ J ′ m i∈I i = MethLabel(CItf j ) i ∈ I t ∈ QName f ∈ N { -, !Bind_Itf j (t), -, -, -, j →?Bind(t) → Bind_Itf j (t), [1] -, !Unbind_Itf j , -, -, -, j →?Unbind → Unbind_Itf j , [2] -, -, l →!Q_mi(f, arg), -, -, j →!Bound(t) →!Q_mi(p, t, arg), [3] -, -, l →!Q_mi(f, arg), -, -, j →!Unbound → Error(Unbound ), [4] !Serve_Bind_Itf j (t), ?Serve_Bind_Itf j (t), -, -, -, -→ Serve_Bind_Itf j (t), [5] !Serve_Unbind_Itf j , ?Serve_Unbind_Itf j , -, -, -, -→ Serve_Unbind_Itf j } [6] ⊆ SV BC C (CItf j∈J ′ j , L)

P5

The new synchronisation vectors for client interfaces are dened by rule [P5] shown in Table 6. ] synchronise the request queue with the body in order to serve bind and unbind requests. The target of the invocation will be used at the higher level in the hierarchy, as expressed below.

Items

Recongurable Composite Components: pNets and Synchronisation Vectors

First of all, a composite component can be assigned binding controllers allowing its client interfaces to be bound to a new target. The introduction of such binding controllers is extremely similar to the case of the primitive components. We do not formalise it here, the only two technical dierences are: the number of elements of the pNet is dierent, and the intercepted requests are emitted by the Deleg_m i sub-pNets instead of the service methods. Also, as an internal client interface corresponds to each server interface, the server interfaces can be assigned a binding controller if they are recongurable. Considering their similarity with the case of primitive components, we do not describe formally here the binding controllers for composite components. More interestingly, targets of invocations should be used by the synchronisation vectors generated by the potential bindings. We describe in Table 7 the synchronisation vectors corresponding to bindings that can be recongured, those synchronisation vectors are able to use the target reference sent as argument to address the request to the bound component. The new behavioural semantics thus requires to replace the items transmitting requests for methods for recongurable interfaces by the ones dened in Table 7.

CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , TopBinding b∈B b > BC = CName < SItf i∈I i , CItf j∈J j , Comp k∈K k , TopBinding b∈B b > {Q_mn|mn belongs to a recongurable interface} ⊕ SV BC B (TopBinding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k , CName)
In fact the operator ⊕ is only used here to add new synchronisation vectors, no sub-pNet is added. The synchronisation vectors for replies are kept from the non-recongurable case, except that there must be one reply channel for each binding of TopBinding instead of each binding of Inria Table 7: Binding synchronisation vectors for recongurable composite components.

The synchronised sub-pNets occur in the following order: Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents, BC

(This.SI, C.SI2) ∈ TopBinding b∈B b This.SI is recongurable i ∈ I SI = Name(SItf i ) C = Name(Comp k ) m n∈N n = MethLabel(SItf i ) n ∈ N m ′ n = mn{ {SI ← SI2} } q ∈ N t = C.SI2
-, -, n →!Q_mn(q, t, arg), -, -, k →?Q_m ′ n (q, arg), -→ Q_mn(q, arg),

∈ SV BC B (TopBinding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k , CName) C11 (C.CI, This.CI2) ∈ TopBinding b∈B b C.CI is recongurable j ∈ J CI = Name(CItf j ) C = Name(Comp k ) m n∈N n = MethLabel(CItf j ) n ∈ N m ′ n = mn{ {CI ← CI2} } f ∈ N t = CName.CI2 ?Q_m ′ n (f, arg), -, -, -, -, k →!Q_mn(f, t, arg), -→ Q_mn(f, arg), ∈ SV BC B (TopBinding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k , CName) C12 (C.CI, C ′ .SI) ∈ TopBinding b∈B b C.CI is recongurable C = Name(Comp k ) C ′ = Name(Comp k ′ ) CItf ′ i i∈I = CItfs(Comp k ) i ∈ I CI = Name(CItf ′ i ) m n∈N n = MethLabel(CItf ′ i ) n ∈ N m ′ n = mn{ {CI ← SI} } f ∈ N t = C ′ .SI -, -, -, -, -, (k →!Q_mn(f, t, arg), k ′ →?Q_m ′ n (f, arg)), -→ Q_mn(f, arg), ∈ SV BC B (TopBinding b∈B b , SItf i∈I i , CItf j∈J j , Comp k∈K k , CName) C13
Binding. There is no need to use addressing in this direction: a single component will necessarily send each reply because a single one received the corresponding request. The synchronisation vectors shown in Table 7 replace the ones of Section 4.2 for dealing with recongurable bindings. Now, SV B receives an additional parameter: CName, the name of the composite component that contains the bindings. The rules of Table 7 are relatively straightforward: the target t is used and unied with one destination of a potential binding to trigger the right communication. Note that, in rule [C12], the encompassing composite is referred by its name, CName, and not by This because t is the reference that is stored in the binding controller of the contained component, and there is no reason to refer to the parent component by This.

Note that the initial state of the binding controllers is unbound. In practice, if the ADL of the system denes initial bindings, then it is necessary to change the coresponding initial states, either in the denition of the pLTSs of the binding controllers, or by initialising the request queues with a sequence of binding commands.

Multicast Interfaces

This section provides a model for multicast interfaces where the capabilities of the pNets' synchronisation vectors are fully used and allow one component to broadcast a request to several others, or one component to provide a reply that would reach the right index in a group of futures. For this, we dene richer future proxies that can handle a list of results, and provide a result as soon as enough results are available. This section denes MC , the behavioural semantics for components equipped with recongurable multicast interfaces. Figure 13 shows a primitive component with a multicast client interface. When a client interface is of type Multicast, it may have a variable number of outgoing bindings (it is bound to the server interfaces of several components). Invocations emitted by a multicast interface are broadcasted to all the server interfaces bound to it. In GCM, depending on the interface policy, arguments of requests emitted by the interface can be dispatched in a parameterisable manner. Here, we suppose that the argument is broadcasted to all the destination components. Then results will come back in an asynchronous way from the elements of the group. The encoding of multicast Figure 14: A Group Manager and a Group Proxy interfaces relies on the two pLTSs of Figure 14 for dealing with the specic future proxies:

!MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) !GetValue_m(f,vect) [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] [vect(n)!=undef] !GetNth_m

one Group Proxy Manager for each method of each Multicast interface: the left part of Figure 14 shows the process GrPM_m that denes the value of m proxyManager in case the method m belongs to a multicast interface. Compared to a classical proxy manager, each group proxy manager is also in charge of managing changes in the group content (bindings and unbindings). Each binding/unbinding operation targeted at a client multicast interface is thus broadcasted to all the group proxy managers of all the methods of this interface.

for each method in the Multicast interface, an indexed family of Group Proxies: the right side of Figure 14 denes a process GrProxy_m that overrides the value of m proxy in case m belongs to a multicast interface. Upon each request invocation, a corresponding proxy is activated and initialised. Each incoming reply to this request will update a result vector (additional conditions check that a given component does not reply twice). Results

Inria can be accessed by the service methods that can query either the result vector totally lled (GetValue_m), or a partially lled vector (WaitN_m). As in the case of the standard future proxies, group proxies can be Recycled, whenever it can be decided that it will never be used again.

Note that in the Group Manager pLTS, the group variable G is modied by !Bind and !Unbind messages. Each time the Group Manager activates a new Group proxy (!New_m message), it sends a copy of the value of G, so that even if recongurations occur, each proxy keeps its own copy of Group, on which the invocation has been performed.

Multicast Example

GrProxy m1[p] GrPM m1 GrPM m2 P6.1 P6.2 P6.3
P6. [START_REF] Barros | Behavioural models for distributed fractal components[END_REF][START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF][START_REF] Basu | Incremental component-based construction and verication of a robotic system[END_REF][START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF] P6.10 P6.9 The pNet of a primitive component with a multicast interface is shown in Figure 15, it corresponds to the primitive component that was shown in Figure 13. The gure shows the parts of the pNet that are specic to the handling of multicast interfaces. It shows that binding operations received in the queue are broadcasted to each group proxy manager of the targeted multicast interface. Then proxy creation (New_m) is synchronised similarly to the case of usual interfaces except that the current status of the multicast interface (G) is transmitted to the created proxy. The main specicity of the synchronisation vectors for multicast interfaces is the fact that a request emission is also synchronised with the corresponding proxy that sends the group G targeted by the invocation (!MC(G)), and the outgoing request also sends G as argument. This argument containing the invoked group will be used at the higher level in the hierarchy by the encompassing composite component. Consequently, G ranges over sets of qualied names. We will also use variable g for members of G: g ranges over qualied names. Finally, actions for accessing the group proxy (waitN_m, GetValue_m, GetNth_m) can be invoked by the service methods.

P6.5 !R m(f, val) GetProxy m1 GetProxy m2 ?R m1((p, id), val) ?R m2((p, id), val) !R m(val) ?Q Unbind Itfj(t) ?Q m(f, arg) ?Q Bind Itfj(t) Bind Itfj(t) Unbind Itfj(t) !Q m1(p, arg) !Q m2(p, arg) !Q m1(p, G, arg) !Q m2(p, G, arg) GrProxy m2[p] !MC(G) New m1(p, G) New m2(p, G) Recycle m2(p) Recycle m1(p) ∀m in {m1,m2} WaitN m(p, n) R WaitN m(p,
Figure 16 illustrates the principle of the synchronisation occurring at the higher hierarchical level, in the composite that contains the component with the multicast interface. Depending on the group targeted by the invocation, a dierent synchronisation vector is used, and the adequate server interfaces receive the invocation. As for recongurable interfaces, the queue and the body of the components that contain multicast interfaces must be able to accept and handle bind and unbind messages. Like for binding controller, the set of non-functional requests now contain Bind and Unbind requests.

B[1] B[2] B[n] Multicast Example !Q mi(p, arg) !Q mi(p, G,
However, in the case of multicast interfaces, the proxy has to know the group addressed by the invocation because it will contain as many entries for receiving replies as there are elements in the group. In our specication, to simplify notations, we rather create a bigger array of results but only the ones corresponding to elements of G will be used. Knowing G at invocation time is also useful to implement a GetValue primitive returning a result if all replies came back. It is important to note that the group G known by the proxy is the one that was active at invocation time regardless of bind/unbind operations that occurred after the invocation.

The way we handle recongurable multicast interfaces is relatively close to what we have shown in the previous section. However, there is no binding controller here. Instead, the role of the binding controller of the previous section is split between the proxy managers and the group proxies. The proxy managers receive Bind/Unbind actions and store the current value of the group, whereas the group proxies are responsible for emitting the current value of the group at invocation. Another dierence is to be noticed: in the case of a multicast interface, the unbind operation receives a target reference as a parameter. Indeed, contrarily to the usual binding controller, multicast interfaces are in general bound to several targets, it is thus necessary to transmit the reference of the target to be unbound.

Finally, the structure of future identiers has to be enriched for dealing with multicast interfaces: in the following a future identier, like f , p, can be either a classical future identier, or a couple made of a classical future identier and an index, the index being used to identify uniquely the destination of the invocation among G, the group of invoked components. This way we will be able to distinguish replies originating from two dierent members of the group, and concerning the same invocation. Consequently, we rely on a function Index G (g) that returns an integer for each g ∈ G. This index will be attached to the future identier to uniquely identify the destination of the multicast invocation. The function should be injective so that two targets cannot receive the same index; we let id range over those indexes Inria Table 8: Synchronisation vectors for multicast client interfaces in primitive components.

The synchronised sub-pNets occur in the following order: Queue, Body, ServiceMethods, ProxyManagers, Proxies

j ∈ J l ∈ L m i∈I i = MethLabel(CItf j ) i ∈ I p ∈ N CItf j is multicast { -, -, l →!GetProxy_mi, j →i →?GetProxy_mi, -→ GetProxy_mi, [1] -, -, l →?New_mi(p), j →i →!New_mi(p, G), j →i →p →?New_mi(G) → New_mi(p, G), [2] -, -, l →!Q_mi(p, arg), -, j →i →p →!MC(G) →!Q_mi(p, G, arg), [3]
-, -, -, -, j →i →p →?R_mi(id, val) →?R_mi((p, id), val), [START_REF] André | Composing Components with Shared Services in the Kmelia Model[END_REF] -, -, l →!Recycle_mi(p), j →i →?Recycle_mi(p), j →i →p →?Recycle_mi → Recycle_mi(p), [START_REF] Attiogbé | Checking Component Composability[END_REF] -, -, l →!WaitN_mi(p, nb), -, j →i →p →?WaitN_mi(nb) → WaitN_mi(p, nb), [START_REF] Barros | Behavioural models for distributed fractal components[END_REF] -, -, l →?R_WaitN_mi(vect), -, j →i →p →!R_WaitN_mi(vect) → R_WaitN_mi(p, vect), [START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF] -, -, l →!GetNth_mi(p, nb, val), -, j →i →p →?GetNth_mi(nb, val) → GetNth_mi(p, nb, val), [START_REF] Basu | Incremental component-based construction and verication of a robotic system[END_REF] -, -, l →?GetValue_mi(p, vect), -, j →i →p →!GetValue_mi(vect) → GetValue_mi(p, vect), [START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF] -, !Bind_CItf j (t), -, j →(i ′ ∈ I →?Bind(t)), -→ Bind_CItf j (t), [START_REF] Baude | GCM: a grid extension to Fractal for autonomous distributed components[END_REF] -, !Unbind_CItf j (t), -, j →(i ′ ∈ I →?Unbind(t)), -→ Unbind_CItf j (t), [START_REF] Beisiegel | SCA service component architecture, assembly model specication[END_REF] !Serve_Bind_CItf j (t), ?Serve_Bind_CItf j (t), -, -, -, -→ Serve_Bind_CItf j (t), [START_REF] Bensalem | Compositional verication for component-based systems and application[END_REF] !Serve_Unbind_CItf j (t), ?Serve_Unbind_CItf j (t), -, -, -, -→ Serve_Unbind_CItf j (t)} The pNet of a primitive component with multicast interfaces is similar to the pNet without multicast interfaces, except that the proxy managers and the proxies for methods of multicast interfaces are replaced by the pLTSs dened in Figure 14:

proxyManager is overloaded for multicast interfaces, it returns the classical proxy manager of Figure 6 for a singleton interface, and the new one of Figure 14 for a multicast interface, and similarly for proxy . Additionally to these changes in the behavioural semantics of future proxies and their managers, the synchronisation vectors are modied as shown in the next rule: synchronisation vectors containing the name of a multicast interface are replaced by a new one. Note that, as method labels contain the name of the interface, (CItf j∈J ′ j ) removes all the synchronisation vectors containing the name of a method m i of an interface CItf j among its action labels.

m l∈L l = MethLabel(SItf i∈I i ) CItf j∈J ′ j = {CItf j |j ∈ J ∧ CItf j is multicast} CName < SItf i∈I i , CItf j∈J j , M k∈K k > MC = CName < SItf i∈I i , CItf j∈J j , M k∈K k > (CItf j∈J ′ j ) ⊕ SV MC C (CItf j∈J j , L)
The synchronisation vectors for the multicast interface of a primitive component are dened in Table 8, they correspond to Figure 15. We introduce a new variable vect, similarly to arg and val, vect ranges over arrays of values. In the rules, we write (i ′ ∈ I →(?Bind(t))) to represent the family ?Bind(t) i ′ ∈I ; this represents a synchronisation vector that broadcasts the action ?Bind(t) to all the elements inside I, here all the proxy managers of the recongured interface. Cases [P6.1] and [P6.2] are used to create a proxy: compared to Section 4.1, the content of the group targeted by the invocation (G) is transmitted to the proxy. The element [P6.3] expresses request emission, with the proxy emitting the adequate value of G. Compared to singleton interfaces, reply reception uses the fact that an index id is attached the future, and

[len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G)] [len=length(G

!MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G)

Figure 17: The Proxy of a Multicast interface inside a Composite component transmits this index to the future proxy for multicast interface. Recycle [P6.5] is similar to the non-multicast case. Elements [P6.6] and [P6.7] are used for waiting for a given number, nb, of responses: rst, nb is sent to the proxy (WaitN_m i action), and then a reply is sent back to the service method by R_WaitN_m i . The two next rules [P6.8] and [P6.9] do not require to work in a request/reply manner, the proxy can directly emit GetNth_m i and GetValue_m_m i actions when they are enabled, i.e. when the necessary replies have arrived. The next two elements ([P6.10] and [P6.11]) deal with the reconguration of the multicast interface: they transmit bind and unbind orders from the body to all the group proxy managers corresponding to the recongured interface. The two last items [P6.12] and [P6.13] synchronise the request queue with the body in order to serve bind and unbind requests.

Multicast Interfaces for Composite Components

Concerning composite components, two aspects have to be added. First, composite components can also have multicast client interfaces. Compared to other recongurable interfaces, multicast interfaces have to deal with future proxies in a special manner, the behaviour of a composite multicast interface is dierent enough from the primitive ones to necessitate its complete specication. Second, composite components have to encode the synchronisation between multicast interfaces and the plugged components.

Concerning the rst point, to be precise, multicast interfaces can be either external client interfaces, or internal client interfaces (that correspond to multicast external server interfaces). There is no multicast server interface, thus to state that an internal client interface is multicast, we tag as multicast the corresponding server interface (see Section 2.3.3).

Similarly to primitive components, the proxy managers and the future proxies are dierent for multicast interfaces compared to normal interfaces. The proxy manager for a method of a multicast interface is the same as the one for primitive components (see Figure 14). The group proxy is quite dierent and quite simpler than the primitive component case, it is shown in Figure 17: the process GrProxyComposite_m denes the behavioural semantics of the proxy for a multicast interface of a composite component: m proxy . After creation and emission of a !MC (G) action, this future proxy accumulates replies and when all futures have been received, a !R_m(f, vect) action is emitted. Note that, as there is no application logic encapsulated in the composite component, a given policy must be chosen to know when a reply is issued from a multicast interface belonging to a composite. Here we choose to reply the whole vector of Inria replies when it is completely lled. It would also be possible to implement a dierent policy, for example return the most frequent result, this would be particularly adapted to the case where the multicast interface targets several replicas of the same component for redundancy purposes. The behavioural semantics of proxies and their managers feature the new semantics for multicast interfaces. Then, the behavioural semantics of a composite component supporting multicast interfaces is the following: it redenes the synchronisation vectors for transmitting request and replies concerning multicast interfaces, and the ones concerning the group proxies and their management. The second rule [C15] expresses the creation of a new future proxy and the binding/unbinding of interfaces, it is very similar to the primitive component case, except that, as it is the case for a normal interface of a composite component, the future corresponding to the request served by the composite component is transmitted to the proxy.

We now describe how we generate synchronisation vectors for bindings involving a multicast interface. When dening well-formed components, we required that there is no looping binding and two bindings from the same MC interface do not reach the same component; this allows

Multicast Composite Example

Deleg m2 C16.2 C15.1 C16.3 C16.1 C15.2 C14.2 C14.1 C15.1 C15.4 C15.3 Body C15.3 C15.4 C15.2 C19 Sub-components New m2(p) !Q m2(p, G, arg) !MC(G) !R m2(f, vect) !Recycle m2(p) ?Q Unbind Itfj(t) ?Q m2(f, arg) ?Q Bind Itfj(t) ?R m1(p, f i, vect) !R m2(p, k, val) New m2(p, f, G) GetProxy m2(f ) !Q m1(p, G, arg) !MC(G) R m1(p, id, val) !R m1(p, f i, vect) Deleg m1 New m1(p, f i, G) New m1(p) GetProxy m1(f i) Unbind Itf1(t) Bind Itf1(t) Serve mi(f, arg) Serve bind Itfj(t) Serve unbind Itfj(t) !Recycle m1(p) Bind Itf2(t) Unbind Itf2(t) Itf1 GrProxyC m1[p] Itf1 GrPMC m1 Itf2 GrProxyC m2[p] Itf2 GrPMC m2 !Q m1(f i, arg) R m1(p, vect) Queue !Call m2(f, arg) !Call m1(f i, arg)
Figure 19: pNets for the Composite component with multicast internal and external interfaces us here to write synchronisation vectors for expressing multicast interfaces. Indeed, those restrictions ensure that in each of the synchronisation vectors expressed below, each sub-pNet of the composite pNet performs a single action in a given synchronisation vector. Section 5.4 will discuss how to avoid this limitation.

In order to dene recongurable bindings for multicast interfaces, similarly to Section 5.2, we rely on TopBinding, the maximal set of bindings that can exist. Then we dene four rules for building synchronisation vectors from TopBinding. For each of the three rst rules, we build G max the maximal set of qualied names that can be bound to the considered multicast interface. Then we consider all the possible subsets G of G max ; these are the possible sets on which the request invocations originating from the multicast interface can arrive. Note that SV B has now CName as additional parameter, it is the name of the composite component that contains the bindings. We use two auxiliary functions for computing G max , and for obtaining the index of the component inside a qualied name:

Gmax(TopBinding b∈B b , QName, CName) = {C.Itf|(QName, C.Itf) ∈ TopBinding b∈B b ∧ C = This}{ {This ← CName} } Target(C.Itf, Comp k∈K k ) = k ∈ K such that C = Name(Comp k )}
Note that Gmax renames the occurrences of This into CName because when the encompassing composite is bound, it is referred by its name, not This.

Table 10 shows rules for building synchronisation vectors related to bindings involving a multicast interface. Rule [C16] deals with the case when a server interface is multicast, or more precisely an internal client interface is multicast. The item [C16.1] in the synchronisation vector expresses request emission. Each request emitted by a delegation method is broadcasted to the bound interfaces, where the destination set G is taken from the adequate group proxy. For each destination of the invocation g ∈ G, the index of the target component is obtained thanks to the Target function; then Index G (g) is attached to the future identier. Replies can originate Inria Table 9: Synchronisation vectors for multicast interfaces in composite components.

The synchronised sub-pNets occur in the following order: Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents

j ∈ J m k∈K k = M ethLabel(CItf j ) k ∈ K p ∈ N CItf j is multicast { -, -, k →!Q_m k (p, arg), -, j →k →p →!MC(G), -→!Q_m k (p, G, arg), [1]
-, -, -, -, j →k →p →?R_m k (id, val), -→?R_m k ((p, id), val)}

[2] ⊆ SV MC C (CItf j∈J j , Itf h∈H h ) C14 h ∈ H m k∈K k = M ethLabel(Itf h ) k ∈ K f, p ∈ N Itf h is multicast { -, -, k →!GetProxy_m k (f ), h →k →?GetProxy_m k (f ), -, -→ GetProxy_m k (f ), [1] -, -, k →?New_m k (p), h →k →!New_m k (p, f, G), h →k →p →?New_m k (f, G), -→ New_m k (p, f, G)} [2] -, !Bind_Itf h (t), -, h →(k ′ ∈ K →?Bind(t)), -→ Bind_Itf h (t), [3] -, !Unbind_Itf h (t), -, h →(k ′ ∈ K →?Unbind(t)), -→ Unbind_Itf h (t), [4] !Serve_Bind_Itf h (t), ?Serve_Bind_Itf h (t), -, -, -→ Serve_Bind_Itf h (t), [5] !Serve_Unbind_Itf h (t), ?Serve_Unbind_Itf h (t), -, -, -→ Serve_Unbind_Itf j (t)} [6] ⊆ SV MC C (CItf j∈J j , Itf h∈H h ) C15
from each g member of G independently; overall, we build one reply vector for each element of G max . The synchronisation vectors for replies are split into two vectors compared to singleton interfaces: the return of results from sub-components [C16.2] is done independently from the reply of the overall result [C16.3], the second only occurs when the vector of replies is lled. The last item of the rst rule is in fact unrelated to bindings, it is however more natural to mention it here; it sends a reply out of the composite component when the vector of replies of a future proxy f of a multicast server interface has been completely lled. Method renaming (computation of m ′ g from m j ) relies on a function Itf that returns the interface of a method label.

The second rule [C17] deals with the case when a sub-component has a client multicast interface that sends request to other sub-components. The rules are quite similar to the previous case except that the emitter component has to be found (it is indexed by k). The synchronisation between sub components for the transmission of a request synchronises the emitter k with the elements of G, or more precisely with the sub-components indexed by Target(g) for g ∈ G.

Again, indexes of the destination components are attached to the future identier. The set of synchronised sub-components is a family of card(G) + 1 elements (remember that the denition of well-formed components ensures that k cannot be among the indexes in G). There is no need to specify a rule for replies here because the case of singleton interfaces still applies (except that it is instantiated for the maximal binding set, TopBinding, and that it returns a future identier that contains an index Index G (g)).

Rule [C18] deals with the case when a sub-component has a client multicast interface that sends a request to other sub-components, but also to the encompassing component. This rule applies when the invocation is performed on a target group G that contains CName.Itf where CName is the name of the composite component. Note that as bindings are recongurable, the composite component can be bound or not, and depending on whether it is bound, [C17] or [C18] applies. This rule only applies for request transmission, it is similar to the preceding rule except that the composite component also receives a request and that the set of destination sub-components is obtained from G ′ , the elements of G that are not the composite component.

The last rule [C19] deals with the sending of replies from a multicast client interface of the composite component to a sub-component. As replies for multicast are bound similarly to replies for singleton interfaces, the only dierence with the rules of Section 4 is when the client interface of the composite that sends the reply is a multicast interface. Indeed, when the interface is singleton the reply occurs as soon as one reply is received, and the proxy for future is used to rename the future identier (see Section 4.2). In the case of a multicast interface, the reply occurs independently from external communications when the vector of replies is entirely lled. This is visible in the rule because the global action is just an observable action of the form R_m instead of a communication reception of the form ?R_m. Rule [C14.2] that species the reception of the reply ?R by the composite still applies for receiving replies from other components.

5.4

Dealing with Binding Loops

The denition of Well-formed components in Section 2.3 does not allow a client interface to be bound to a server interface of the same component (binding loop). Also, the same multicast interface cannot be bound twice to the same component. Those restrictions do not exist in the GCM specications; we had to add them because synchronisation vectors do not allow two actions to occur simultaneously on the same sub-pNet. Additionally, performing this kind of bindings, especially binding loops, is sometimes useful in real applications. We explain below how to overcome this restriction; we focus on the binding loop case but a similar approach can be used to allow one multicast interface to be bound twice to the same component.

A rst idea to encode a binding loop could be to add an additional pNet that would transmit its input to its output; such a pNet would intercept the outgoing request invocations (and replies) and send them back to the same sub-pNet. While this approach is feasible it would un-synchronise the communication and thus does not t the original semantics for communications.

Instead, we should add an action to the pNet of the sub-component that performs both the sending and the reception of the request (it could be labelled Q &R_m). We thus add an action exported by the sub-component that at the same time enqueues and emits a request. For all interfaces of all components that support loop-bindings, such a compound action can be added.

One possibility would be to add a generic action product operator, as in the SCCS or Meije process algebras. But this would complexify too much the structure of actions, and the complexity of model-checking. Instead, we prefer to introduce local products in a very limited manner, when really required.

Concerning the restriction on multicast interfaces, a similar approach can be taken: a single action can be added that enqueues two requests at the same time (in an order arbitrarily chosen) and if the same component is bound twice, this compound action is triggered.

Full example

We will sketch here a small example illustrating the most important of the constructs dened in this article. This is an application called HyperManager which role is to monitor and control a pre-existing distributed application. The HyperManager itself (see Figure 20) is distributed, with a GCM composite encapsulating each of the original application legacy components, together with local monitoring and control GCM components. The application administrator can issue commands through a toplevel HyperManager component, for conguring the local legacy component, setting trace level attributes in the local monitors, and trace ltering rules in the global monitor, or performing reconguration operations by Binding or Unbinding local components from the global HyperManager.

This allows us to illustrate the construction of pNets for primitive and composite components, with future proxies, service and client delegation processes, attribute controllers, a multicast Additionally, this gives us the opportunity to discuss a number of implementation issues, and in particular of simplication of the generated pNet structure depending on the conguration of the GCM components considered. A brute application of the semantical rules from this article would produce an unnecessary number of management pNets, and we give example of optimisations that are applicable in a signicant number of situations. A full description of the implementation of the pNets construction, and of the optimisations, is out of the scope of this paper.

6.1

Structure of the pNets semantics

We illustrate here, in an informal manner, the construction of the pNets semantics of the Hyper-Manager example. We focus on the pNets hierarchy and their synchronisation vectors, dened in a graphical way (examples of the pLTS representing the basic blocks of the semantics will be given in Annex C). We give some gures about the complexity of this construction. We start, in Figure 21, with the pNet structure representing the semantics of one of the (identical) Local HM components. Only the structure of the pNets is dened here, some of the pLTSs involved in the composition will be dened in appendix C. Each Local HM is a composite containing a business process represented here by a Code pNet, a Local Manager primitive component managing the requests coming from the global HyperManager, and a Local Monitor listening to monitoring messages coming from Code.

Remark that the semantic rules above dening the produced pNet structures systematicaly build an intermediate pNet containing all sub-pNets for the sub-component of a composite (resp. the sets of proxies, proxy managers, deleg methods, etc). These intermediate pNets simplify the writing of the rules, but are unnecessary when building a particular instantiation, and we have omitted them in the drawings.

Logic Logic GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p] GrProxy_config[p]

?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_config(fid,cmd) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) ?Q_traceLvl(fid,lvl) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(fid,code) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) !R_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd) ?Q_config(p,cmd)

!Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Set_traceLvl(lvl) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !Q_traceEvt(evt) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl)
?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACSet_traceLvl(lvl) ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl ?Q_ACGet_traceLvl The Local HM composite has a very simple conguration: it receives requests on a single service interface, and directly passes these requests to the Local Manager sub-component, it has a single client interface whose methods have a void return type, and it has no reconguration features. This is a pattern that allows us to omit its whole control structure (Queue, Body, and proxies), and to synchronise directly the interface events with the corresponding inner pNets.

!R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl
The Local Manager primitive component has a standard pNet structure, with: a service interface with 2 service methods cong and trace that go through the Queue and Body pNets, before being routed towards their respective methods. a single client interface Cong with a single method cong, but that may be called several times from within the cong method. This interface requires a proxy manager and a family of future proxies Proxy_cong[p]. the cong service request requires a result code, so we have a returning !R_cong message, while the trace request simply forwards its command to the Local Monitor component, without requiring a return message.

The Local Monitor primitive component has a quite simple pNet structure: it has a queue listening to requests from the Code, but also to Set_traceLvl requests addressed to the TraceLvl attribute controller (see Annex C, Figure 26). It has a single (client) interface, with a single method requiring no answer, so it needs no proxies.

The Code object is not a GCM component, but rather a simple encapsulation of legacy code.

The API entry and return points are directly connected to the business code itself.

We move now to Figure 22, and explain the structure of the Global HM composite. This part features a complete pNet infrastructure in the composite membrane, and the management of a recongurable multicast client interface.

?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1

!Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C1(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt) !Q_trace_C2(evt)
!call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_traceFilter_S1(fid,fi) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1(fid,cmd) !call_config_S1 ( ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_config_S1(fid,cmd) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Q_traceLvl_S1(fid,lvl) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Q_traceFilter_S1(fid,fi) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?Unbind_M1(i) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) ?R_config(fa,codes) The Global HM composite has two sub-pNets for its internal sub-components, and a full set of pNets modelling its membrane, namely: a Queue receiving requests both from its service interface S1 and from the Global Manager sub-component, a body dispatching these requests to the Global Manager or to the controllers (Deleg, GrPM) of the multicast interface M1. On the M1 interface, only the cong method requires an answer, and has an indexed family of group proxies, managing the R_cong return messages. The GrProxy_traceLvl proxy role is only to store the group value (G) before sending the broadcasted request, so it only needs one instance, and no recycling. Last, the cong_S1 service method requires an answer, so it has a set of controllers (Deleg, PM, Proxy) managing this future.

!call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt) !call_trace_S2(evt)
The Global Manager and Global Monitor primitive components are very similar to the Local Manager and Local Monitor.

The last step is to assemble the toplevel composite, including the (dynamic) modelling of the multicast binding. In the current version of the Fractal/GCM ADL, we have no possibility for specifying this architecture in a parameterized manner: the (maximum) number of Local HM components must be known from the beginning. Only the group G may vary dynamically, by the eect of Bind/Unbind operations.

In Figure 23 we show this toplevel pNet, for a conguration with a maximum of 3 local components. As we do not show here the state machines (pLTSs) of the controllers, the initial ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_config((p,i1),cmd) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) ?Q_traceLvl((p,i1),lvl) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !R_config((p,i1),code) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?R_config((p,i),code) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_trace_S2(evt) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_config((p,i3),cmd) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl) ?Q_traceLvl((p,i3),lvl)

!R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !R_config((p,i3),code) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt)
?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_config((p,i2),cmd) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) ?Q_traceLvl((p,i2),lvl) The Toplevel HM composite component has no need for membrane components, with an argument similar to theLocal HM case: all requests on the service interface, including bind/unbind requests, are simply forwarded to the Global HM sub-component. The interesting part here is the dynamic multicast bindings between the Global and Local HM components 9 . All synchronisation vectors between the !Q_cong and !Q_traceLvl ports of the Global HM and the corresponding input ports of the Local HMs are guarded by a predicate testing the value of the group parameter. Each of these synchronisation vectors models the synchronous sending of the messages to all currently connected Local HMs. The other way round, the !R_cong messages from each Local HM are synchronised with the corresponding port of the Global HM, with the index of the emitting group member inserted as explained in rule [C16].

!R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !R_config((p,i2),code) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Q_TraceEvt(evt) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Bind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !

Discussion

The implementation of this semantics will only be usable in practice if we are able to dene signicant optimisations on the generated pNet structure. We have sketched some of the main structural optimisations in this section, but the resulting model size is still quite big: let p be the number of proxies per proxy family, and l be the number of local HMs, then we have (parameterized) synchronisation vectors. For a typical small instantiation of l := 3, p := 3, we get 66 basic nets and 225 parameterized vectors, that is more or less 2 orders of magnitude bigger than the last use-case we published [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF].

9 for the sake of readability, we have omitted the connections for the !Q_traceLvl broadcast messages

In this previous case-study, we showed how to combine 3 main techniques to master the stateexplosion of such systems, namely data-abstraction, compositional construction/minimization, and distributed model-checking. Naturally all will be useful here, but we want to highlight the rst one that will probably be very sensible here: many of the parameters that occur in the actions of our behaviour rules may be safely abstracted away in specic congurations (like the optimisations we described previously), others will have to be abstracted in a manner depending on the formulas we want to prove. Naturally, we want to validate formally all these optimisations.

Related Work

Component-based development has in recent years become an established approach. It shown successes in many application domains such as in distributed and embedded systems. There are several component models that are supplied for building complex systems: Fractal [START_REF] Bruneton | An open component model and its support in java[END_REF], Ptolemy [START_REF] Eker | Taming heterogeneity -the Ptolemy approach[END_REF], CCM [START_REF]The Common Component Architecture (CCA) Forum home page[END_REF][START_REF]CORBA Component Model Specication, omg headquarters edition[END_REF][START_REF] Beisiegel | SCA service component architecture, assembly model specication[END_REF], AADL, and GCM [START_REF] Baude | GCM: a grid extension to Fractal for autonomous distributed components[END_REF]1]. But there are only a few that have a theoretical framework that allows reasoning about modelled systems and verication of their behavioural properties.

Some of the formal developments around components are done with objectives very dierent from ours. For example, the formalisation of the Fractal model in Alloy [START_REF] Merle | A formal specication of the Fractal component model in Alloy[END_REF] brings several interesting properties, but they are mainly related to the model itself more than to the component applications. Similarly, a formal model of GCM has been specied in Isabelle/HOL [START_REF] Henrio | A framework for reasoning on component composition[END_REF], while it gives an interesting framework to reason on the component model and prove some of its properties, it is not adapted to prove the correct behaviour of applications. A formal framework for reasoning on futures has been dened in [START_REF] Frank | A complete guide to the future[END_REF], but the authors did not provide, to our knowledge, the tools to use their equations in order to automatically or semi-automatically prove properties on programs. Behavioural specication, on the contrary, is better adapted to the correctness proofs for given applications. Among the researches dedicated to the component oriented behavioural verication that we are aware of, the closest are SOFA, Kmelia, STSLib, and BIP.

The SOFA system [START_REF] Bure² | SOFA 2.0: balancing advanced features in a hierarchical component model[END_REF] is a development and verication framework for large-scale distributed software systems based on hierarchical components. It uses behaviour protocols [START_REF] Plasil | Behavior protocols for software components[END_REF] to specify interactions between components in terms of ordering of method invocation events. Behaviour protocols are also used, at each level of the component hierarchy, to dene a black blox specication of the subsystem. The behaviour compliance and consent relations are dened on behaviour protocols based on their trace semantics, allowing to prove separately at each level of the hierachy the compliance of an implementation (called architecture) with its specication (protocol).

Behavior protocols can also be encoded e.g. in Promela, that allows for classical LTL modelchecking [START_REF] Kofron | Checking Software Component Behavior Using Behavior Protocols and Spin[END_REF]. Kmelia [START_REF] André | Adaptation for hierarchical components and services[END_REF][START_REF] Attiogbé | Checking Component Composability[END_REF][START_REF] André | Composing Components with Shared Services in the Kmelia Model[END_REF] is a component specication model based on the description of complex services. Kmelia and its toolbox COSTO can be used to model software architectures and their properties, these models being later rened to execution platforms. It can also be used as a common model for studying component or service model properties (abstraction, interoperability, composability), using various verication toolsets, including CADP, MEC5, and Atelier-B. To our knowledge, though, there is no explicit behavioural semantics dened for Kmelia applications.

The STSLib library [START_REF] Fernandes | The stslib project: Towards a formal component model based on sts[END_REF] provides a formal component framework that synthesizes components from symbolic protocols in terms of Symbolic Transition Systems (STS). Just as pNets, STS concisely represent innite systems, however STS rely on Abstract Data Types (ADT) which are more expressive than the Simple Types used in pNets but less intuitive for software engineers. Both formalisms rely on (N-ary) synchronization vectors, but in STS they are static whereas Inria in pNets they are dynamic. STSLib synthesizes components based on their STS protocols; a controller interprets the STS protocol and data from which the ADT is implemented (and generated) in Java. The communication in STS components is rather low level ; both emitter and receiver must agree to exchange a message, and there is no explicit notion of required nor provided services.

On the implementation side, the two approaches are quite dierent: the implementation of STS simulates the synchronisation vectors that can be expressed in the specication, whereas in our approach, we write only the synchronisation vectors corresponding to the possible communications between components. Our specication language is more independent from the middleware, and it allows us to express complex synchronisations. This allows us to reason on ecient, expressive, and proved communication mechanisms. Overall, even if the pNet formalism is approximately at the same level of abstraction as STS, in our approach, the programmer is rather exposed to a higher-level composition framework, closer to his usual programming and composition concerns.

BIP [START_REF] Bensalem | Compositional verication for component-based systems and application[END_REF][START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF] is a formal framework that allows building and analysing complex componentbased systems, both synchronous (reactive) or asynchronous (distributed) by coordinating the behavior of a set of primitive and heterogeneous components. A component's behaviour is described as a Petri net extended with data and functions, whereas coordination is described as interactions between components and scheduling policies between interactions. Even if the BIP framework allows powerful compositional reasoning on the system, it does not support the denition of parameterised components, nor does it allow explicit data transfer between components.

BIP is supported by a toolset including translators from various programming languages as Lustre and C into BIP, a compiler for generating code executable by a dedicated engine, and the verication tool D-Finder. This last tool ( [START_REF] Bensalem | D-nder: A tool for compositional deadlock detection and verication[END_REF]) is not a generic model-checker, but a specic tool for deadlock detection and diagnosis, allowing to address systems of large size, as shown e.g. in [START_REF] Basu | Incremental component-based construction and verication of a robotic system[END_REF][START_REF] Bensalem | Compositional verication for component-based systems and application[END_REF].

Conclusion

This article provides a formal framework for the generation of behavioural semantics of asynchronous distributed software components. Asynchronous software components provide a convenient programming abstraction for designing large-scale distributed systems, where each component acts as an autonomous entity, only communicating with the others by asynchronous communications. Behavioural semantics enable the generation of a model of the program behaviour; then its correctness can be veried using dedicated platforms, for example based on model-checking techniques. The main contributions of this article are: a minimal formal denition of pNets. This denition does not cover all aspects previously published, but constitutes a simpler core denition, self-contained and sucient for this article. a formal denition of GCM components, their abstract syntax, and a well-formedness criteria, together with an informal description of their semantics, a precise formal denition of the behavioural semantics of GCM, in the form of structural rules constructing pNet models, an illustrative example sketching ideas for using these rules in practice.

RR n°8167

Among these contributions, the main part concerns the behavioural specication of the most important Fractal/GCM features. For some of these, we have already described a behavioural semantics in previous conference papers, but only in an informal way. Here we have given a full denition, and a procedure for building their pNet models. This includes the basic structure for GCM components, request queues, body expressing the service policy, future proxies and proxy managers; it also denes the semantic artifacts needed for rst class futures, and for group communication over multicast interfaces, including management of group recongurations.

The example described in the last section is extracted from a new (yet unpublished) industrial use-case, and features all the aspects listed above, except for rst class futures. We also use this example to comment on the possible implementation of our semantic model generation, and to discuss a number of optimisation rules that would be important to take into account.

Naturally enough, we are currently working on a full implementation of this semantics in our VerCors specication and verication platform [START_REF] Cansado | Specication and verication for grid component-based applications: From models to tools[END_REF]. This eort is complemented by the case-study mentioned in the above paragraph, and will be clearly a dicult challenge in terms of state-explosion, and may be several orders of magnitude more complex than previous studies [START_REF] Ameur-Boulifa | Verifying safety of fault-tolerant distributed components[END_REF]. We also plan to extend this work in several directions. First there are still some GCM features that are not included in the current core semantics, and that are important in pratical applications. This is the case of Gathercast interfaces (see [START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF]), and the various policies for managing parameters distribution and results gathering. And there is much more to do about the reconguration features of GCM, either considering explicit reconguration scripts, or autonomic components.

But the pNets approach can easily be applied to other types of distributed languages or formalisms, in the way we have dealt with Active objects, Fractal components, and GCM. It encodes in a very exible and expressive way any kind of process composition, communication and synchronisation, provided it stays within the family of rst-order hierarchical structures. This rules out formalisms such as the Π-calculus or the chemical machine, but includes most component models (CCM, SCA, Creol, ...) and their implementations.

In a completely dierent direction, we plan to relate the behavioural semantics of this article with the more operational one dened in [START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF]. We have used the latter in our research on theorem-prover based formalisations and proofs for GCM, and relating the two semantics would give us powerful tools for dealing with properties of dynamicaly evolving applications, and in the longer term to combine model-checking and theorem proving methods to reason about realistic applications.

A An operational semantics for pNets

This appendix provides an operational semantics for the pNet model; it is based on a valuation domain for the variables of the pNet, that can be nite, innite, or even contain new variables.

To give a semantics to pNets, we need a unique valuation domain D. This domain can possibly be a countable instantiation domain for each variable. To simplify the semantics, we require that it is possible to decide whether a boolean expression in D is true, and to decide whether two expressions have the same value (e.g. when two action labels are the same). If we choose a nite domain for each variable and if each pLTS has a nite set of states, the semantics of the pNet will be a nite LTS that can be used in a nite-state model-checker.

We let φ = {x j → V j |j ∈ J} be a valuation function where x j range over variables of the considered pNet (each variable must be given a value), and V j ∈ D. Such a valuation maintains a mapping from variables to values. For a term t ∈ T P , tφ ∈ D is the value of the term obtained by replacing each variable by their values given by φ. A valuation can be applied to expressions, actions, or even indexed sets. In all cases, the variables are replaced by their value and the new expressions are evaluated. The set of valuation functions, Φ, allows the precise denition of the state-space to be considered: only valuation functions such that φ ∈ Φ are considered. We dene an update operator + on valuations, where φ 1 + φ 2 replaces some of the values dened in φ 1 by the ones in φ 2 ; φ 2 might also dene new entries, formally:

{x j → V j |j ∈ J} + {x ′ j → V ′ j |j ∈ J ′ } = {x ′ j → V ′ j |j ∈ J ′ } ∪ {x j → V j |j ∈ J \ J ′ }
Note that variables are used locally to each pNet/pLTS, it is thus possible to use qualied names to avoid collision of variable names in the valuation. To simplify notations, in the semantics we suppose that variable names are unique. Consider a pNet pNet and an initial valuation φ 0 ∈ Φ associating a value to each variable of the pNet. The semantics of pNet, starting from a valuation φ 0 , is given by a LTS (or possibly a pLTS if D contains variables) where: states are hierarchical composition of product states of the sub-pNets, more precisely states are S(pNet) where: .n] ?Q_Mn+1φn+1

----------→ (M j φ j ) j∈ [1..n+1] ∈ Queue(M)

n ∈ N ∀j ∈ [1..n]. M j ∈ M ∧ φ j ∈ Φ (M j φ j ) j∈[1.
.n] !Serve_M1φ1

---------→ (M j+1 φ j+1 ) j∈ [1..n-1] ∈ Queue(M)

The most complicated part of the semantics is the way variables are dealt with in the pLTS:

only input variables, and assigned variables are allowed to change value in the valuation function.

This also applies (indirectly) to the queue where the valuation used in the action is in the Serve case constrained by the source state, and unconstrained in the case of a ?Q_M... transition. ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) ?Serve_Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) !Unbind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) ?Serve_Bind_M1(i) In Figure 24(right) the Body LTS is more complex, because the Global HM has a total of 4 service methods on its two service interfaces S1 and S2, plus 2 outgoing methods on the multicast interface M1 and 2 on C1. In addition we have two specic loops dealing with the Bind/Unbind requests managing the group at interface M1.

B Signature of Behavioural Semantics

MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig MethodConfig

?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) ?call_config_S1(cmd) !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3() !GetProxy_config_C3 In Figure 25 we give an example of a service method behaviour, expressed as a pLTS. This is the cong method of the Local Manager primitive component. It receives a request call on the service interface S1 with argument cmd. Then it sends a similar request to the Code component, which is bound on the client interface C3; this one is a standard remote request call, requiring the activation of a future proxy: the pLTS here requires a proxy (from the proxy manager), and gets back its value in the ?New_cong_C3 message, passes the future proxy id, together with the cmd argument, in the request !Q_cong_C3, waits for the return of the future value, Inria signals that the proxy can be recycled, and terminates by replying to the original request with the message !R_cong_S1(val).

TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl TraceLvl_AttrCtrl ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) ?Q_ACSet_traceLvl(val) lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val lvl:=val !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl !R_ACSet_traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl ?Q_ACGet-traceLvl !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl) !R_ACGet_traceLvl(lvl)

Figure 1 :

 1 Figure 1: A typical GCM assembly

  consists of a name CName, a set of Server Interfaces S Itf , a set of Client Interfaces C Itf , and a set of method denitions M k∈K k , where M k ∈ MSignature × pNet.

Figure 2 Figure 2 :

 22 Figure 2 illustrates a simple conguration of a primitive component. It exposes two service interfaces, which can receive requests. It has also a single client interface showing 2 client methods. The corresponding pNet system will be drawn in Figure 4.

  Binding ::= (QName, QName) (4) QName ::= This.Name | CName.Name

Figure 3 :

 3 Figure 3: Abbreviations for matching external/internal interfaces

  3 pNets: a formalism for dening behavioural semantics3.1Term algebra

Figure 4 :

 4 Figure 4: pNet for the Simple Primitive Component from Figure 2

?

  Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,arg) ?Serve_m0(fid,fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,arg) ?Serve_m1(fid,fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,arg) ?Serve_m2(fid,fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) !R_m0(fid) fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m1(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid) !R_m2(fid)

Figure 5 :

 5 Figure 5: Graphical representation of the behaviour of the Body

  free=true] !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(p) !New_m(.free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false Pool_Proxy(p).free:=false ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(.free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true Pool_Proxy(p).free:=true ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(p) ?Recycle_m(

  (p, val) ?R m2(p, val) ?R m1(p, val) CPM m4 CProxy m0[q]

?Figure 8 :

 8 Figure 8: Auxiliary processes proxy and delegate of composite components

  composite. This second rule uses the second argument of SV S , i.e., the list of client and server interfaces of the component. It deals with request service [C2.1], and subsequent calls [C2.2] to delegation pNets. Client-side synchronisation vectors are expressed by rules [C3] and [C4] of Table 2. Similarly to the server case, [C3] is specic to external client interfaces (given as rst argument of SV C ), whether [C4] is applicable to both external and internal client interfaces (the second argument of SV C ). Remember the internal client interfaces are the symmetric of server interfaces of the composite component. The rst rule exports request sending (Q_m) sent by delegate methods to the external components. Note that delegate methods are indexed by the method labels of the interfaces: in the pNet denition m l∈L l = MethLabel(SItf j∈J j ) ⊎ MethLabel(CItf i∈I i

⊕:

  For I ∈ I P and I ′ ∈ I P disjoint, let pNet = P, L, pNet i∈I i , SV k∈K k be a pNet and pNet ′ i i∈I ′ be a pNet family (possibly empty). Let SV ′ k k∈K ′ be synchronisation vectors Inria over I ⊎ I ′ , i.e., ∀k ∈ K

Figure 9 :Figure 10 :

 910 Figure 9: Scenario of rst-class future transmission

  gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef gf:GRef val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !Forward(gf,val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val) !GetValue_m(val)

  Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) ?Call_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(gf) !GetProxy_m(

  are seven entries in the new synchronisation vectors of rule [P3]. The two rst ones, [P3.1] and [P3.2] intercept the invocation from the body to the service method, those invocations now are intercepted by the FutDetect process. [P3.3] and [P3.4] deal with the creation of proxies for futures received as argument, which is quite similar to a classical proxy creation, as shown in Section 4.1. All the service methods can access the Proxy_F1 proxies by a GetValue_F1 8 , which is expressed by [P3.5]. The new future proxies are updated by a Forward action instead of a R action for usual proxies [P3.6]. Finally, [P3.7] emits a forward from the rst-class future proxy. Indeed, if the component that received a rst-class future itself forwards the future to another component (inside a request parameter), it also needs to forward the future value when it is known.

Figure 13 :

 13 Figure 13: Example with a Multicast Interface

  nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(G) nbWait:=length(undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef.

  (f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(n)) !GetNth_m(f,n,vect(

Figure 15 :

 15 Figure 15: pNet model for Figure 13

Figure 16 :

 16 Figure 16: Dynamic Connector for a Multicast Interface

  )] !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) !R_m(f,vect) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(f,G) ?New_m(fundef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] vect:=[undef..undef] len:=0 len:=0 len:=0 len:=0 len:=0 len:=0 len:=0 len:=0 len:=0 len:

Figure 18 :

 18 Figure 18: A Composite component with multicast internal and external interfaces, VCE graphics Figure 19 illustrates the construction of synchronisation vectors for a composite component having one internal client multicast interface, and one external client multicast interface. The rules for generating the synchronisation vectors dealing with the multicast server and client interfaces of a composite component are shown in Table 9. The rst rule [C14] denes the emission [C14.1] of a request on a multicast external client interface and the reception of a reply by this interface [C14.2]. The request is emitted by the delegation method indexed k, the proxy provides the target group G. The emission of request by internal multicast client interfaces will be described below as it depends on the bindings inside the composite component. The reply reception [C14.2] is similar to the reply reception in a primitive component [P6.4].The second rule [C15] expresses the creation of a new future proxy and the binding/unbinding of interfaces, it is very similar to the primitive component case, except that, as it is the case for a normal interface of a composite component, the future corresponding to the request served by the composite component is transmitted to the proxy.We now describe how we generate synchronisation vectors for bindings involving a multicast interface. When dening well-formed components, we required that there is no looping binding and two bindings from the same MC interface do not reach the same component; this allows

Figure 20 :

 20 Figure 20: Component Structure of the Full Example

Figure 21 :

 21 Figure 21: pNets for a Local HM composite

  (i) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_config(p,cmd) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) !Q_traceLvl(p,lvl) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p,G) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?New_traceLvl(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p) ?Recycle_config(p)

  fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_traceLvl_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !R_config_M1(fid) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G)

  code) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt) !Q_trace(hl_evt)!MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !MC(G) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_config_M1(fa,cmd) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl) !Q_traceLvl_M1(lvl)

Figure 22 :

 22 Figure 22: pNets for a Global HM composite

!

  Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_config(p,G,cmd) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl) !Q_traceLvl(p,G,lvl)

( 21 + 2

 212 * p) + l * (10 + p) basic pNets generated, and (7 + 2 * l + 2 * 2 l ) + (58 + 8 * p) + l * (26 + 4 * p)

S

  ( P, S, s 0 , L, → ) = {(s, φ)|s ∈ S ∧ φ ∈ Φ} S( P, L, pNet i∈I i , SV k∈K k) = { s i i∈Iφ | φ ∈ Φ ∧ ∀i ∈ Iφ. s i ∈ S(pNet i )} S(Queue(M )) = {(M j φ j ) j∈[1..n] |n ∈ N ∧ ∀j. (M j ∈ M ∧ φ j ∈ Φ)} labels are {αφ|α ∈ Sort(pNet) ∧ φ ∈ Φ};the initial state is the composition of initial states, S 0 (pN ets) where:S 0 ( P, S, s 0 , L, → ) = (s 0 , φ 0 ) S 0 ( P, L, pNet i∈I i , SV k∈K k ) = S 0 (pNet i ) i∈Iφ0 S 0 (Queue(M )) = [ ]and transitions are dened as the pNet , the smallest set of transitions verifying the rules below.Inria φ ∈ Φ k ∈ Kφ α j∈J j → α ∈ SV k ∀j ∈ Jφ. φ j ∈ Φ ∧ s j αj φj ---→ s ′ j ∈ pNet j ∀i ∈ Iφ \ Jφ. s ′ i = s i s i∈Iφ i αφ --→ s ′ i i∈Iφ ∈ P, L, pNet i∈I i , SV k∈K k φ ∈ Φ s α, e b , (xj:=ej ) j∈J -------------→ s ′ ∈→ iv(α)={x ′ i | i ∈ K} ∀i ∈ K. V i ∈ D φ ′ = φ + {x ′ i → V i |i ∈ K} e b φ ′ = True φ ′′ = {x j → e j φ ′ |j ∈ J} (s, φ) αφ ′ --→ (s ′ , φ ′ + φ ′′ ) ∈ P, S, s 0 , L, → n ∈ N ∀j ∈ [1..n + 1]. M j ∈ M ∧ φ j ∈ Φ (M j φ j ) j∈[1.

  Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(cmd) !Call_config(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(lvl) !Call_traveLvl(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_config(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(fid) !R_traceLvl(

  Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) !Call_config_S1(cmd) fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) !R_config_S1(fid) fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid) !R_trace_S2(fid)

Figure 24 :

 24 Figure 24: Bodies of the Local Manager (full) and GlobalHM (partial) components In Figure 24(left) we have the instantiation of the Body of a Local Manager component (the one inside the Local_HM composite). It only has two service methods cong and traceLvl, and no non functional interface.In Figure24(right) the Body LTS is more complex, because the Global HM has a total of 4 service methods on its two service interfaces S1 and S2, plus 2 outgoing methods on the multicast interface M1 and 2 on C1. In addition we have two specic loops dealing with the Bind/Unbind requests managing the group at interface M1.

  () ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p) ?New_config_C3(p)!Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) !Q_config_C3(p,cmd) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) ?GetValue_config_C3(p,val) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !Recycle_config_C3(p) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val) !R_config_S1(val)

Figure 25 :

 25 Figure 25: pLTS for the cong method of the Local Manager

Figure 26 :

 26 Figure 26: Attribute controller in the Local Monitor Attributes controllers, in Fractal and in GCM, are linked to non-functional interfaces providing an external get/set access to local variables of a component. In Figure 26 we see an example of such a controller, for the variable traceLvl of the Local Monitor, that can be controlled (set) by the Local Manager.

  If the qualied name is of the form CN.IN, then Get returns the external interface named IN of the inner component of name CN. Else, the qualied name is of the form This.IN; then the inner interface of the composite component is returned, it is the symmetric of the external interface of name IN.

  arg)

	Queue			Proxy m5[p5]
					P2.4
	P1.1			Proxy m4[p4]
	P1.2 Serve m*(f id * , arg)	GetProxy m*	New m5(p5) New m4(p4) P2.2	P2.6	GetValue m5(p5, val) GetValue m4(p4, val) P2.5
	P1.3	P2.1	!Recycle m5(p5) !Recycle m4(p4)
	P1.4				P2.3

val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val) ?R_m(val)

	Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m Proxy_m val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType val:resultType
	?R_m(

  ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m ProxyManager_m Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] Pool_Proxy:array[1..Max_Proxy] p:nat p:nat p:nat p:nat p:nat p:nat p:nat p:nat p:nat p:nat

	p:nat p:nat p:nat p:nat p:nat p:nat p:nat

Table 6 :

 6 Client synchronisation vectors for recongurable primitive components.

	The synchronised sub-pNets occur in the following order:
	Queue, Body, ServiceMethods, ProxyManagers, Proxies, BindingControllers

Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body Config Config Config Config Config Config Config Config Config Config Config Config Config Config Config Config Config TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config PM_config Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Queue Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body Body TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceEvt TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl TraceLvl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl AttrCtrl Business Business Business Business Business Business Business Business Business Business Business Business Business Business Business Business Business Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic Logic

	Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor Local Monitor
	Inria

  This appendix summarises the signatures of the functions computing the behavioural semantics in this paper Section 6 we gave the structure of the pNets hierarchy for the HyperManager example. Here we give some of the pLTS corresponding to this case-study. Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body

	Function F 1 BC MC service body proxyManager MethodLabels → pNet Signature Component → pNet Component → pNet Component → pNet Component → pNet MethodLabels× P(MSignature × pNet) → pNet Service methods(not specied here) Description basic behavioural semantics behavioural semantics for rst-class futures behavioural semantics for recongurable compo-nents behavioural semantics of components with mul-ticast interfaces P(MethodLabels)× P(MethodLabels) → pNet The body: serves requests in a FIFO order Manages future proxies overloaded for multicast interfaces proxy MethodLabels → pNet future proxy overloaded for composite components overloaded for multicast interfaces MethodLabels × GRef → pNet overloaded for rst-class futures FutDetect MethodLabels → pNet pLTS detecting a future received as request pa-rameter delegate MethodLabels → pNet Delegation method (in composite components) BC CItf → pNet Local_Manager.Body Local_Manager.Body Local_Manager.Body Local_Manager.Body binding controller C Examples of instantiated pLTS ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_config(fid,cmd) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl) ?Serve_traceLvl(fid,lvl)	page 18,24 32 35,36 41,43 20 22 38 22 25 38,42 31 31 25

In

  Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body Global_HM.Body . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt) ?Serve_trace_S2(fid,evt)
	?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd) ?Serve_config_S1(fid,cmd)

RR n°8167

Those interfaces are found thanks to the Get function: they are either interfaces of sub-components or internal interfaces of the composite component.

We chose constructors coherent with the term algebra we will use in this paper to simplify notations.Inria

j →i →a should be read j →(i →a) RR n°8167

Non-functional requests used in Section 5.2 are similar except that unbind_Itf has no parameter.Inria

The future references can be transferred between two service methods only if the component is stateful Inria

This work was partially funded by the ANR Blanc International project MCorePhP, and by the FUI project CloudForce

p,t:nat p,t:nat G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool G:array[1..Max_Group] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool Pool_Proxy:array[1..Max_Proxy] of bool ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m ?GetProxy_m

Code Code Code Code Code Code Code Code Code Code Code Code Code Code Code Code Code Local Monitor

?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait) ?WaitN_m(nbWait)

[ ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); ?R_m(i,val); The synchronised sub-pNets occur in the following order: Queue, Body, DelegationMethods, ProxyManagers, Proxies, Subcomponents

len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait] [len>=nbWait

Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor Global Monitor

GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl GrPM_M1_traceLvl

GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p] GrProxy_traceLvl[p]

!Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) !Q_setFilter(fi) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_config_M1(fa,cmd) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Q_traceLvl_M1(lvl) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i) ?Bind_M1(i)