Verifying the correct composition of distributed components: Formalisation and Tool

This article provides formal definitions characterizing well-formed composition of components in order to guarantee their safe deployment and execution. Our work focuses on the structural aspects of component composition; it puts together most of the concepts common to many component models, but never formalized as a whole. Our formalization characterizes correct component architectures made of functional and non-functional aspects, both structured as component assemblies. Interceptor chains can be used for a safe and controlled interaction between the two aspects. Our well-formed components guarantee a set of properties ensuring that the deployed component system has a correct architecture and can run safely. Finally, those definitions constitute the formal basis for our Eclipse-based environment for the development and specification of component-based applications.

Introduction
Designing safe distributed component-based software systems is a challenging task including a wide range of issues ranging from the safe composition of components to the applications performance and reliability. This work focuses on the correctness of component assembly which is a strong prerequisite for correct deployment and execution of components. We target component models which are hierarchical [13] and provide runtime control on the component application. In component-based software engineering, this last feature, i.e. the control and management of the system architecture and of the business application, is part of what is generally called non-functional concern. More precisely, non-functional aspects may cover many aspects, from security, latency, time aspects, energy or cost, to management concerns including mechanisms for dynamic reconfiguration, fault-tolerance, load balancing, self-healing, or more elaborate autonomic behaviours. In this paper, we are essentialy considering the second category, i.e. the management aspects, and we want to support the ability to design non-functional aspects themselves as a component system, which ensures a clear design of the whole application. The business logic of the application is called the functional aspect.
Our main goal is to provide a clear and formal definition of component assemblies and a set of logic predicates ensuring the correctness of component composition and component interconnection. In particular our predicates ensure a strong separation of concerns: a non-functional component can only interact with non-functional components, or with non-functional interfaces of business components. This way, each binding between components only transmits either functional or non-functional invocations. However a clean interaction between these concerns is highly desirable: we introduce interceptors, which are special components providing interaction between functional and non-functional elements. They can observe functional invocations and trigger a reaction of the control part of the component. In the other direction, non-functional components can influence the functional behavior by modifying its behaviour in two ways: either through reconfiguration, i.e. modification at runtime of the component architecture, or by changing parameters, i.e. component attributes, that will influence the functional behaviour.
In this paper we focus on one specific component model: the Grid Component Model (GCM) [4]. GCM allows the construction of distributed hierarchical applications with asynchronous group communications and strong separation between business logic and control parts of a system. To our knowledge, GCM is one of the only established component models that provides specific features for managing complex software systems, and that offers architectural artifacts and methodological approaches to organise the control part of such applications. GCM-based systems can be designed and modeled using the Ver-Cors tool 1 ; An XML-based Architecture Description Language (ADL) file, describing the architecture of the application, can then be generated by VerCors and used to build and deploy the GCM application, using the GCM/ProActive execution environment [5]. We started from the formal representation of GCM architecture given in [2] and introduced a number of important concepts. This article has the following new contributions: • First, we provide a formal representation of component architectures including a flexible set of constructs for the definition of non-functional part of an application which has never been formalized before. The business logic and control parts of a system are strongly separated. • Second, we formalize the notion of interceptors and define a number of auxiliary predicates insuring their safe composition with the rest of the system. • Third, we specify a set of key properties for component architecture, those properties are guaranteed for any component assembly that is well-formed according to the rules defined in Section 3.4. After validation of these rules, we garantee that the generated ADL code is correct, in the sense that building the component-based application by running the GCM component factory will terminate successfully with no runtime error. Additionally, the properties we exhibit are necessary prerequisite for the correct execution and the reconfigurability of the system; those properties include uniqueness of naming, separation of concerns, and communication determinacy. • Finally, we implement an environment allowing graphical modeling and validity check for the distributed systems architecture with respect to the proposed formalization.
The purpose of our formalization is threefold. First it is component model independent: by formalizing the correctness rules, we make them applicable outside the scope of GCM, and of our tools. Second, it makes it easier to re-use the formalization for different purposes, e.g. to implement different checkers, or encode it in a theorem prover. Finally, it allows reasoning on the properties ensured by the component model: properties of Section 3.5 can be formally proven from the definition of component correctness. This paper is organized as follows. Section 2 describes the Grid Component Model and our modeling platform. Section 3 presents the formalization of GCM architecture and of correct architecture. Section 4 describes how to adapt our formalism to other features or other component models and presents an overview of the related work. Section 5 describes our environment for modeling GCM-based systems. 7] component model; we summarize below the architectural aspects of GCM, and its main advantages. We also provide an illustrative example of a real-world application built using GCM.
A GCM component application is a composition of components, interfaces and bindings. GCM is a hierarchical component model, consequently there are two types of components in GCM: primitive and composite ones. Composite components are used to compose other components while the primitive ones are the leaves of the composition hierarchy. More precisely, a composite component (Application in Figure 1) is made of two parts: membrane (gray part) and content (white part). The content contains the sub-components dealing with the functional aspects. The membrane includes sub-components which are responsible for everything besides business logic: control, monitoring, structural reconfiguration, etc. A primitive component is similar except that the content is not known (e.g., Front-end, Repository and W1 in Figure 1). It encapsulates some business code. It has a list of methods, which it can execute.
The communication between components is performed in the form of method invocation. In Fractal and GCM interfaces are similar to object interfaces characterized by a set of methods that can transit through this interface. There are client and server interfaces. Client interfaces (e.g. C1) emit the methods invocations. Server interfaces (e.g. S1) receive them. We also distinguish the interfaces dealing with the business logic (functional interfaces drawn in blue color) and the ones dealing with the control of an application (non-functional ones colored in green). A binding is an arrow from a client to a server interface, communications between components follow those bindings.
In GCM, the interfaces can be attached to the components. An interface that is accessible from the exterior of a component is called an external interfaces (e.g. S1). When an interface is reachable from the inside of a component, i.e. from its content, it is called an internal interfaces (e.g. M1). The membrane of a component can also have internal interfaces, but they are not declared explicitly. The set of internal interfaces of a membrane is represented by the union of two other sets: all the external interfaces of the component containing the membrane and all the internal interfaces of the content inside the component. All the interfaces are taken with the same properties, but with an opposite role (e.g. a server interface becomes a client one and vice-verse). Figure 2 illustrates the (implicite) internal interfaces of a membrane, displayed in red color. Figure 1 shows an illustrative example taken from [5]. It represents the architecture of a real-world GCM system implementing an autonomic master-slave application treating incoming requests in parallel. Component Front-end is a front-end of the application. It receives the job-requests from the user. The requests are, then, processed by the workers (W1 and W2). The results are sent to the repository represented by a component Repository. The application reconfigures itself autonomically: the workers are added or removed depending on the system workload. This is realized by the sequence of components: Collector, Analyser, Planner, and Executor. This sequence follows the principle of the MAPE model for autonomic computing. The Monitoring components (Monitor, In Monitor) in the membranes of the workers and in Application monitor different metrics such as served requests per minute, and available disk space, CPU, and memory. Component Collector gathers the information from the Monitoring components. It sends the information to the component Analyser. Based on the received information, Analyser sends an alarm to the Planning component (Planner). The former one plans the reconfiguration, which is enacted by the Execution component (Executor).
GCM provides the following features to the applications: Strong separation of concerns The functional part of a GCM application can be separated from the control part thanks to the separation of a composite component into a membrane and a content and to the usage of functional and non-functional interfaces. In the provided example, the components performing the reconfiguration (Collector, Analyser, Planner, Executor) are separated from the ones responsible for the business logic (W1, W2, Repository). This separation ensures, as much as possible, the independence of the business code -the request treatment in the example -from the management code -the sequence of control components in the example. Reconfiguration In GCM, the architecture of the application can be accessed and modified at runtime; this is realized in the example by the execution component. It allows the non-functional concern to modify the structure of the functional (and the non-functional) part of the component application, and thus to change its behavior. Interceptors Sometimes, some information should be shared between the functional part and the controllers of the application. Interceptors are specific components inside the membrane that can intercept the flow of functional calls in order to trigger reaction from the non-functional aspects. For example, in the use-case, Monitor components are monitoring the number of job-requests sent to the worker, they illustrate very well what is an interceptor. In the membrane, functional interfaces are directly connected, however one or several interceptors can be inserted within such a binding and interact with other non-functional components (see the non-functional binding between Monitor and Collector in the example). One-to-many / many-to-one communications GCM also targets large-scale distributed systems where an invocation is to be broadcast to several entities or simply sent to different servers to ensure loadbalancing. For this, GCM introduces one-to-many client interfaces, called multicast interfaces like the interface M1 of Figure 1. From a structural point of view the particularity of multicast interfaces is that they can be connected to several server interfaces. Symmetrically, GCM introduce gathercast server interfaces for synchronizing many-to-one communications, typically waiting for a number of communications before triggering a communication. Our main contribution here is a formal definition and specification of the non-functional aspects of components; we will also see how we formally insure the separation of concerns and how we formally specify the interceptors.

VerCors
VerCors is a platform for the specification, analysis, verification, and validation of the GCM-based applications. The principle of the tool is illustrated in Figure 3. First, a user specifies the architecture of a GCM-based application, the signature of its interfaces, and the behavior of the primitive components using VerCors Component Editor (VCE). Then, from these descriptions the behavioral model of an application is generated (ADL2N) in a form of a dedicated behavioral semantic model: a parameterized networks of synchronized automata (pNets). This semantic model is transformed by abstraction functions (ABS*), until reaching a finite model suitable for model-checking. Finally, the resulting behavioral model is translated (N2F) into a set of languages used by a Model Checker (CADP tool [10]). Finally, the Model Checker verifies the correctness of the model with respect to a set of temporal logic properties (user requirements) and in the case of detected errors it provides their description. Once the requirements have been proven correct on the VCE specification, the user can generate the set of files (ADL for the Architecture Description, IDL for the Interface definition in the form of Java interfaces). Then naturally, user has to provide java classes implementing the service methods of the primitive components. These files are processed by the GCM component factory to build an executable application, that is executed with the GCM/ProActive execution environment.
In this paper we focus only on the structural aspect of GCM-based applications which is covered by the VerCors Component Editor. Our purpose is to ensure that the components provided to the rest of the tool chain are well-formed; for this we describe below a set of rules that must be satisfied to ensure the Element Formalization Server interface SItf ::= (Name, MSignature i∈I i , Nature) S

Client interface
CItf ::= (Name, MSignature i∈I i , Nature) C Interface Itf :  Using VerCors tool, we were able to design the architecture of the example illustrated at Figure 1, check its static semantic correctness properties, generate ADL files and deploy the corresponding application.

Formalization
The purpose of this section is to define formally well-formed components and exhibit their properties.

Structure
We start with the formal model representing the GCM architecture. First, we discuss the core elements. Second, we formalize the non-functional part of the GCM architecture.

Core
In this section we define the core elements of GCM, namely: Interfaces, Components and Bindings. Their formalization is given in Table 1. We denote A i∈I i a set of elements A i indexed in a set I. The formal definition is not provided for some elements of the table, because they are the terminal symbols. Such elements are presented in different font (e.g. Name, Type, NF).
Each server (SItf) or client (CItf) interface is characterized by three attributes: Name is the name of an interface; MSignatures represent the methods which can be served by a server interface or called by a client interface, with their signature; Nature defines if it is a functional or a non-functional interface.
Each component is characterized by its name, the sets of external client and server interfaces, and its membrane. A primitive component also includes a set of local methods. A composite component includes its content with a specific structure. The membrane is responsible for the non-functional activity. The content is defined by the sets of internal client and server interface, sub-components and a set of bindings located inside the content.

Function name Function Definition Sym
Sym : A binding connects two interfaces. It is described as a couple of names defining its source and target interfaces. Each name consists of two parts. The first part describes the container of the interface, either the name of a sub-component or the identifier This. The second part is the name of the interface itself.

Non-functional aspects
The Nature property of interfaces can be either functional (F) or non-functional (NF). The membrane is the part of a component which is responsible for the non-functional aspect of an application. Its formalization is given in the bottom of Table 1. The bindings (Binding l∈L l ) are the connections between the interfaces in the membrane. A membrane can contain a set of sub-components (Comp k∈K k ). The interceptors are recognized in this set essentially from their binding patterns, all the other components in a membrane are simple controllers.

Auxiliary functions
In this section we introduce the auxiliary functions used for the GCM architecture well-formness formalization. The auxiliary functions are given in Table 2.
First, we use auxiliary functions providing the access to the attributes of the interfaces and components. For example, the Nature(itf : Itf) function returns the nature of an interface, Binding(membr : Membr) returns the set of bindings in a membrane. The definitions of such functions are straightforward and we omit them in Table 2.
Second, the symmetry function (Sym) takes an interface as an input and returns an interface with exactly the same properties but with an opposite role: a client (. . .) C interface becomes a server (. . .) S one and symmetrically. to Third, we introduce a GetItf function. It takes a container (a component, a membrane or a content) as an input and computes the set of interfaces stored by it. If its argument is a component or a content, then its result is the union of its server and client interfaces sets. The case of membrane is more complicated as its internal interfaces are not explicitly defined. Instead, we compute the set of the symmetric of the interfaces belonging to the component containing the membrane and its content.
Finally, most of the consistency rules dealing with the bindings will use the auxiliary functions GetSrc and GetDst. They are able to retrieve the Interface objects which represent respectively the source and the destination ends of a binding. If GetSrc and GetDst functions are applied to a binding inside a membrane, then they may return an internal interface of the membrane.
Conversely, some rules use the Parent auxiliary function, that recovers the container (component, membrane or content) of an interface, a component, a content or a membrane.

Interceptors
In this section we define interceptors more precisely. First, we provide the non-formal definition of an interceptor. Then, we introduce a predicate recognizing the interceptors among the other sub-components of a membrane.
An interceptor is a functional component inside a membrane. It is connected to one external and one internal functional interfaces of the membrane's parent. An interceptor "intercepts" a functional call that goes from outside to inside of the membrane (input interceptor) or vice versa (output interceptors). The interceptors are used to monitor an application and its functional calls. The only functional activity of an interceptor should be to intercept and forward the functional calls through its functional client and server interfaces. All the other actions are performed through non-functional interfaces. To allow more modularity in the design, interceptors can be assembled in chains inside the membrane. Interceptors in a chain must all be either input or all output; we shall speak of input chains and output chains.
In principle, it would be possible to relax this definition, and allow for more general interceptor structures, e.g. including some parallelism in the form of multicast client interface in the "chain", allowing more efficient processing. However it is not clear whether this would be useful fo rreal applications, and this not implemeted in the GCM/ProActive middleware, so we prefer to keep the (relatively) simpler form in the formal definition.
In order to distinguish formally the interceptors from the other components, we define a predicate IsInterc. It is given in Table3. It takes a component and a membrane as an input and returns true if the component belongs to a chain of interceptors inside the given membrane. An interceptor chain consist of one or several interceptors. IsInterc uses a predicate IsIntercChain which identifies if a given sequence of K components is a chain of pipelined interceptors inside the given membrane. IsIntercChain predicate checks the following features of the indexed set of components given as input: • all the components are nested inside the membrane; • all the components have exactly one functional server and one functional client interface; Predicate IsIntercChain uses two auxiliary functions: GetSItf F (comp) (resp. GetCItf F (comp)) returns the sets of all functional server (resp. client) interfaces of component comp.
The predicate IsExtEnd checks, for an input interceptor chain, whether the first interceptor in the chain is connected to a server functional interface of the parent component or, for output interceptors, whether the last one is connected to a client functional interface of the parent component. Predicate (IsExtEnd(I 0 , b 0 , SI 1 , membr, I 0 ) ∧ IsIntEnd(CI k , b K , I K , membr, I K )) ∨(IsIntEnd(I 0 , b 0 , SI 1 , membr, I 0 ) ∧ IsExtEnd(CI k , b K , I K , membr, I K )) IsExtEnd IsExtEnd (

3: Interceptor Predicates
IsIntEnd is the symmetric, it checks connection with the content. However, the content is not known for a primitive component; in that case the interfaces of the content are computed by symmetry of the external (functional) interfaces of the component.

Well-formed components
In this section we define the well-formness rules for GCM components. First, we introduce the core rules and predicates used for the definition of well-formness. Then, we focus on the non-functional aspects. Table 4 formalizes the auxiliary predicates which are used for the definition of the following constraints:

Core
• Components naming constraint (UniqueCompNames): all the components at the same level of hierarchy must have different names. This restriction is due the fact that components are referenced by their name; typically, QName can be of the form CName.Name; and if two components had the same name the functions GetSrc and GetDst would not return a single deterministic result. The two contents of two different composite components as well as two membranes are considered to be different name-spaces. A membrane and a content are also different name-spaces even if they belong to the same component.  • Role constraint (BindingRoles): a binding must go from a client interface to a server interface. The predicate uses a function Role(I) that returns C (resp. S) if I is a client (resp. server) interface. • Typing constraint (BindingTypes): a binding must bind interfaces of compatible types. The compatibility of interfaces means that for each method of a client interface there must exist an adequate corresponding method in the server interface. In other words, if a client interfaces is connected to a server interface and it wants to call some method, then this method must actually exist on the server interface. In general, a corresponding method does not need to have exactly the same signature as the one required, but can use any sub-typing or inheritance pre-order available in the modeling language. We denote ≤ such an order between interface signatures. • Cardinality constraint, CardValidity, ensures that a client interface is bound to a single server one.
We use the previous constraints to define a well-formness predicate, denoted W F. It is defined recursively on component architecture, namely on primitive components, on composite components, and on contents.
A GCM primitive component is well-formed if all its interfaces have distinct names and its membrane is well-formed.
A GCM composite component is well-formed if all its external interfaces have distinct names, its content and its membrane are well-formed.
Let compos : Compos = CName < SItf i∈I i , CItf j∈J j , Membr, Cont >; (2) The content of a GCM component is well-formed if all its interfaces have distinct names, all its subcomponents have distinct names, all its nested bindings ensure valid cardinality, all its sub-components are well-formed, the role, type and nature constraints are respected for all its sub-bindings. The nature constraint for the bindings relies on The BindingNature predicates. It is discussed in Section 3.4.2 Predicate name Predicate Definition UniqueNamesAndRoles UniqueNamesAndRoles(Itf i∈I i : set of Itf) ⇔ ∀i, i ∈ I.(i = i ∧ Name(Itf i ) = Name(Itf i )) ⇒ Role(Itf i ) = Role(Itf i ) BindingNature BindingNature(b : Binding) ⇔ CL(GetSrc(b, Parent(b))) = CL(GetDst(b, Parent(b))) = 1∨ (CL (GetSrc(b, Parent(b))) > 1 ∧ CL (GetDst(b, Parent(b))) > 1) The well-formness of a membrane is only significant for the non-functional aspect, it is defined below.

Non-functional aspects
In this section we define the static semantics constraints ensuring safe composition of the non-functional part of a GCM-based application. Correctness of a membrane relies on the two predicates defined in Table 5: • Interfaces naming constraint (UniqueNamesAndRoles): if there are two interfaces with the same names in a membrane, then they must have different roles. This is as slight relaxation from the UniqueItfNames rule of the general case: we want to allow corresponding external/internal interfaces pairs of opposite role to have the same name. This also ensure compatibility with the original Fractal model, where internal interfaces were implicitly defined as the symmetric of external ones. • Binding nature constraint(BindingNature) is a rule imposing the separation of concerns between functional and non-functional aspects. We want the functional interfaces to be bound together (only functional requests will be going through these), and non-functional interfaces to be connected together as a separate aspect. This is simple to impose in the content of composite components, but a little more tricky in the membrane because of the specific status of interceptors.
The solution is to qualify as functional all the components in a content and all the interceptors, while all other components in the membrane are non-functional. Then the interfaces are declared functional or non-functional. From this we compute for each interface a control level ranging from 1 to 3, where 1 means functional; 2 and 3 mean non-functional. Then the compatible interfaces are either both "1", or both greater than "1". The ControlLevel function is formally defined as: This constraint on the nature of bindings was already mentioned in [15], we propose here a formal definition that is simpler and more intuitive.
As the last step, we define the well-formness predicate for membranes. A membrane is well-formed if all its sub-components have distinct names, the naming constraint is respected for its interfaces, all its sub-components are well-formed, all its bindings ensure a valid cardinality, and the role, type, nature constraints are respected for all its sub-bindings, Let membr : Membr =< Comp k∈K k , Binding l∈L l >; This section presented an extension to the definition of well-formed components defined in previous works [12,11]. More precisely, most of the definitions given in this section allow us to formalize the notion of well-formed non-functional features and well-formed interceptors, that have never been formalized before. The new definition of well-formed components is the basis for the correct composition of distributed components with clear separation of concerns.

Properties
The well-formed definition of the preceding section guarantees that, from an architectural point of view, the specified component assembly behaves well, both at deployment time and during execution. More precisely, the constraints specified above ensure the following properties: Component encapsulation Bindings do not cross boundaries. Indeed, GetSrc and GetDst predicates are only defined in the context of the parent component, for example, the call to GetDst and GetSrc inside the definition of the BindingRoles predicate ensure that both bound interfaces are either internal interfaces of the parent component or external interfaces of its sub-components, which guarantees that no binding crosses component boundaries.

Deterministic communications
The CardValidity predicate guarantees that each client interface is bound to a single server interface, which guarantees that each communication between components is targeted at a single, well-defined, destination. Section 4.1 will introduce mutlticast interfaces to express communications with multiple destinations. 3) Bindings only connect together functional (resp. nonfunctional) interfaces. 4) We clearly identify interceptor components that are the only structural exception to these rules: an interceptor is a component in the membrane that can have a single functional client and a single functional server interface, but as many non-functional interfaces as necessary. In order to guarantee that the generated ADL deploys correctly, i.e. without runtime error, it is sufficient to ensure that (1) each interface and class the ADL file refers to exists (which is ensured by the generation process), that (2) no binding exception will be raised at instantiation time (which is ensured by the well-formedness property and in particular by the determinacy of communications), and that (3) each mandatory interface is bound and thus the component system can be started without error (which is again ensured by the well-formedness property dealing with bindings); finally (4) the unique names ensure that the components and interfaces can be manipulated adequately during instantiation. All those arguments ensure that each ADL file generated by our platform deploys correctly, provided the wellformed property is verified by the system.
The properties verified by well-formed components not only guarantee that the ADL generated from a well-formed specification deploys correctly, but also ensure some crucial properties concerning the runtime semantics (deterministic communications, separation of concerns, reconfigurability ...).

Extension and Related Work
While Section 3 focused on the core concepts of a component model with componentized membranes, we illustrate in this section how our framework can be used to model other features of GCM or of other component models. We also compare our approach with related works.

Collective communications
One of the crucial features of GCM is to enable one-to-many and many-to-one communications through specific interfaces, namely gathercast and multicast.
In order to specify such communications let us add a Cardinality (Card) field in the specification of the GCM interfaces. The cardinality can be singleton, multicast or gathercast. For example, interface M1 at Figure 1 is multicast: it sends requests to several workers at the same time. G1 is gathercast: it can receive requests from several workers. S1 and C1 are singleton interfaces.
These new interfaces modify the definition of cardinality validity. In particular, the multicast interface allows two bindings to originate from the same client interface. The CardValidity is modified as follows: The intended semantics is that any invocation emitted by a multicast interface is sent to all the server interfaces bound to it. Gathercast interface on the contrary synchronizes several invocations arriving at the same server interface, they do not entail any structural constraint. An interceptor chain should not contain any multicast functional interface because it should transmit invocations in a one-to-one manner.

Other component models
Our work is placed in the context of GCM component model but it can also be used to model the characteristics of most component models, we review some of them in this paragraph. First, concerning the functional parts of components, a lot of component models have a structure similar to GCM components, like, e.g., SCA [1] or Fractal [7]. Our framework can be used to formally define architectural correctness for these component models. Additionally, several frameworks offer different notion of componentized component control, we focus on these aspects below.
SOFA 2.0 [9] features hierarchical composition and componentized component control. Interestingly, similarly to our approach, one of the objectives of SOFA is also to provide formal verification tools for distributed component systems. It is easy to adapt our formal specification to SOFA 2.0, more precisely: Micro-controllers are components dedicated to non-functional concerns, they reside in the membrane and are not hierarchical: to take them into account, we should restrict the correctness rules for the membrane to only allow primitive components in the membrane. The other aspects of SOFA are not different from the model used in this paper. In particular, delegation chains are chains of interceptors, following exactly the rules defined in Section 3.3.
AOKell [16] is an extension of Fractal specifically for componentizing membranes, it is interesting to note that the authors define a notion of control level, which is quite similar to the ControlLevel function used in our paper. In this case again, our approach could be used to verify the correct composition of AOKell-based components, and ensure the safe design of AOKell component systems.
In a similar way, Dynaco [8] could also benefit from our approach, it is a component model targeting dynamic adaptation and allowing full-fledged components in component's membranes.

Related Approaches
In a slightly different application domain, BIP [6,3] is a formal framework that allows building and analyzing complex component-based systems, both synchronous (reactive) or asynchronous (distributed) by coordinating the behaviour of a set of primitive and heterogeneous components. BIP is supported by a tool set including translators from various programming languages as Lustre and C into BIP, a compiler for generating code executable by a dedicated engine, and the verification tool dFinder.
Concerning the formalization of component structure, the two closest previous works are the formalization of Fractal in Alloy [14], and the formalization of GCM in Isabelle/HOL [12]. The first framework focuses on structural aspects in order to prove the realisability of component systems, while the second aims at providing lemmas and theorems to reason on component models at a meta-level, and prove generic properties of the component model. None of those formalizations included the notion of non-functional components, many-to-many interfaces, or interceptors. The formal specification of component correctness defined in this paper could be used to extend the expressiveness of the component model in the Alloy and the Isabelle frameworks. Also the strength of the present work is that it is directly implemented in the VCE environment in order to provide tools accessible for the programmer. The tools presented here ensure, in a graphical environment, that the component systems composed by the programmer are well-formed.
From another point of view, in [11] we investigated a language for generating correct-by-construction component systems, and reconfiguring them safely. Similarly to the cases above, this language does not deal with the structure of the membrane and one-to-many/many-to-one communications, it should be extended to the enhanced component structure presented here.

Implementation: the VCE modeling environment
The presented formal model and formal constraints were implemented in a tool called VerCors Component Editor (VCE v.3) which is the graphical specification part of the VerCors project. VCE v.3 combines a set of semantics models and graphical diagram editors, the tools for graphical and textual export of models and a set of additional wizards. Using VCE v.3 one can design the architecture of a componentS-based system, validate its structure according to the rules specified in this paper and export its representation, either as an ADL (XML) file, that will be used in the execution environment, or as a semantic representation, for model-checking. We briefly discuss below the basic features of the tool.  Figure 4 is a screen-shot of GCM Components diagram editor. It has a standard interface of an Eclipse-based application.
The static semantics constraints, defined in the previous sections are encoded in VCE v.3 in order to validate component assemblies. The Acceleo language 4 is used for the definition of such rules. An example of a rule defining the naming constraint for the components is given below: [not self.siblings(Component)->collect(name)->includes(self.name)/] This rule will be applied to each component. Here, self is the component on which the constraint is validated; let us denote it C. The function siblings(Component) returns the set of all the components in the same container as C. The function collect(name) extracts the names of all such components. Finally, includes(self.name) checks if there is any component with the same name as C and returns true if it finds one.
VCE v.3 editor reports about the constraint violations. The elements of the architecture which are not correct are marked with red signs. The description of an error is given in a standard Eclipse Problem panel. Figure 4 illustrates an example of the architecture validation result; the architecture contains only one error: there is a binding between two interfaces with incompatible types (C1 and S1).
To conclude, based on the formal definitions given in this paper, we implemented an environment for the specification of the component-based applications involving group communications and with strong separation of functional and non-functional concerns. The validation of designed models ensures the correctness of the components assemblies. From this specification VerCors environment allows the verification of the behavioural properties of the system, and the generation of executable code that is safe by construction and can be run using the GCM/ProActive library.

Conclusion and Future Work
This article presented the formalization of rich component models with strong separation of functional and non-functional concerns, including the definition of interceptors. It also presented a tool implementing the formalized model. The main contributions of the article are: • the formal definition of GCM components including non-functional aspect and interceptors; • the formal definition of well-formness predicates including special rules for non-functional aspects, binding compatibility, and interceptors; special care has been put on the separation of concerns: the notion of control level was introduced and formally defined for the interfaces and components; • implementation of a tool for GCM-based systems architecture graphical modeling and their static semantics validation. • the identification of basic and crucial properties of the component assemblies which are guaranteed by our rules, and by the VCE platform. In particular, when a GCM application specification has been checked valid in VCE, the generated ADL file is guaranteed correct by construction, and the corresponding components will be built and deployed correctly (with no execution error) by the middleware component factory.
One of the key challenges addressed by this paper is the clear representation of interceptors chains and especially the formalization of predicates which recognize them among the other components inside a membrane.
Our approach is general enough to be extensible in order to take into account many-to-many communications or other component models.
However, the VerCors platform is not completely implemented yet. We are now working on the representation and validation of GCM-based systems behavior using UML State Machines for the definition of primitive components behavior in VCE v.3. This functionality is already partially specified and implemented. The state-machine and architecture models will be used to generate a finite semantic representation, suitable as the input to verification tools. The structural wellformess rules from this paper will have to be complemented by others, ensuring the coherency between the structural and behavioural models.


extfieldsofstudy:
Computer Science
Physics

text:
Results from the Wide-field Infrared Survey Explorer (WISE) Future Uses Session at the WISE at 5 Meeting

During the"WISE at 5: Legacy and Prospects"conference in Pasadena, CA -- which ran from February 10 - 12, 2015 -- attendees were invited to engage in an interactive session exploring the future uses of the Wide-field Infrared Survey Explorer (WISE) data. The 65 participants -- many of whom are extensive users of the data -- brainstormed the top questions still to be answered by the mission, as well as the complementary current and future datasets and additional processing of WISE/NEOWISE data that would aid in addressing these most important scientific questions. The results were mainly bifurcated between topics related to extragalactic studies (e.g. AGN, QSOs) and substellar mass objects. In summary, participants found that complementing WISE/NEOWISE data with cross-correlated multiwavelength surveys (e.g. SDSS, Pan-STARRS, LSST, Gaia, Euclid, etc.) would be highly beneficial for all future mission goals. Moreover, developing or implementing machine-learning tools to comb through and understand cross-correlated data was often mentioned for future uses. Finally, attendees agreed that additional processing of the data such as co-adding WISE and NEOWISE and extracting a multi-epoch photometric database and parallax and proper motion catalog would greatly improve the scientific results of the most important projects identified. In that respect, a project such as MaxWISE which would execute the most important additional processing and extraction as well as make the data and catalogs easily accessible via a public portal was deemed extremely important.

INTRODUCTION
NASA's Wide-field Infrared Survey Explorer (WISE) 1 was launched into orbit five years ago, and surveyed the entire mid-infrared sky in 2010. The satellite resumed surveying as NEOWISE 2 in December 2013, and is now on its fifth pass over the sky. Over 1,200 refereed papers based on the data have now been published 3 , with results ranging from the discovery of the first Earth Trojan asteroid, to challenging the standard paradigm for quasar unification. To celebrate what has been done with WISE, what is being done with NEO-WISE, and what will be done in the future, the "WISE at 5: Legacy and Prospects" conference 4 was held Feb. 10 -12, 2015, on the campus of Caltech in Pasadena, CA.
During the meeting, a new type of session was introduced to encourage broad engagment among meeting participants. In general, scientific meetings offer standard opportunities to interact with fellow attendees. Typically these happen formally during poster sessions, post-talk question and answer time, or panels. Informally these happen at coffee breaks, lunches, or dinners where attendees are able to isolate key people to engage with individually. However it is often difficult to generate discussions that engage all participants, especially junior attendees who may be intimidated by speaking up during sessions or are shy in informal situations. Recent meetings have been inserting interactive sessions to try and encourage more informal engagement among a larger and broader range of participants (e.g. at the "Exoplanets and Brown Dwarfs: Mind the Gap" meeting held in Hertfordshire, UK and at the "Gaia and the Unseen: the Brown Dwarf Question" meeting held in Torino, Italy). The second day of the "WISE at 5" meeting was centered around the topic "future uses of WISE/ NEOWISE data." This type of forward-thinking session, which lacks traditional results or data to present, naturally lends itself to a group discussion. Hence, 90 minutes were dedicated to discussing and brainstorming future uses of WISE/NEOWISE mission data in small, rotating groups. In this paper, we report the results of this interesting session where conference attendees assessed the most important questions that WISE/NEOWISE could still answer as well as the current and future data and tools that would help address these topics. We were par- ticularly interested in assessing what additional processing of WISE/NEOWISE data might contribute to the important scientific questions that the mission would be engaged in during the coming years. In section 2 we describe the procedure followed for setting up and executing the interactive session. In section 3 we summarize the results broken down by each of the four brainstorming questions. In section 4 we present conclusions.

PROCEDURE
The plan for the interactive session was to break attendees into small groups and have them brain-storm answers to questions regarding the future uses of the WISE/NEOWISE data (see Figures  1 -2). There were ∼120 attendees at the meeting from North and South America, Europe, Asia, and Africa. A large number of North American attendees were local to southern California and therefore the actual number of people present for any given session on any given day varied. Not all conference attendees participated in the interactive session as it was held in a different venue. In all there were ∼65 participants in the interactive session.
Prior to the meeting, attendees were randomly pre-assigned into 12 groups of up to 10 people 5 . One moderator for each table was contacted ahead of time and asked to remain at a pre-assigned table, help guide the conversation and take notes while other participants rotated. The session was held in a single, large room with enough tables and chairs to hold all attendees. Large easel-sized paper and markers were placed at each table so moderators could record group answers to each discussion question. Before the meeting, the scientific organizing committee developed four questions aimed at engaging attendees on the future uses of WISE and NEOWISE data. Each question built upon the previous. In total, there were 90 minutes dedicated to the session or roughly 20 minutes for each question. Groups began at one table to answer the first question but then rotated in a pre-assigned manner (labeled on their conference badges) to three subsequent new groups. In so doing, attendees engaged with four random groupings of participants. The questions proceeded in the following order: 1) What five major science questions can WISE or NEOWISE data still answer? Participants were given 20 minutes to introduce themselves to their fellow tablemates and brainstorm.
At the end of the time, attendees were rotated to a second pre-assigned table and asked to brainstorm the follow-up question: 2) What are the most important existing data and tools to help answer these questions? Participants were at a new table, and therefore were answering question 2 in regards to what a previous group had brainstormed. By having one group work off of what the previous group produced, the conference indirectly engaged at a large level. After another 20 minutes, attendees rotated to a third table with an entirely new pre-assigned group and brainstormed a third question: 3) What are the most important future data and tools to help answer these questions? After another twenty minutes of brainstorming on the answers provided by group 1 and 2 at a given table, the attendees rotated one final time to answer a fourth question: 4) 6 How would additional processing of WISE and NEOWISE data help answer these questions? In this manner the output of any one table was the product of four rotations or dozens of attendees brainstorming. Moderators were anchors at each table and did not rotate but rather helped guide 6 We acknowledge that Q3 and Q4 are somewhat degenerate, but we considered the question about upcoming WISE/NEOWISE data products to be important enough to require a separate answer. discussions. To ensure that we were able to collate the results from the attendees, we asked the moderators to take careful notes during the session. Furthermore, since the point was to rotate participants through different tables, it was important to ensure that the work of a previous rotation was clearly visible. Hence each table was given a giant easel-sized paper and the responses to each question were boldly displayed. Post session, moderators were asked to summarize the results of their table using an online document. We then collated the responses and asked the moderators to comment in more detail (as described in the summary below).

SUMMARY
Many attendees of the "WISE at 5" conference were extensive users of the dataset and the results reported here will reflect the scientific interests of the participants. However, the expertise of attendees spanned a range of topics -from solar system objects to quasars (see Figure 3 for a distribution of the scientific interests of the attendees). Therefore, individual bias should be minimized 7 . Participants in the interactive session were asked to think both within and beyond their own field and they were encouraged to think outside the box.
3.1. What five major science questions can WISE or NEOWISE data still answer?
The first brainstorming session was the setup for all subsequent interactions. Participants were asked to work with their first assigned table and come up with five major science questions that WISE or NEOWISE could still answer. We allowed 20 minutes for group discussions. The outcome was 64 WISE-relevant science questions that were submitted across 12 tables (two tables submitted six questions and one table submitted seven). See Figure 4 for a word cloud of all the responses. These questions spanned a range of scientific topics and reflected the expertise and forward thinking of the attendees. The questions brainstormed ranged from broad (e.g. Where and why do stars form? and How do galaxies and clusters form and evolve over cosmic time?) to specific (e.g. Study the integrated Sachs-Wolfe effect in the local Universe, and Study the structure of magnetic fields in the interstellar medium). We also asked the attendees to consider "outside the box" ideas and several responses fell into that category (e.g. Characterize the South Atlantic Anomaly, and Characterize geostationary satellites).
We found the majority of answers were bifurcated between two themes: (1) brown dwarf questions, and (2) active galactic nuclei (AGN) or quasar questions. There were six WISE-relevant science questions repeated more than once across the 12 tables. We list each of these along with the number of times that they appeared in parentheses below: (1) Determine the initial mass function (IMF) in the substellar regime (x6) (2) Identify obscured AGN and test AGN unification (x5) (3) Discover new quasars (x3) (4) Discover or constrain unknown populations (x3) (5) Characterize high redshift quasars (x2) (6) Find Planet X (x2) To summarize the 43 remaining results, we grouped the questions by common scientific theme. The following were recurring topics that appeared at least two times: (1) Exploring populations of brown dwarfs (x6) (2) Galactic structure (x5) (3) Star formation (x4) (4) Large scale structure (x3) (5) Zodiacal dust (x2) (6) Asteroid populations (x2) (7) Man-made satellites (x2) (8) Dust extinction maps and the cosmic microwave background (x2) For those interested, we have made the full list of WISE-relevant science questions available to view in a shared Google document 8 .

What are the most important existing
data and tools to help answer these questions?
The second brainstorming session was focused on evaluating what current instrumentation, facilities and/or tools would help address the scientific questions enumerated in the first session (see Figure 5 for a word cloud of the discussions). In the moderators' summary of each table's response, we asked them to generalize if (1) the follow-up data already existed (e.g. all-sky photometric surveys) or (2) if one needed to apply for the time. In the case of the latter, we also evaluated whether or not this follow-up could be obtained by small proposals (i.e. individuals could spearhead the work) or if it required a large collaborative follow-up (i.e. something the community would need to ask for).
In general, many of the scientific questions cited cross-correlating WISE data with other all-sky or large-area surveys such as SDSS 9 (x7), 2MASS (x4), UKIDDS (x4), and VHS (x3) as well as those conducted by Spitzer and Herschel as significant for follow-up. In that respect many groups converged on the idea that multi-wavelength photometric approaches (using the above surveys as well as ROSAT-x3, Fermi-x2, Swift-x2, GALEX-x2) would help with the most important science questions. Co-adding the current WISE data and extracting parallaxes, time-variations, and proper motions was also cited although this is discussed in greater detail in section 3.4.
The major follow-up using current data that requires a community effort to execute was in regard to spectroscopic follow-up. This was noted for several of the scientific goals that varied in theme including: (1) investigating the initial mass function into the substellar regime, (2) exploring AGN unification, and (3) establishing the large-scale structure map of the Universe over the entire sky.
A few current tools of note that would aid in addressing the scientific topics were (1) the IRSA finder chart tool, (2) the WISE image server, and (3) the SQL interface for AllWISE. Also noted as critical for achieving many of the scientific goals was an implementation of machine-learning algorithms. This was of note for both current and future uses as teams were not sure whether these were tools that needed to be developed or if they already existed.

What are the most important future
data and tools to help answer these questions?
The third brainstorming session was focused on evaluating what future instrumentation, facilities and/or tools would help address the scientific questions enumerated in the first session (see Figure 6 for a word cloud of the discussions). As with brainstorming session #2, we asked the moderators to summarize by reflecting on whether or not the future follow-up could be done with small pro-posals (i.e. individuals could spearhead the work) or if it would require a large collaborative followup (i.e. something the community would need to ask for).
Several upcoming facilities were overwhelmingly present among the desired follow-up for addressing the scientific questions. Those included spectroscopic follow-up using the James Webb Space Telescope (JWST) as well as the Wide-Field InfraRed Survey Telescope (WFIRST-AFTA) and a cross-correlation with the data from the Large Synoptic Survey Telescope (LSST) as well as Gaia and Euclid. As was described in the session #2 summary, many groups stated that complementing the WISE data with multiwavelength photometric surveys (including VHS, and TESS in addition to those listed above) would be beneficial for the most important scientific questions.
In regards to whether small proposals or a community effort would be required, there was a similar response as to that detailed in the summary of session #2. Small proposals on major future instrumentation were highly regarded although several projects, such as an all-sky spectroscopic survey to determine high redshift sources, were also cited.
As multiwavelength astronomy and crosscatalog searching was very high on the list of responses, several groups noted that tools to facilitate large-scale catalog matching across a broad list of surveys would augment the science results moving forward. Moreover, developing and implementing machine-learning tools to explore and understand the data were often mentioned.
3.4. How would additional processing of WISE and NEOWISE data help answer these questions?
For the fourth and final brainstorming session, we asked participants to comment on how additional processing of WISE and NEOWISE data would help answer the questions enumerated in session #1. Across brainstorming sessions #2 and #3, we found that the co-adding of WISE/NEOWISE data as well as source extractions for motion, parallax, and variability searches were cited multiple times as both a current and future tool for addressing the science questions. Hence, without even asking this follow-up question, we had an overwhelming consensus that additional processing of WISE and NEOWISE data would aid in answering the most important questions possible with the mission.
In the moderators' summary of this session, we asked for (1) a description of how the additional processing would impact the scientific project as well as (2) specifics on the type of processing discussed at each table. Furthermore, moderators were asked to report whether the additional processing would require some large funding source (e.g. MaxWISE 10 ) or whether individual ADAP grants could cover it.
To summarize, the additional processing most often recommended was co-adding the WISE and NEOWISE data to facilitate the discovery of fainter objects (e.g. QSOs, AGN, Y-type brown dwarfs, galaxy clusters). Moreover, the creation of a complete and detailed Multi-epoch Photometry Database (MEP), as well as a proper motion and parallax catalog, dominated the needs of many science programs (e.g. identifying unknown populations of brown dwarfs, finding RR Lyrae variables to determine the distance to and structure of tidal streams). Also of note were (1) better background subtraction which would help with both Galactic and extragalactic projects (e.g. the detection of low surface brightness light from ejected stars, detection of diffuse emission in stars and dust to map the Milky Way in 3D), and (2) an improved PSF model which would help with the numerous astrometric and variability studies.
As to the question of whether this additional processing would require a large funding source or whether individual ADAP grants could cover it, there was a diversity in responses. MaxWISE, the proposed co-adding of WISE data and catalog extraction, was cited as important for numerous questions. This type of activity would enable the main additional processing points that were cited by attendees as critical for addressing the most important science questions possible with the WISE mission. In the summaries, the moderators noted that portions of the additional processing, such as co-adding parts of the sky of interest or extracting only certain regions, were certainly plausible with something like an ADAP grant. However, what seems clear from this session is that a concerted effort to uniformly co-add the data and extract sources is the optimal product for addressing the most important science questions that WISE/NEOWISE can still answer. Importantly, 10 See poster by P. Eisenhardt from the "WISE at 5" meeting http://wise5.ipac.caltech.edu/posters/Eisenhardt.pdf many noted that a project like MaxWISE was required to both execute the additional processing and extraction AND make the end result accesible to the community.

CONCLUSIONS
The "WISE at 5" meeting brought together experts and super-users of the dataset. As such, it was an excellent opportunity to identify the major scientific questions that could be answered by WISE/NEOWISE in the coming years as well as the complementary datasets, tools, or additional processing that would aid in addressing these topics. Overall, the results showed several recurring topics bifurcated between extragalactic and brown dwarf science. Likely this is a reflection of the scientific preference of the attendees.
Among the 12 separate tables asked to brainstorm five important (or potentially out of the box) questions that WISE could answer in the coming years, several questions came up repeatedly, including: (1) Determine the initial mass function (IMF) in the substellar regime; (2) Identify obscured AGN and test unification; (3) Characterize high-redshift quasars; and (4) Find Planet X. Many of the scientific questions will be complemented by a cross-correlation with other photometric surveys (e.g. SDSS, Pan-STARRS, LSST, Gaia, Euclid, etc.) and would benefit from the development or implementation of machine-learning algorithms to aid in the studies.
Finally, it was largely agreed by attendees that additional processing of WISE data would greatly benefit all future studies. Co-adding WISE with NEOWISE data, extracting a multi-epoch photometric database as well as a proper motion and parallax catalog that would be easily accessible in a public portal was among the top cited additional processing techniques. While small grants (e.g. ADAP) would enable some of the work, a community-backed project such as MaxWISE was mentioned numerous times and would greatly improve our ability to address the most important scientific topics cited by conference participants.


extfieldsofstudy:
Computer Science
Mathematics

text:
Optimality of Poisson processes intensity learning with Gaussian processes

In this paper we provide theoretical support for the so-called"Sigmoidal Gaussian Cox Process"approach to learning the intensity of an inhomogeneous Poisson process on a $d$-dimensional domain. This method was proposed by Adams, Murray and MacKay (ICML, 2009), who developed a tractable computational approach and showed in simulation and real data experiments that it can work quite satisfactorily. The results presented in the present paper provide theoretical underpinning of the method. In particular, we show how to tune the priors on the hyper parameters of the model in order for the procedure to automatically adapt to the degree of smoothness of the unknown intensity and to achieve optimal convergence rates.

Introduction
Inhomogeneous Poisson processes are widely used models for count and point data in a variety of applied areas. A typical task in applications is to learn the underlying intensity of a Poisson process from a realised point pattern.
In this paper we consider nonparametric Bayesian approaches to this problem. These do not assume a specific parametric form of the intensity function and produce posterior distributions which do not only give an estimate of the intensity, e.g. through the posterior mean or mode, but also give a measure of the remaining uncertainty through the spread of the posterior.
Several papers have explored nonparametric Bayesian approaches in this setting. An early reference is Møller et al. (1998), who study log-Gaussian priors. Gugushvili and Spreij (2013) recently considered Gaussian processes combined with different, non-smooth link functions. Kernel mixtures priors are considered in Kottas and Sansó (2007). Spline-based priors are used in DiMatteo et al. (2001) and Belitser et al. (2013).
The present study is motivated by a method that is not covered by earlier theoretical papers, namely the method of Adams et al. (2009). These authors presented the first approach that is also computationally fully nonparametric in the sense that it does not involve potentially inaccurate finitedimensional approximations. The method involves a prior on the intensity that is a random multiple of a transformed Gaussian process (GP). Both the hyper parameters of the GP and the multiplicative constant are endowed with priors as well, resulting in a hierarchical Bayes procedure (details in Section 2.3). Simulation experiments and real data examples in Adams et al. (2009) show that the method can give very satisfactory results.
The aim of this paper is to advance the theoretical understanding of the method of Adams et al. (2009), which they termed "Sigmoidal Gaussian Cox Process" (SGCP). It is by now well known both from theory and practice that nonparametric Bayesian methods need to be tuned very carefully to produce good results. An unfortunate choice of the prior or incorrectly tuned hyper parameters can easily result in procedures that give misleading results or that make sub-optimal use of the information in the training data. See for instance the by now classical reference Diaconis and Freedman (1986), or the more recent paper van der Vaart and van Zanten (2011) and the references therein.
A challenge in this problem (and in nonparametric function learning in general) is to devise a procedure that avoids overfitting and underfitting. The difficulty is that the appropriate degree of "smoothing" depends on the (unknown) regularity of the intensity function that produces the data. Indeed, intuitively it is clear that if the function is very smooth then to learn the intensity at a certain location we can borrow more information from neighborrowing points than if it is very rough. Ideally we want to have a procedure that automatically uses the appropriate degree of smoothing, i.e. that adapts to regularity.
To address this issue theoretically it is common to take an asymptotic point of view. Specifically, we assume that we have n independent sets of training data, produced by Poisson processes on the d-dimensional domain S = [0, 1] d (say), with the same intensity function λ 0 : S → [0, ∞). We aim to construct the learning procedure such that we achieve an optimal learning rate, irrespective of the regularity level of the intensity. In the problem at hand it is known that if λ 0 has regularity β > 0, then the best (minimax) rate that any procedure can achieve is of the order n −β/(d+2β) , see, e.g. Kutoyants (1998) or Reynaud-Bouret (2003). Note that the smoothness degree is unknown to us, so we can not use it in the construction of the procedure, but still we want that the posterior contracts around λ 0 at the rate n −β/(d+2β) , as n → ∞, if λ 0 is β-smooth. In this paper we prove that with appropriate priors on the hyper parameters, the SGCP approach of Adams et al. (2009) attains this optimal rate (up to a logarithmic factor). It does so for every regularity level β > 0, so it is fully rate-adaptive.
Technically the paper uses the mathematical framework for studying contraction rates for Gaussian and conditionally Gaussian priors as developed in van der Vaart and van Zanten (2008a) and van der Vaart and van Zanten (2009).
We also use an extended version of a general result for Bayesian inference for 1-dimensional Poisson processes from Belitser et al. (2013). On a general level the line of reasoning is similar to that of van der Vaart and van Zanten (2009). However, due to the presence of a link function and a random multiplicative constant in the SGCP model (see Section 2 ahead) the results of the latter paper do not apply in the present setting and additional mathematical arguments are required to prove the desired results.
The paper is organised as follows. In Section 2 we describe the Poisson process observation model and the SGCP prior model, which together determine a full hierarchical Bayesian model. The main result about the performance of the SGCP approach is presented and discussed in Section 3. Mathematical proofs are given in Section 4. In Section 5 we make some concluding remarks.

The SGCP model 2.1 Observation model
We assume we observe n independent copies of an inhomogeneous Poisson process on the d-dimensional unit cube S = [0, 1] d (adaptation to other domains is straightforward). We denote these observed data by N 1 , . . . , N n .
The object of interest is the underlying intensity function. This is a (integrable) function λ : [0, 1] d → [0, ∞) with the property that given λ, every N j is a random counting measure on [0, 1] d such that N j (A) and N j (B) are independent if the sets A, B ⊂ [0, 1] d are disjoint and the number of points N j (B) falling in the set B has a Poisson distribution with mean B λ(s) ds.
If we want to stress that the probabilities and expectations involving the observations N j depend on λ, we use the notations P λ and E λ , respectively. We note that instead of considering observations from n independent Poisson processes with intensity λ, one could equivalently consider observations from a single Poisson process with intensity nλ.

Prior model
The SGCP model introduced in Adams et al. (2009) postulates a-priori that the intensity function λ is of the form where λ * > 0 is an upper bound on λ, g is a GP indexed by S and σ is the sigmoid, or logistic function on the real line, defined by σ( In the computational section of Adams et al. (2009) g is modeled as a GP with squared exponential covariance kernel and zero mean, with a prior on the length scale parameter. The hyper parameter λ * is endowed with an independent gamma prior.
In the mathematical results presented in this paper we allow a bit more flexibility in the choice of the covariance kernel of the GP, the link function σ and the priors on the hyper parameters. We assume that g is a zero-mean, homogenous GP with covariance kernel given in spectral form by where ℓ > 0 is an (inverse) length scale parameter and µ is a spectral density on R d such that the map a → µ(aξ) on (0, ∞) is decreasing for every ξ ∈ R d and that satisfies for some δ > 0 (the Euclidean inner product and norm are denoted by ·, · and · , respectively). Note that, in particular, the centered Gaussian spectral density satisfies this condition and corresponds to the squared exponential kernel Eg(s)g(t) = e −ℓ 2 t−s 2 .
We endow the length scale parameter ℓ with a prior with density p ℓ on [0, ∞), for which we assume the bounds, for positive constants C 1 , D 1 , C 2 , D 2 , nonnegative constants p, q, and every sufficiently large x > 0, This condition is, for instance, satisfied if ℓ d has a gamma distribution, which is a common choice in practice. On the upper bound λ * we put a prior satisfying an exponential tail bound. Specifically, we use a positive, continuous prior density for all λ 0 > 0. Note that this condition is fulfilled if we place a gamma prior on λ * . Finally, we use a strictly increasing, infinitely smooth link function σ : R → (0, 1) in (2.1) that satisfies for all x, y ∈ R. This condition is in particular fulfilled for the sigmoid function employed by Adams et al. (2009). It holds for other link functions as well, for instance for the cdf of the standard normal distribution.
The main results of the paper concern the posterior distribution of the intensity function λ, i.e. the conditional λ | N 1 , . . . , N n . Throughout we will denote the prior on λ by Π and the posterior by Π(· | N 1 , . . . , N n ). In this setting Bayes' formula asserts that where the likelihood is given by (see, e.g., Kutoyants (1998)).

Main result
Consider the prior and observations model described in the preceding section and let Π(· | N 1 , . . . , N n ) be the corresponding posterior distribution of the intensity function λ.
The following theorem describes how quickly the posterior distribution contracts around the true intensity λ 0 that generates the data. The rate of contraction depends on the smoothness level of λ 0 . This is quantified by assuming that λ 0 belongs to the Hölder space C β [0, 1] d for β > 0. By definition a function on [0, 1] d belongs to this space if it has partial derivatives up to the order ⌊β⌋ and if the ⌊β⌋th order partial derivatives are all Hölder continuous of the order β − ⌊β⌋. Here ⌊β⌋ denotes the greatest integer strictly smaller than β. The rate of contraction is measured in the L 2 -distance between the square root of intensities. This is the natural statistical metric in this problem, as it can be shown that in this setting the Hellinger distance between the models with intensity functions λ 1 and λ 2 is equivalent to min{ √ λ 1 − √ λ 2 2 , 1} (see Belitser et al. (2013)). Here f 2 denotes the L 2 -norm of a function on S = [0, 1] d , i.e. f 2 2 = S f 2 (s) ds. Theorem 3.1. Suppose that λ 0 ∈ C β [0, 1] d for some β > 0 and that λ 0 is strictly positive. Then for all sufficiently large M > 0, as n → ∞, for some ρ > 0.
The theorem asserts that if the intensity λ 0 that generates the data is β-smooth, then, asymptotically, all the posterior mass is concentrated in (Hellinger) balls around λ 0 with a radius that is up to a logarithmic factor of the optimal order n −β/(d+2β) . Since the procedure does not use the knowledge of the smoothness level β, this indeed shows that the method is rate-adaptive, i.e. the rate of convergence adapts automatically to the degree of smoothness of the true intensity. Let us mention once again that the conditions of the theorem are in particular fulfilled if in (2.1), λ * is taken gamma, σ is the sigmoid (logistic) function, and g is a squared exponential GP with length scale ℓ, with ℓ d a gamma variable.

Proof of Theorem 3.1
To prove the theorem we employ an extended version of a result from Belitser et al. (2013) that gives sufficient conditions for having (3.1) in the case d = 1, cf. their Theorem 1. Adaptation to the case of a general d ∈ N is straightforward. To state the result we need some (standard) notation and terminology. For a set of positive functions F we write F c for its complement and For ε > 0 and a norm · on F, let N (ε, F, || · ||) be the minimal number of balls of radius ε with respect to norm · needed to cover F. The uniform norm f ∞ of a function f on S is defined, as usual, as f ∞ = sup s∈S |f (s)|. The space of continuous function on S is denoted by C(S).
Let Π now be a general prior on the intensity function λ and let Π(· | N 1 , . . . , N n ) be the corresponding posterior (2.7).
Theorem 4.1. Assume that λ 0 is bounded away from 0. Suppose that for positive sequences δ n , δ n → ∞ such that n(δ n ∧ δ n ) 2 → ∞ 1 as n → ∞ and constants c 1 , c 2 > 0, it holds that for all L > 1, there exist subsets F n ⊂ C(S) and a constant c 3 such that Then for ε n = δ n ∨ δ n and all sufficiently large M > 0, as n → ∞.
for constants c 1 , c 2 > 0 and δ n as defined above.
The link function σ is strictly increasing and smooth, hence it has a smooth inverse σ −1 : (0, 1) → R. Define the function w 0 on S by so that λ 0 = 2 λ 0 ∞ σ(w 0 ). Since the function λ 0 positive and continuous on the compact set S it is bounded away from 0 on S, say λ 0 a > 0. It follows that λ 0 (s)/2 λ 0 ∞ varies in the compact interval [a/2||λ 0 || ∞ , 1/2] as s varies in S, whence w 0 inherits the smoothness of λ 0 , i.e. w 0 ∈ C β (S). Now observe that for ε > 0, Since λ * has a positive, continuous density the first factor on the right is bounded from below by a constant times ε. Since the function √ σ is Lipschitz by assumption, the second factor is bounded from below by P( g − w 0 ∞ cε) for a constant c > 0. By Theorem 3.1 in van der Vaart and van Zanten (2009) we have the lower bound with δ n as specified above. The proof of (4.5) is now easily completed.

Construction of sieves
Let H ℓ be the RKHS of the GP g with covariance (2.2) and let H ℓ 1 be its unit ball (see van der Vaart and van Zanten (2008b) for background on these notions). Let B 1 be the unit ball in C[0, 1] d relative to the uniform norm. Define and λ n , M n , γ n , r n and ε n are sequences to be determined later. In the next two subsections we study the metric entropy of the sieves F n and the prior mass of their complements.
(4.6) By substitutingη n = ε n √ λ n we get that for some constants K 1 and K 2 , log N (η n , F n , · 2 ) K 1 r d n log So we conclude that we have the entropy bound log N (η n , F n , · 2 ) nη 2 n for sequences λ n , M n , r n andη n satisfying (4.7) and

Remaining mass
By conditioning we have By (2.5) the second term is bounded by a constant times exp(−c 0 λ κ n ). For the first term, note that for λ λ n we have hence P(λσ(g) ∈ F n ) P(g ∈ G n ). From (5.3) in van der Vaart and van Zanten (2009) we obtain the bound P(g ∈ G n ) K 3 r p−d+1 n e −D 2 r d n log q rn log q r n + e −M 2 n /8 , for some K 3 > 0, ε n < ε 0 for a small constant ε 0 > 0, and M n , r n and ε n satisfying M 2 n > 16K 4 r d n (log(r n /ε n )) 1+d , r n > 1, (4.9) where K 4 is some large constant. It follows that P(g ∈ G n ) is bounded above by a multiple of exp (−Ln η 2 n ) for a given constant L and η n = λ n ε n , provided M n , r n , γ n and ε n satisfy (4.9) and D 2 r d n log q r n 2Ln η 2 n , r p−d+1 n e Ln η 2 n , M 2 n 8Ln η 2 n . (4.10) Note that in terms ofη n , (4.9) can be rewritten as M 2 n > 16K 4 r d n (log(r n λ n / η n )) 1+d , r n > 1. (4.11) We conclude that if (4.11),(4.10) holds and c 0 λ κ n > Ln η 2 n , (4.12) then P(λ * σ(g ∈ F n )) e −Ln η 2 n .

Completion of the proof
In the view of the preceding it only remains to show that η n ,η n , r n , M n > 1 and λ n can be chosen such that relations (4.7), (4.8), (4.10), (4.11) and (4.12) hold.
One can see that it is true for η n = δ n andη n = δ n described in the theorem, with r n , M n , λ n as follows:

Concluding remarks
We have shown that the SGCP approach to learning intensity functions proposed by Adams et al. (2009) enjoys very favorable theoretical properties, provided the priors on the hyper parameters are chosen appropriately. The result shows there is some flexibility in the construction of the prior. The squared exponential GP may be replaced by other smooth stationary processes, other link functions may be chosen, and there is also a little room in the choice of the priors on the length scale and the multiplicative parameter. This flexibility is limited, however, and although our result only gives upper bounds on the contraction rate, results like those of Castillo (2008) and van der Vaart and van Zanten (2011) lead us to believe that one might get sub-optimal performance when deviating too much from the conditions that we have imposed.
We expect that a number of generalizations of our results are be possible. For instance, it should be possible to obtain generalizations to anisotropic smoothness classes and priors as considered in Bhattacharya et al. (2014), and classes of analytic functions as studied in van der Vaart and van Zanten (2009). These generalizations take considerable additional technical work however and are therefore not worked out in this paper. We believe they would not change the general message of the paper.