José Luiz Fiadeiro

Antónia Lopes

Laura Bocchi

Antpay Ant

Laupay Lau

Cpl Lauba

Under consideration for publication in Formal Aspects of Computing An Abstract Model of Service Discovery and Binding

Keywords: Business-reflective run-time configurations, Dynamic reconfiguration, Quality-of-service constraints, Service binding, discovery, ranking, Service level agreement, Service-oriented computing

come

Introduction

Service-Oriented Computing (SOC) is a new paradigm in which interactions are no longer based on the exchange of products with specific parties -what is known as clientship in object-oriented programming -but on the provisioning of services by external providers that can be procured on the fly subject to a negotiation of service level agreements (SLAs). A number of research initiatives (among them the FET-GC2 integrated project Sensoria [WHar]) have been proposing formal approaches that address different aspects of the paradigm independently of the specific languages that are available today for Web Services (e.g., [START_REF] Bistarelli | Semiring-based constraint satisfaction and optimization[END_REF][START_REF] Peltz | Web services orchestration and choreography[END_REF]) or Grid Computing (e.g., [START_REF]The Grid 2: Blueprint for a New Computing Infrastructure[END_REF]). For example, recent proposals for service calculi (e.g., [BBC + 06, CHY07, LPT07, KQCM09]) address operational foundations of SOC (in the sense of how services compute) by providing a mathematical semantics for the mechanisms that support choreography or orchestration -sessions, message/event correlation, compensation, inter alia. This line of work has contributed to languages and standards developed by organisations such as OASIS (www.oasis-open.org) and W3C (www.w3.org) for Web Services.

Whereas such calculi address the need for specialised language primitives for programming in this new paradigm, we are still lacking models that are abstract enough to understand the engineering foundations of SOC, i.e., those aspects (both technical and methodological) that concern the way applications can be developed to provide business solutions, independently of the languages in which services are programmed. The Open Service Oriented Architecture collaboration (www.osoa.org) has been proposing a number of specifications, namely the Service Component Architecture (SCA), that address this challenge: "SCA aims to provide a model for the creation of service components in a wide range of languages and a model for assembling service components into a business solution -activities which are at the heart of building applications using a service-oriented architecture" [START_REF] Osoa | Service component architecture: Building systems using a service oriented architecture[END_REF].

However, SCA addresses low-level design in the sense that it provides an assembly model and binding mechanisms for service components and clients programmed in specific languages, e.g., Java, C++, BPEL, or PHP. The goal of the work that we discuss in this paper is to address high-level design. More specifically, we aim for models and mechanisms that support the design of complex services from business requirements in ways that are independent of the languages in which the service components are programmed, and for analysis techniques through which designers can verify or validate properties of composite services. So far, SOC has been short of support for high-level modelling. Indeed, languages and models that have been proposed for service modelling and design (e.g., [START_REF] Broy | A formal model of services[END_REF][START_REF] Remco | Service-oriented design: A multi-viewpoint approach[END_REF][START_REF] Reisig | Modeling-and analysis techniques for web services and business processes[END_REF]) do not address the higher level of abstraction that is associated with business solutions, in particular the key characteristic aspects of SOC that relate to the way those solutions are put together dynamically in reaction to the execution of business processes -run-time discovery, instantiation and binding of services. Yet, these dynamic aspects are among those that truly distinguish SOC from component-based development and other forms of distributed computing [START_REF] Elfatatry | Dealing with change: components versus services[END_REF][START_REF] Gu | A stakeholder-driven service life cycle model for soa[END_REF]. They are also the aspects that are particularly relevant for the engineering foundations of SOC. This is why, within Sensoria, we have defined the modelling language Srml [FLBAar]. Its 'static' aspects -the design-time definition of complex services in terms of orchestrations of simpler servicesare formalised over state transition systems and temporal logic [START_REF] Abreu | A coordination model for service-oriented interactions[END_REF][START_REF] Luiz Fiadeiro | A formal model for service-oriented interactions[END_REF]. Its 'dynamic' aspects are formalised over the mathematical model put forward in this paper. More specifically, the model that we propose herein is, essentially, parametric in the formalisms adopted for modelling the static aspects and, therefore, can be instantiated for those used in Srml. To the best of our knowledge, our approach is the first to provide a clear separation between service computation and discovery/instantiation/binding, and to offer a formal framework that is independent of the SOA middleware components that act as service registries or brokers (e.g., the UDDI [UDD04]) and the protocols through which bindings and invocations are performed (e.g., SOAP [W3C07]).

In the rest of this section, we make more precise the nature and the role of the mathematical model that we define in the paper. We also present the example that will be used to illustrate the way our model supports SOC. In Section 2, we expand on the notion of service-overlay computer; we discuss the notion of a service that we address in the paper and the impact of SOC on software engineering methodology; then, we put forward a layered graph-based model for state configurations of global computers, made to be 'business reflective' by enriching them with an explicit representation of the types of business activities that are active in the current state. In Section 3, we discuss the typing mechanism that we propose for services and a notion of correctness that acts as an abstract static semantics of services; we also formalise the notion of quality of service. In Section 4, we present a formal model for service discovery and binding. In Section 5, we compare our proposal to other related approaches. We conclude with an overview of the way the proposed formal model was used within Sensoria in support of a service-based modelling approach to software-intensive systems.

Models for service-oriented computing

Mathematical models that capture the essence of a paradigm at the desired level of abstraction play an essential role as a foundation for methods, languages and support tools for that paradigm. The choice of a model reflects the level of abstraction at which one wishes to capture a particular aspect of a paradigm. In this paper, our concern is not the behaviour of software applications viewed in terms of the transformations that they perform over data or the events that they exchange with their environment. Like in SCA, we address the coarser-grain process that SOC induces over the configuration of systems because of the ability that applications have to bind dynamically to services that are discovered, selected and instantiated at run time. This is why, drawing an analogy with the semantics of programming languages, we could say that we put forward mathematical notions of (typed) state and state transition that account for the evolutionary process that SOC induces over software systems.

Therefore, the proposed model addresses the layer of abstraction that SOAs superpose over any concrete computer platform in terms of service discovery, instantiation and binding. Just like developers working over an object-oriented platform do no need to program the dynamic allocation, referencing and de-referencing of names, designers of complex services working over a SOA should not need to include the discovery, selection and binding processes among the tasks of the orchestrators of the services.

In this sense, our aim is to provide an abstract virtual machine that captures the essence of SOC as a 'business overlay computer'. Our operational model does not include the service broker or the service providers as components of the system -it relies on them as resources available in the architecture in the same way as an operational model for sequential programming does not include memory allocation or access as processes. The availability of abstract models such as the one we propose in this paper is a precondition for defining semantically-enhanced service discovery [START_REF] Papazoglou | Service-oriented computing: State of the art and research challenges[END_REF], a challenge that has already led to the definition of a run-time infrastructure consisting of a number of brokers that handle quality-of-service constraints [START_REF] Mukhija | QoS-aware service composition in Dino[END_REF].

More specifically, in the model that we propose in Section 2, the states of the abstract virtual machine are graphs of components and connectors that capture configurations that execute business activities, and state transitions are reconfigurations that result from binding to selected services. In order to make the model reflective (in the sense of [CBG + 08], as discussed in Section 2.3), states are typed with so-called activity modules, which determine the state transitions that are possible, i.e., the services that need to be discovered and the criteria for selection -matching required functional properties and optimising quality-of-service constraints. In Section 2.2, we also discuss how these abstract states and transitions of the configuration process relate to the computational model that captures the way components execute in each configuration.

The travel-booking scenario

In order to illustrate our approach, we use a travel-booking scenario that goes somewhat beyond what is typically found in papers on SOA. In this example, we consider the case of a company that wishes to offer as a service the ability to book a flight and a hotel according to given preferences, and handle the corresponding payments. For that purpose, the company has a database of clients and an agent that orchestrates a booking process that relies on three external agents: one that handles the booking of the flights, another the booking of the hotel, and a third the payments. In order to be able to offer the best possible deal at any moment and take into account data of the specific customer, these external agents are procured at run time subject to given service-level agreements.

From the software development point of view, adopting a service-oriented approach means that the booking agent is not programmed to perform the discovery and selection of these external agents. These tasks are left to the middleware, which is also responsible for binding the booking agent with the selected agents. From a modelling point of view, this means that the task of the designer is just to define the criteria according to which the discovery and selection should be made. Concerning the database of users, although it is external to the service, it is internal to the service provider and does not need to be discoveredbinding takes place when the service is invoked and the booking agent is instantiated.

The customers of the service offered by this company will be software components that implement business activities run by other companies, which require the use of a travel agent. This means that, in order to be discovered by these activities, our travel-booking service provider needs to register with a directory in which it advertises the properties of the service that it offers. Typically, these business activities will include an interface to a user that can invoke them directly. In our example, this user could be a person wishing to go on holiday who uses a web browser to launch an activity on their favourite holiday agent's site. That activity would then execute its business process over a SOA, which could include binding dynamically to a travel agent that, say, offers a best match for the user's environmental concerns or to a trusted agency that can provide a nanny to look after the user's children.

Business-Reflective Configurations of Global Computers

Service-overlay engineering methodology

The term 'service' is being used in Information Technology (IT) in a wide variety of contexts, often with different meanings. In this paper, we address the notion of 'service-overlay computer', by which we mean the development of highly-distributed loosely-coupled applications over 'global computers' -"computational infrastructures available globally and able to provide uniform services with variable guarantees for communication, co-operation and mobility, resource usage, security policies and mechanisms" (see the Global Computing Initiative at cordis.europa.eu/ist/fet/gc.htm).

In this context, it is necessary to rethink the way software applications are engineered. It is clear that the typical 'static' scenario in which components are assembled to build a (more or less complex) system that is delivered to a customer no longer applies. Instead, SOC supports more 'dynamic' development scenarios in which (smaller) applications are developed to run on global computers and respond to business needs by interacting with services and resources that are globally available. In this latter setting, there is much more scope for flexibility in the way business is supported: business processes need not be confined to fixed organisational contexts; they can be viewed in more global contexts as emerging from a varying collection of loosely coupled applications that can take advantage of the availability of services procured on the fly when they are needed.

Indeed, an important impact that we see SOC having on software engineering methodology derives from the fact that the discovery and selection of services required by business applications is performed, on the fly, by the middleware (not by skilled engineers at design time), and that this selection is not made from a fixed universe of business components but an open and dynamic market of service provision. Likewise, developing services that can be discovered is not the same as developing software applications to a costumer's set of requirements: it is a separate business that exists independently of the nature of the customers. This independence requires the definition of shared ontologies of data and services so that providers and requesters can negotiate and agree on levels of service provision.

This view is summarised (in a somewhat abstract form) in Figure 1, where we elaborate beyond the basic Service-Oriented Architecture [START_REF] Alonso | Web Services -Concepts, Architectures and Applications[END_REF] to make explicit the different stakeholders and the way they interact, which is important for understanding the formal model that we are proposing. In this model, we distinguish between 'business activities' and 'services' as software applications that pertain to different stakeholders (see [START_REF] Gu | A stakeholder-driven service life cycle model for soa[END_REF] for a discussion on the stakeholders of service-oriented systems):

• Activities correspond to applications developed by 'business IT teams' according to requirements provided by their organisation, e.g., the applications that, in a tour operator, implement the products that are made available to its customers. The activity repository provides a means for the computing infrastructure of the organisation to trigger such applications when the corresponding requests are published, say when a client requests a quote for a holiday at a counter or through the web. The implementation of activities may resort to 'classical' direct invocation of components (e.g., for exchange rates or medical insurance), but it can also rely on services that will be procured on the fly (for instance, an agent that can take care of the travel requirements) to ensure competitiveness and context-based optimisation. • Services differ from activities in that they are not developed to satisfy specific business requirements of a given organisation. Instead they are developed by service providers who publish them (in service repositories) in ways that allow them to be discovered when a request for an external service is published in the run-time environment. As such, they are classified according to generic service descriptions that are organised in a hierarchical ontology to facilitate discovery. In the SOA middleware that is currently available, the UDDI [UDD04] is an example of a (less sophisticated) service registry or broker.

Notice that the 'business IT teams' and the 'service providers' can be totally independent and unrelated: the former are interested in supporting the business of their companies or organisations, whereas the latter run their own businesses. They share the ontology component of the architecture so that they can do business together. In addition to these two repositories, our engineering infrastructure includes:

• A configuration management unit, which is responsible for the binding of the new components and connectors that derive from the instantiation of new activities or services. Current SOA middleware uses mechanisms like SOAP [W3C07] for providing the protocols through which bindings and invocations are performed.

Current configuration

(software components and interaction protocols that interconnect them)

Triggers Reconfiguration

Discovery and selection Invocation

Business IT teams

Service providers

Publication Application development

Ontology

(data and service descriptions)

Configuration Management

Service repository t t • An ontology unit, which is responsible for organising both data and service descriptions. This is an area that is still lacking standards, though there has been substantial progress in the development of Semantic Web techniques (see the W3C Semantic Web Activity at www.w3.org/2001/sw/).

Activity repository

In the context of this infrastructure, the paper makes the following contributions:

• It proposes a formal (graph-based) model for the 'current configuration' (Section 2.2).

• It proposes formal notions of type for business activities and services that are parametric on the formalisms that are used for describing orchestrations and interactions (Sections 2.3 and 3.1).

• It uses these types to make the current configuration business-reflective, i.e., it adds to the configuration a level of representation that makes the underlying business model explicit and uses that representation for rewriting the configuration according to given business rules (Sections 2.3 and 3.1).

• It proposes a formal notion of SLA and negotiation based on constraint optimisation with c-semirings [BMR97] (Sections 3.2 and 4.1).

• It proposes a formal model of service discovery and binding over such business-reflective configurations (Section 4.1).

We do not discuss the classification and retrieval mechanisms per se, i.e., the processes through which the activity and service repositories are managed. See, for instance, [START_REF] Pahl | An ontology for software component matching[END_REF][START_REF] Rao | A survey of automated web service composition methods[END_REF] for some of the aspects involved when addressing such issues.

Layered state configurations of global computers

As already mentioned, we take SOC to be about applications that can bind to other applications discovered at run time in a universe of resources that is not fixed a priori. As a result, there is no structure or configuration (or what sometimes is called 'system architecture') that one can fix at design-time for an application; rather, there is an underlying notion of configuration of a global computer that keeps being redefined as applications execute and get bound to other applications that offer required services. As is often the case (e.g., [START_REF] Allen | A formal basis for architectural connection[END_REF]), by 'configuration' we mean a graph of components (applications deployed over a given execution platform) linked through wires (e.g., interconnections between components over a given communication network) in a given state of execution. Typically, wires deal with the heterogeneity of the partners involved in the provision of the service, performing data (or, more, generally, semantic) integration. Figure 2 presents an example of a configuration related to the case study described in Section 1.2the nodes of the configuration graph correspond to the boxes and the edges to the lines (the meaning of the shadows is explained below). The example consists of two instances of a travel-booking activity sharing a database DB of users. Each of these activities corresponds to a sub-graph that captures a distributed orchestration of the activity, as explained in Section 2.3 and illustrated in Figure 3.

We denote by Comp and Wire the set of all components and wires, respectively. Every component c∈Comp and wire w∈Wire may be in a number of states (e.g., valuations of local state variables), the set of which is denoted by State c and State w , respectively. We denote by State the corresponding indexed family of sets of states. The precise nature of these local states is of no particular importance for this paperin relation to the semantics of discovery and binding, the dependency on states concerns the evaluation of the conditions that trigger the discovery of external services (as discussed in Section 4.1) and the initialisation of the new components and wires that result from the binding (as discussed in Section 4.2), both of which are dealt with what we call 'internal configuration policies' (see Section 3.2). Consequently, we refrain from making any further assumptions on State. The specific nature of the states and state transitions used in Srml is presented in [START_REF] Luiz Fiadeiro | A formal model for service-oriented interactions[END_REF]. Definition 2.1 (State configuration). A state configuration F consists of:

• A simple graph G, i.e., a set nodes(F) and a set edges(F) where every edge is associated with a 2element set (unordered pair) n↔m of nodes. We take nodes(F)⊆Comp (i.e., nodes are components) and edges(F)⊆Wire (i.e., edges are wires). • A (configuration) state S, which assigns a state S(n)∈State n to every node n and a state S(e)∈State e to every edge e.

Every state configuration G, S can change because either the state function S or the graph G changes (or both, in the case of components or wires that are not effected by the reconfiguration). Changes to the state function result from computations executed by components and the coordination activities performed by the wires that connect them. However, the essence of SOC, as we see it in this paper, is not captured at the level of state changes (which is basically a distributed view of computation), but at the level of the changes that operate on configuration graphs: in SOC, changes to the underlying graph of components and wires occur at run time when a component performs an action that triggers the discovery and binding of a service. Another important aspect of our model is the fact that we view SOC as providing a layer that interacts with two other layers. This can be noticed in Figure 2 where shadows are used for indicating that certain components reside in different layers: LUI and AUI (two user interfaces) belong to what we call the top (or user) layer; DB (a database of users) lies in the bottom (or persistent) layer; all other components execute in the middle (or service) layer.

We use layers as abstractions of organisation and change, not as hierarchies of implementation as found in software engineering where one layer provides the implementation of the design primitives used in the layer above. Our notion of layer is closer to that of 3-tiered architectures, but our layers do not impose a strict hierarchical design methodology in the sense that components are not designed and implemented to sit on a particular layer. Rather, our layers reflect the dynamics of configurations from the point of view of the activities that drive a given business system. This is why there is no formal, static semantics of layers: a configuration is a (flat) graph as indicated above but, in order to understand and model the way it evolves, it is useful to distinguish different levels of dynamicity.

More precisely, in the context of a business activity (for example, an activity executing the request of a client for booking a holiday), the components that execute in the middle layer reflect the sessions of a number of services whose discovery the activity has triggered (e.g., the workflow that orchestrates the travel reservation of that client). These components are created when the session of the corresponding service starts, i.e., as fresh instances that last only for the duration of the session.

The bottom layer consists of the components and connectors that are persistent as far as the service layer is concerned; that is, when a new session of a service starts (for example, a travel agent starts booking a trip on behalf of the activity's client), the components of the bottom layer should be available so that, as the service executes, they can be used as (shared) servers -for example, a database of clients shared by all sessions of the travel booking service, or the reservation log of a hotel, or a currency converter. In particular, the bottom layer can be used for making persistent the effects of services as they execute. In componentbased development (CBD) one often says that the bottom layer provides 'services' to the layer above. As we see it in this paper, the difference between CBD and SOC is precisely in the way such services are procured, which in the case of SOC involves identifying (possibly new) providers and negotiating terms and conditions for each new instance of the activity, e.g., for each new user of a holiday-booking agent. SOA middleware supports this service layer by providing the infrastructure for the discovery and negotiation processes to be executed without having to be explicitly programmed as (part of) components.

The top layer is the one responsible for launching business activities. More precisely, the user of a given activity resides in the top layer; it can be an interface for human-computer interaction, a software component, or an external system (e.g., a control device equipped with sensors). When the user launches an activity, a component is created in the service layer that starts executing a workflow that may involve the orchestration of services that will be discovered and bound to the workflow at run time. This is explained in more detail in Section 4.2.

Business activities and configurations

In our model, state configurations change as a result of the execution of business processes. More precisely, changes to the configuration graph result from the fact that the discovery of a service is triggered and, as a consequence, new components are added and bound to existing ones (and, possibly, other components and wires disappear because they finished executing). The information about the triggers and the constraints that apply to service discovery and binding are not coded in the components themselves: they are properties of the business activities that are active and determine how the configuration evolves. Thus, in order to formalise the dynamic aspects of SOC, we need to look beyond the information available in a state configurationstate configurations account only for which components are active and how they are interconnected, not why they are active and interconnected in that way.

Business activities are autonomous and active computational ensembles of components that collectively pursue a given business goal and are able to bind dynamically to services discovered at run time, thus reconfiguring the ensemble as it executes. A business activity is characterised, in every configuration, by:

• A sub-configuration, i.e., a subset of the components, and the wires between them, that execute as part of the activity. • A model of the workflow that implements the business logic of the activity.

For instance, we identify in Figure 3 the sub-configurations of the two activities that we mentioned relative to the configuration depicted in Figure 2. Intuitively, both correspond to two instances of the same business logic (two customers booking their travel using the same service) but at different stages of their workflow: one (launched by LUI) is already connected to a flight and a hotel agent (LauF and LauH, respectively); the other (launched by AUI) is also connected to a (different) flight agent (AntF), but still has to find a hotel agent. Both share the component DB (a database of users shared by all instances of the service), which resides in the bottom layer (for persistency).

What we are calling 'business logic' is formally captured by typing the sub-configuration of the activity by what we call an 'activity module'. An activity module is a modelling artefact defined by a graph whose nodes correspond to interfaces and are typed by formal descriptions or specifications of the behaviour expected at those interfaces. We use the graphical notation of Srml [FLBAar] to depict activity modules, an example of which is given in Figure 4 (a summary of the elements used in this notation is given in the Appendix).

We distinguish between different kinds of interfaces, which in the graphical notation corresponds to the shapes and their placement relative to the boundary. What we call 'component-interfaces' correspond to the rectangles inside the boundary: their labels are called 'business roles', which describe the behaviour of the components that, in a state configuration, implement the interface. For instance, the activity module depicted in Figure 4 types the component-interface Lau with the business role BizTrav. For the purposes of this paper, the exact language that is used for defining business roles is not important. We will simply assume that we have available a set Brol of business roles and a typing relation on Comp × Brol through which we can tell whether a given component complies with a given business role.

Other nodes of activity modules may consist of interfaces to components of the bottom layer: this is the case of DB of type UsrDB. Several such 'uses-interfaces' (possibly none) can be included in an activity module. They are depicted through skewed quadrangles and placed at the bottom boundary. Every activity module includes a 'serves-interface' for the top layer, also depicted through a skewed quadrangle but placed at the top boundary. This is the case of LUI of type TravUI -a user interface through which the travel booking is made. Both uses-and serves-interfaces are labelled by 'layer protocols' -descriptions of the behaviour that can be expected at the interfaces. Once again, the exact nature of these descriptions is not relevant for the purposes of this paper, so we will simply assume that we have available a set Layp of specifications of layer protocols and a typing relation on Comp × Layp.

The edges of an activity module are called 'wire-interfaces' and labelled with connectors [START_REF] Allen | A formal basis for architectural connection[END_REF]. For instance, in Figure 4, the wire-interface BHL is labelled with the connector c 3 , ≡, b 2 . As defined in Section 3.3, a connector consists of an 'interaction glue' that describes a protocol between two 'roles' (by ≡ we denote a direct transmission of events [START_REF] Abreu | Specifying and composing interaction protocols for service-oriented system modelling[END_REF]) and two attachments (c 3 and b 2 in the example at hand) linking the roles to the two nodes (LauBA and LauH, respectively). In general, the interaction glue may include the routing of events, encryption/decryption of messages, or transforming sent data to the format expected by the receiver. See [START_REF] Abreu | Specifying and composing interaction protocols for service-oriented system modelling[END_REF] for a detailed account of how connectors are formalised in Srml, and [START_REF] Luiz | Structured co-spans: An algebra of interaction protocols[END_REF] for a language-independent algebraic semantics. We use Cnct to designate the set of connectors and Iglu the set of specifications of the corresponding interaction glue. We also rely on a typing relation Wire × Cnct between wires and connectors. In software architecture in general, connectors may involve an arbitrary number of roles, but service-oriented architectures involve only interactions between two parties.

Finally, an activity module identifies three important aspects related to the way the configuration can evolve and the activity can reconfigure its workflow:

• The external services that the activity may still need to discover and bind to in order to fulfil its business goal. • An internal configuration policy (indicated by the symbol ), which identifies the triggers of the external service discovery process as well as the initialisation and termination conditions of the components.

• An external configuration policy (indicated by the symbol

SLA

), which consists of the variables and constraints that determine the quality profile of the activity to which the discovered services need to adhere.

The configuration policies (both internal and external) are discussed in more detail in Section 3.2.

Concerning the external services, activity modules can have multiple (or none) 'requires-interfaces', which are labelled by 'business protocols' specifying the properties required of the services that need to be procured externally. Requires-interfaces are presented by convex pentagons and placed at the right-hand boundary. For instance, the node BA labelled by the business protocol HotelAgent in the activity module depicted in Figure 5 is a requires-interface for a hotel booking service. In Srml, business protocols are specifications written in a temporal logic of stateful interactions [START_REF] Luiz Fiadeiro | A formal model for service-oriented interactions[END_REF]. Once again, the exact logic that is used for specifying requires-interfaces is not relevant for this paper, so we assume that we have available a set Busp of specifications of business protocols.

Notice that the wire-interfaces that connect the requires-interfaces to the other parties -BH in the example in Figure 5 -should also be seen as part of the services that are required by the activity. More precisely, they specify the protocols through which the activity wants to interact with the external services.

Definition 2.2 (Activity module). An activity module M consists of:

-label M (n)∈Brol if n∈components(M ), where components(M ) = nodes(M ) \ (requires(M ) ∪ uses(M ) ∪ {serves(M )}) -label M (n)∈Busp if n∈requires(M ) -label M (n)∈Layp if n∈uses(M ) -label M (serves(M ))∈Layp -label M (e)∈Cnct if e∈edges(M )
• An internal configuration policy (discussed in Section 3.2).

• An external configuration policy (discussed in Section 3.2).

We denote by body(M ) the (full) sub-graph of graph(M ) that forgets the nodes in requires(M ) and the edges that connect them to the rest of the graph.

We can now formalise the typing of state configurations with activity modules that we discussed in relation to Figure 3, which accounts for the coarser business dimension that is overlaid by services on global computers. That is, we define what corresponds to a state configuration of a service overlay computer, which we call a business configuration. We consider a space A of business activities to be given, which can be seen to consist of reference numbers (or some other kind of identifier) such as the ones that organisations automatically assign when a service request arrives.

Definition 2.3 (Business configuration). A business configuration consists of:

• A state configuration F. • A partial mapping B that assigns an activity module B(a) to some activities a∈A -a model of the workflow being executed by a in F. We say that the activities in the domain of this mapping are those that are active in that state configuration. • A mapping C that assigns a homomorphism C(a) of graphs body(B(a)) → F to every activity a∈A that is active in F. We denote by F(a) the image of C(a) -the sub-configuration of F that corresponds to the activity a.

A homomorphism of graphs is just a mapping of nodes to nodes and edges to edges that preserves the end-points of the edges. Therefore, the homomorphism C of a business configuration F, B, C types the nodes (components) of F(a) with business roles or layer protocols -i. -and the edges (wires) with connectors -i.e., C(a)(e) : label B(a) (e) for every edge e of the body of the activity. In other words, the homomorphism binds the components and wires of the state configuration to the business elements (interfaces labelled with business roles, layer protocols and connectors) that they fulfil in the activity.

We normally represent the homomorphism C(a) by drawing a dashed line around F(a) and replacing the nodes of B(a) by those of F(a) as in Figure 6 for an activity that we will call ANT -the state graph is the one in Figure 2, the sub-configuration F(ANT) is the one that we marked in the lower part of Figure 3, and the activity module B(ANT) is as in Figure 5. Notice that although we use the same icons for state configurations as for modules, the nodes of modules are not components and the edges are not wires: modules involve abstract models, not instances. The homomorphism establishes the correspondence between the two levels.

The fact that the homomorphism is defined over the body of the activity module means that business protocols are not used for typing components of the state configuration -one can note in Figure 6 that the node HA of the activity module is not mapped to the state configuration. Indeed, as discussed above, the purpose of the requires-interfaces is for identifying dependencies that the activity has, in that state, on external services. In particular, this makes requires-interfaces different from uses-interfaces as the latter are indeed mapped through the homomorphism to a component of the state configuration. The operational semantics that we propose in Section 4.2 for discovery and binding shows that these two kinds of interfaces fulfil totally different purposes: the former are for 'horizontal' dynamic composition through service discovery and binding; the latter are for 'vertical' composition with the bottom layer through a 'classic' static binding process.

In a sense, the homomorphism makes state configurations reflective in the sense of [CBG + 08] as it adds meta (business) information to the state configuration. This information is used for deciding how the configuration will evolve (namely, how it will react to events that trigger the discovery process). Indeed, reflection has been advocated as a means of making systems adaptable through reconfiguration, which is similar to the mechanisms through which activities evolve in our model.

Modelling Services

Service modules

In our approach, services are modelled through 'service modules', which are like the activity modules that we discussed in the previous section except that, instead of a serves-interface to the upper layer, they include a 'provides-interface' through which activities can connect to the service (identified through a requiresinterface). Such interfaces are labelled by business protocols that describe the properties that a customer can expect from the interactions with the service. Uses-interfaces and requires-interfaces can be included in service modules in the same way as in activity modules. Definition 3.1 (Service module). A service module M consist of:

• A graph graph(M ). • A distinguished subset of nodes requires(M )⊆nodes(M ). • A distinguished subset of nodes uses(M )⊆nodes(M ). • A node provides(M )∈nodes(M ) not belonging to requires(M ) or uses(M ). • A labelling function label M such that -label M (n)∈Brol if n∈components(M ), where components(M ) = nodes(M ) \ (requires(M ) ∪ uses(M ) ∪ {provides(M )}) -label M (n)∈Busp if n∈requires(M ) -label M (n)∈Layp if n∈uses(M ) -label M (provides(M ))∈Busp -label M (e : n↔m)∈Cnct
• An internal configuration policy (discussed in Section 3.2).

• An external configuration policy (discussed in Section 3.2).

We denote by body(M ) the (full) sub-graph of graph(M ) that forgets provides(M ), the nodes in requires(M ), and the edges that connect these nodes (including provides(M )) to the rest of the graph.

In Figure 7 we present the structure of a module that defines a service provided through an interface CR of type Customer for booking a flight and a hotel for a given itinerary and dates. The service relies on a component BA of type BookingAgent that orchestrates interactions with a service FA of type FlightAgent (for booking flights), a service HA of type HotelAgent (for booking hotel rooms), a service PA of type PayAgent (for handling payments), and an external component DB of type UsrDB (that stores information about registered users). The module also makes explicit the connectors that, through the wires, coordinate the communication between the parties involved in the provision of the service. Notice that the wires that connect the providesinterface -CP and CB -are also part of the service offered by the module, i.e., they declare the protocols through which the service can interact with its customers.

The definition of (service) module was inspired by concepts proposed in the Service Component Architecture (SCA) [START_REF] Osoa | Service component architecture: Building systems using a service oriented architecture[END_REF]: "SCA is based on the idea that business function is provided as a series of services, which are assembled together to create solutions that serve a particular business need. These composite applications can contain both new services created specifically for the application and also business function from existing systems and applications, reused as part of the composition. SCA provides a model both for the composition of services and for the creation of service components, including the reuse of existing application function within SCA compositions". Service modules as defined in this paper provide formal abstractions of composite services in the sense of SCA and the way their execution involves a number of external parties that derive from the logic of the business domain. These external parties are not explicitly identified in the module but only implicitly through what we have called requires-and uses-interfaces. As already explained, such interfaces are more than syntactic declarations: they are typed by business protocols -abstract specifications of the conversations in which the parties are required to be involved -or by layer protocols in the case of uses-interfaces -abstract specifications of the interactions supported with the external party. Likewise, the components themselves are not explicitly identified in the module. Instead, the module includes semantic interfaces -business roles -that model the way interactions are orchestrated by the components.

In the case of the provides-interface, the corresponding party is the customer to which the module will be bound to provide a service. The behavioural properties offered in the business protocol that corresponds to the provides-interface result from:

• The tasks performed by the (internal) components that instantiate the business roles;

• The interactions with the external parties that instantiate the requires-and uses-interfaces (and satisfy the properties specified in the corresponding business and layer protocols).

For instance, the business protocol Customer could describe that committing to an offer made by the BookingAgent ensures that the outcome of the payment process will be acknowledged and that the period during which a booking can be revoked (negotiated prior to binding) is within certain bounds. One of the advantages of working in a formal framework such as ours is that we are able to check that the properties being offered in the provides-interface do result from the orchestration, which in the case of Srml is achieved through model-checking techniques [START_REF] Abreu | A model-checking approach for service component architectures[END_REF]tBFGM08]. This notion of correctness is defined in Section 3.3.

By 'customer' we mean the business activity that triggers the discovery of the service, not the top layer user. Indeed, service modules do not include the serves-interface because, in our model, interactions with the top layer are performed exclusively by business activities. Hence, a user cannot invoke directly a service; a user can launch an activity that, as part of its workflow, may trigger the discovery of a service. As already mentioned, this is, for us, a distinguishing aspect of SOC when compared to CBD. For instance, in the case of the business configuration that corresponds to Figure 3, we can see components -Lau and Ant -that interact with the users of the activities through two interfaces (LUI and AUI, respectively). As discussed in Section 4.2, these two interface components are created when the business activities are launched by the corresponding users, orchestrating the interactions with the service components and the corresponding user. We can use this example to illustrate how our operational semantics of service discovery and binding works. Consider that, in the current state configuration, the top layer entity AUI launches a business activity ANT typed by the activity module A ANT0 as in Figure 8. (We will not discuss the operational semantics of the top layer, i.e., the mechanism through which entities of the top layer create new components in the service layer.) Consider further that, at a certain point during the execution of the component Ant, the trigger condition trigTA becomes true and that the service TravelBooking as defined in Figure 7 is selected. The result of the binding is depicted in Figure 9 (and explained in Section 4.2): a new session of Travel-Booking starts, which adds the component AntBA to the service layer of the state configuration and connects it to Ant and the component DB of the bottom layer. That is, the workflow of activity ANT is reconfigured and is now typed by the activity module A ANT1. Notice that every new session of a service adds to the configuration new instances (components) of its business roles but uses the components already available in the bottom layer.

The configuration depicted in Figure 2 with ANT typed as in Figure 5 would be reached after trigFA and trigPA become true. Notice that, besides the workflow, the external configuration policy also changes as new services are discovered and bound. This process, which determines the ranking and selection of the service, is discussed in Section 4.

The configuration policies

Whereas business roles, business protocols, layer protocols and interaction protocols deal with functional aspects of the behaviour of a (complex) service or activity, configuration policies address properties of the configuration process itself. This is why we focus on them in more detail in this paper.

The internal configuration policy of a module M concerns the timing of the binding of its interfaces and instantiation of its component and wire interfaces. • For each requires-node n∈requires(M ), an associated trigger condition trigger(n): this is a condition that is evaluated over the state of the activity (i.e., the sub state configuration that corresponds to the activity). When this condition becomes true as a result of a computation step, the process of discovery, selection and binding starts executing, leading to a reconfiguration step (as discussed in Section 4.2) that completes the transition of state configurations. The next computation step takes place in the new configuration, i.e., computations resume when the components of the selected service are instantiated and connected to those of the activity. • For each component-node n∈components(M ), an initialisation condition init(n) that is ensured when the component is instantiated (as discussed in Section 4.2). Typically, these are conditions on the way the state variables of the component are initialised, but they can also include the publication of given events. • For each component-node n∈components(M ), a second state condition term(n) that determines when the component stops executing and interacting with the rest of the components of the activity. Typically, this condition triggers a garbage collection process that removes the associated wires from the configuration, which may also require the delivery of any events pending in the wires (unless we choose to allow for the loss of events).

The external policy concerns the way the module relates to external parties: it declares a set of constraints that have to be taken into account during discovery and selection. Every constraint involves a set of variables that includes both local parameters of the service being provided (e.g., the percentage of the cost of a trip that is refundable) and standard configuration parameters selected from a fixed set of types -availability, response time, message reliability, inter alia. These standard configuration parameters may apply to the service being provided, or to the services that need to be procured externally, or to the wires.

In our approach, we adopt the framework for constraint satisfaction and optimization presented in [START_REF] Bistarelli | Semiring-based constraint satisfaction and optimization[END_REF], in which constraint systems are defined in terms of c-semirings. As explained therein, this framework is quite general and allows us to work with constraints of different kinds -both hard and 'soft', the latter in many grades (fuzzy, weighted, and so on).

Definition 3.3 (c-semiring). A c-semiring is a semiring A, +, ×, 0, 1 in which A represents a space of degrees of satisfaction, e.g., the set {0, 1} for yes/no or the interval [0, 1] for intermediate degrees of satisfaction. The operations × and + are used for composition and choice, respectively. Composition is commutative, choice is idempotent and 1 is an absorbing element (i.e., there is no better choice than 1). That is, a csemiring is an algebra of degrees of satisfaction. Notice that every c-semiring S induces a partial order ≤ S (of satisfaction) over A -a ≤ S b iff a + b = b. That is, b is better than a iff the choice between a and b is b. Definition 3.4 (Constraint system). A constraint system is a triple S, D, V where S is a c-semiring, V is a totally ordered set (of configuration variables), and D is a finite set (domain of possible elements taken by the variables).

Definition 3.5 (Constraint).

A constraint over a constraint system S, D, V consists of a selected subset con of V and a mapping def : D |con| → S that assigns a degree of satisfaction to each tuple of values taken by the variables involved in the constraint. Definition 3.6 (External configuration policy). The external configuration policy of a module M consists of:

• A constraint system cs(M ) based on a fixed c-semiring.

• A set sla(M ) of constraints over cs(M ).

• For every variable in cs(M ), a type.

• A partial assignment owner of either a node or an edge of M to each variable of cs(M ).

For instance, in the case of TravelBooking, one could consider the following configuration variables:

• KD and PERC -parameters of CR (customer) that denote the period before departure during which a cancellation is accepted and the percentage of the cost that is refundable in case of cancellation, respectively. • RM1 and RM2 -two different reliable message mechanisms (see [START_REF] Mukhi | Supporting policy-driven behaviors in web services: experiences and issues[END_REF] for examples) that apply to the wires CB, CP and BP (see Figure 7). • BOOKFEE -a parameter of CR (customer) and FA (flight agent) that denotes the fixed fee for each trip/flight booking transaction, respectively.

Because we are handling constraints that involve different degrees of satisfaction, it makes sense that we work with the c-semiring [0, 1], max, min, 0, 1 of soft fuzzy constraints [START_REF] Bistarelli | Semiring-based constraint satisfaction and optimization[END_REF]. In this c-semiring, the preference level is between 0 (worst) and 1 (best). The constraints are:

1. {CR.KD, CR.PERC}, def 1 where def 1 (d, p) = 1 if 1 ≤ d and p ≤ 90 and p ≤ 50 + 50 * d 0 otherwise That is, the percentage PERC of the cost that is refundable is bounded by the least of 90 percent and a linear function of the period KD during which the deal can be revoked (the maximum refundable cost is obtained if the period has 8 or more days). That is, the degree of satisfaction for a flight agent is inversely proportional to the booking fee. 4. {CR.BOOKFEE, FA.BOOKFEE}, def 4 where def 4 (d, p) = 1 if p + 5 ≤ d 0 otherwise That is, the booking fee that the customer has to pay consists of the booking fee of the flight agent plus 5 units for the booking agent service.

As illustrated, we tend to use the dot-notation c.X (resp. w.X) in order to express that component c (resp. wire w) is the owner of the configuration variable X.

The c-semiring approach also supports selection based on a characterisation of 'best solution' supported by multi-dimensional criteria, e.g., minimizing the cost of a resource while maximizing the work it supports. See [START_REF] Fournet | Cc-pi: A constraint-based language for specifying service level agreements[END_REF] for other usages of this approach for service ranking and selection.

The correctness property of service modules

Service modules are considered to be 'correct' when the properties offered in the provides-interface are ensured by the orchestration of its components and the properties specified through its requires-interfaces. For instance, in relation to our running example, we would like to certify that properties offered through the business protocol Customer are effectively established by the orchestration performed by BA on the assumption that PA, HA and FA are bound to services that deliver the properties required in the corresponding business protocols (PayAgent, HotelAgent and FlightAgent, respectively). An example could be that committing to an offer made by BA ensures that the outcome of the payment process will be acknowledged; and another that the period during which a booking can be revoked (negotiated prior to binding) is within certain bounds.

This correctness property of modules is best expressed in terms of logical entailment. The mechanisms that we provide for putting together, interconnecting and composing modules is largely independent of any such logic. The particular choice of logic operators, their semantics and proof-theory are essential for supporting the modelling of service-based applications but not for the semantics and pragmatics of composing modules. For the purpose of this paper, what is important is that the logic satisfies some structural properties that are required for the correctness condition and the notion of module composition to work well together as explained below. Notice that this generic characterisation is also agnostic in relation to the specific techniques through which correctness can be checked. In Srml, we have been investigating the use of model-checking techniques [AMFG09, tBFGM08] in particular.

More specifically, we assume that we have available an entailment system (or π-institution) [Fia04] Sign, gram, . By Sign we denote the category of signatures of the logic, each of which represents a set of interactions; signature morphisms are maps that preserve the structure of interactions (whether they are synchronous or asynchronous, their parameters, and so on). The grammar functor gram : Sign → SET generates, for each signature, the language used for describing properties of the interactions. Notice that, given a signature morphism σ : Q → Q , gram(σ) translates properties in the language of Q to the language of Q .

We denote by Q the entailment system that allows us to reason about properties in the language of Q. We write S Q s to indicate that sentence s is entailed by the set of sentences S. Pairs Q, S consisting of a set S of sentences over a signature Q -usually called theory presentations -can be organised in a category Spec whose morphisms capture what are usually called 'interpretations between theories'. We denote by sign the functor Spec → Sign that projects theory presentations to the underlying signatures. We further assume that Spec is finitely co-complete -i.e., that there is a canonical (minimal) way of amalgamating a diagram of specifications -and coordinated over sign [START_REF] Luiz | Categories for Software Engineering[END_REF] (implying that we can amalgamate mixed diagrams of specifications and signatures).

Business roles, layer protocols, business protocols and interaction protocols carry a semantic meaning that we take to be defined by mappings: spec Brol : Brol → Spec, spec Layp : Layp → Spec, spec Busp : Busp → Spec and spec Iglu : Iglu → Spec, respectively. In the case of business roles, this assumes that we can abstract properties from orchestrations, which corresponds to defining an axiomatic semantics of an orchestration language. In the case of business and interaction protocols, this mapping is more of a translation -24 -spec LAYP :LAYP→SPEC, spec BUSP :BUSP→SPEC and spec INTP :IGLU→SPEC, respectively. In the case of business roles, this assumes that we can abstract properties from orchestrations, which corresponds to defining an axiomatic semantics of an orchestration language. In the case of business and interaction protocols, this mapping is more of a translation from the language of interactions to a logic in which one can reason about their properties as well as that of orchestrations. For simplicity, we shall also denote by sign X the compositions of the functors spec X with sign, which we often simplify to sign if there is no risk of confusion. We summarise the relationships between all these formalisms in Figure 10. To formulate the correctness property of modules using these formalisms, we need to map modules to diagrams in SPEC. In order to define this mapping, we need to be more precise on what we mean by a (binary) connector -an interaction protocol together with attachments to the parties being connected. Every interaction protocol consists of a pair of 'roles' -which act as 'formal parameters' -and a 'glue' that describes the coordination mechanisms enforced by the protocol. Our algebraic semantics identifies every interaction protocol P with a structured co-span [30]: The morphisms π A :roleA P →sign(glue P ) and π B :roleB P →sign(glue P ) identify the interactions involved in the roles of the protocol.

Connectors are triples <µ A ,P,µ B > where:

• P is an interaction protocol <π A ,glue P ,π B >.

• µ A and µ B are 'attachments' -signature morphisms with sources roleA P and roleB P , respectively. from the language of interactions to a logic in which one can reason about their properties as well as that of orchestrations. For simplicity, we shall also denote by sign X the compositions of the functors spec X with sign, which we often simplify to sign if there is no risk of confusion. We summarise the relationships between all these formalisms in Figure 10.

To formulate the correctness property of modules using these formalisms, we need to map modules to diagrams in Spec. In order to define this mapping, we need to be more precise on what we mean by a (binary) connector -an interaction protocol together with attachments to the parties being connected. Definition 3.7 (Interaction protocol). An interaction protocol P is a triple π A , glue P , π B where • glue P : Iglu • π A : roleA P → sign(glue P ) and π B : roleB P → sign(glue P ) are signature morphisms.

The specification glue P -called the 'glue' -describes the coordination mechanisms enforced by the protocol. The signatures roleA P and roleB P -the 'roles' of the protocol -act as formal parameters. The morphisms π A and π B identify the interactions involved in the roles of the protocol. This algebraic semantics identifies every interaction protocol with a structured co-span [START_REF] Luiz | Structured co-spans: An algebra of interaction protocols[END_REF] as depicted in Figure 11.

Definition 3.8 (Connector).

A connector is a triple µ A , P, µ B where:

• P is an interaction protocol π A , glue P , π B .

• µ A and µ B -the 'attachments' -are signature morphisms with sources roleA P and roleB P , respectively.

Using this categorical view of connectors, we can now expand the labelled graph associated with every module to define a proper diagram. This construction needs to take into account three different kinds of edges: those that connect internal components, the provides-interface, and the requires-interfaces. Given a module M , let e : n↔m be an edge such that neither n nor m belongs to requires(M ) and, if M is a service module, neither n nor m is provides(M ). For M to be well typed, it is necessary that the attachments of the connector µ A , P, µ B that labels e are morphisms µ A : roleA P → sign(label M (n)) and µ B : roleB P → sign(label M (m)). As shown in Figure 12, such a connector defines a diagram in Sign.

In the case of a service module M , the connectors that label the wires e i : provides(M )↔m i need to be treated in a special way because the 'customer' is not yet available and, therefore, the corresponding attachments cannot be defined. This is why we choose a default signature that consists of all the interactions that are involved in the protocols. More precisely, if the corresponding connectors label M (e i ) are of the form µ i , P i , µ mi , the signature that represents the (logical) customer is the sum ⊕ j roleA Pj of all the roles, and the attachments are the inclusions roleA Pi → ⊕ j roleA Pj . The reason we take the sum is that this is the biggest set of interactions that the corresponding protocol coordinates. Therefore, for a module to be well typed, we also need that all the attachments to provides(M ) be inclusions roleA Pi → ⊕ j roleA Pj as depicted in Figure 13. On the other hand, although we defined the label of provides(M ) to be a business protocol, that specification represents the properties of the service offered by the module, not the customer with which the wires e i should be connected. Therefore, the signature of label M (provides(M )) should be the sum of the other set of roles ⊕ j roleB Pj , i.e., the properties of the provided service should be written in the language of this signature and not that of the customer. In summary, the signature of the business protocol that labels the provides-interface is not the signature to the wires are attached (which is that of a logical customer) but the sum of the interactions supported by the entities connected to it.

A similar condition applies to the requires-interfaces. More precisely, the signature of the business protocols that label the requires-interface should not require more interactions than the ones involved in the wires that connect them to the body of the module (be it an activity or a service module). Therefore, the signature of a business protocol should be a (disjoint) sum of the roles ⊕ j roleB Pj of the interaction protocols involved in the connections as depicted in Figure 14. Definition 3.9 (Well-typed module). We say that a module M is well typed iff:

• If M is a service module, let e i : provides(M )↔m i be all the edges (wires) that connect the node provides(M ) and µ i , P i , µ mi the corresponding labels (connectors). The signature of the business protocol label M (provides(M )) is (isomorphic to) the sum ⊕ j roleB Pj and µ i : roleA Pi → ⊕ j roleA Pj for every attachment. • For every R∈requires(M ), let e i : m i ↔R be all the edges (wires) that connect R and µ i , P i , µ mi the corresponding labels (connectors). The signature of the business protocol label M (R) is (isomorphic to) the sum ⊕ j roleB Pj and we have µ mi : roleA Pi → ⊕ j roleA Pj for every attachment. • For every other edge e : n↔m let µ A , P, µ B be its label. In this case, we have µ A : roleA P → sign(label M (n)) and µ B : roleB P → sign(label M (m)).

Proposition and Definition 3.1 (expanded(M )). Given a module M that is well typed, we construct another labelled graph expanded(M ) as follows:

glue P n π B n π A n roleA P n roleB P n π B 1 roleA P 1 roleB P 1 glue P 1 π A 1 roleB P n roleB P 1 ⊕ sign(label M (m 1 )) sign(label M (m n ))
trigR1 intC1 SLA_M q 1 q 5 q 3 q 2 b 0 roleB P 0 π A 1 π B 1 b 1 a 1 roleA P 1 roleB P 1 spec glue P 1 spec BR_C1 π A 2 a 2 roleA P 2 spec glue P 2 spec LP1 specB(M) π B 2 b 2 roleB P 2 spec BP_R1 q 4
Fig. 15. Example of expanded(M ) -inside the dashed line -and its colimit. We also indicate grey) the morphism that connects the signature of the provides-interface to the expanded diagram

• We remove the provides-interface and all the edges that connect it.

• For every edge (wire) of M that remains, we replace it by the diagram defined by its connector as in Figure 12, which adds three new nodes (for the glue and roles) and four directed edges.

An example is given in Figure 15.

Proposition and Definition 3.2 (specA(M )). Given a module M that is well typed, if we apply the mapping spec to the business roles (of the component interfaces), the layer protocols (of the serves-and uses-interfaces), the glues of the interaction protocols, and the business protocols (of the requires-interfaces) of expanded(M ), we obtain a diagram in the (coordinated) category Spec. The colimit (amalgamated sum) of this diagram returns a specification specA(M ) and, for every node n of expanded(M ), a morphism q n : sign(label M (n)) → sign(specA(M )).

Definition 3.10 (specB(M )). Given a module M that is well typed, we define the specification specB(M ) that results from adding to specA(M ) the properties that derive from the internal configuration policy, which include the initialisation and termination constraints as well as the triggers associated with the requiresinterfaces of M. As for the business protocol of provides(M ), we have already defined its signature as being the sum ⊕ j roleB Pj of the roles of the connectors that label the wires e i : provides(M )↔m i .

Proposition and Definition 3.3 (specP (M )). The attachments µ mi : roleB Pi → sign(label M (m i )) composed with the morphisms q mi : sign(labelM (m i )) → sign(specB(M )) extend to a morphism ⊕ j roleB Pj → sign(specB(M )) (see Figure 13 and Figure 16). We denote by specP (M ) the translation of the specification of the business protocol of provides(M ) induced by that morphism.

Proof. The result follows from the universal properties of the sum.

Given that all these sets of sentences are now in the language of specB(M ), we can define a correctness property for service modules. Definition 3.11 (Correctness). We say that a service module M is correct iff specB(M ) specP (M ).

That is, a module is correct iff the properties of the provides-interface are entailed by the module assuming that the properties of the requires-interfaces and their connectors hold.

Naturally, another important property is consistency, i.e. that specB(M ) is free from contradictions (or, equivalently, that it admits a model). Given that the specifications involved in the colimit are generated by the mappings spec applied to business roles, business protocols, layer protocols and interaction protocols, ensuring their consistency should not be difficult. Consistency of the whole module depends, essentially, on the nature of the connections established by the wires. To state the obvious, specific strategies for ensuring consistency will depend on the nature of the particular formalisms involved. Examples of formal techniques that can be used for this purpose are [BBC + 06, CHY07, VCS08]. See also [START_REF] Luiz Fiadeiro | A formal model for service-oriented interactions[END_REF] for a discussion on consistency for the specific computational and coordination models developed for Srml.

The Operational Semantics of Service Discovery and Binding

Unification: discovery, ranking and selection

As mentioned in Section 3.2, every module declares, as part of its internal configuration policy, a triggering condition for each requires-interface. This is the condition that determines when a service needs to be discovered and bound to the current configuration through that interface. More precisely, given a business configuration BC = G, S , B, C and an activity a, each condition trigger(R) where R∈requires(B(a)) is evaluated over the state S. If the condition trigger(R) for a given requires-interface R holds in BC, the 'unification' process is launched, which should return a service that 'best' fits the business protocol label B(a) (R), the interaction protocols of the wires that connect the requires-interface to the rest of the module, and the external configuration policy of B(a).

In our setting, this unification process involves three steps, outlined as follows:

• Discovery. This step consists in finding the services -among those that are able to guarantee the properties of the business protocol label B(a) (R) associated with R and of the interaction protocols that label the wires that connect R -with which it is possible to reach a service-level agreement. • Ranking. For each service M discovered in the previous step, we calculate the most favourable servicelevel agreement that can be achieved -the contract that will be established between the two parties if M is selected. This calculation uses a notion of satisfaction that takes into account the preferences of the activity a and the service M . • Selection. One of the services that maximises the level of satisfaction offered by the corresponding contract is selected.

We are now going to define each of these steps in more detail.

Proposition and Definition 4.1 (Discovery). Consider a business configuration BC = F, B, C and let R be a requires-interface of a business activity a such that trigger(R) holds in F. The discovery phase returns pairs M, ρ where M is a service module and ρ is a mapping satisfying the properties below. Let P R be the provides-interface of M, i.e., P R = provides(M ).

• For every wire w : s↔R of a, there is a non-empty set ρ(w) of wires of M of the form P R↔q (the set of wires that unify with w). For every wire v : P R↔q of M there is w : s↔R of a such that v∈ρ(w), i.e., each wire on the side of the provides-interface unifies with at least one wire on the requires-interface side. • Let ⊕ρ(w) be the sum of the interaction protocols of the wires in ρ(w) as co-spans, and π A , glue P , π B the interaction protocol of w. The mapping ρ defines a morphism π A , glue P , π B → ⊕ρ(w) of co-spans, i.e., a morphism in Iglu between glue P and the sum of the glues of the interaction protocols of the wires in ρ(w) and signature morphisms between the roles that commute with the morphism of glues. • The collection of signature morphisms of the form roleB P → ⊕ v∈ρ(w) roleB v for all wires that connect R extends to a morphism label B(a) (R) → label M (P R) of specifications, i.e., the behavioural properties offered by the provides-interface of M entail the properties required by the requires-interface of the activity up to a suitable translation between the languages of both. • The constraint system cs(M ) of the external policy of M is compatible with that of cs(B(a)). This means that the mapping ρ is such that, for every variable v ∈ cs(B(a)):

if owner(v) = R, there exists ρ(v) in cs such that type(v) = type (ρ(v)) and owner (ρ(v)) = P R; if owner(v) is a wire w : s↔R then, for every w ∈ ρ(w) there is a variable ρ(v, w ) in cs(M ) s.t. owner (ρ(v, w )) = w and type(v) = type (ρ(v, w )).

• The combination sla(B(a)) ⊕ R,ρ sla(M ) of the sets of constraints of B(a) and M is consistent (as defined below, in Definition 4.1).

Intuitively, compatibility means that each discovered service needs to support the negotiation of the configuration parameters associated with R, i.e., those configuration parameters that belong to R or to the wires that connect R to the components of the activity module. The last condition ensures that it is indeed possible to achieve a service-level agreement between the activity and the service module. Compatibility of the constraint systems of B(a) and M relative to R ensures that they can be combined, which gives rise to another constraint system.

Definition 4.1 (Combined constraint system). The combined constraint system cs(B(a)) ⊕ R,ρ cs(M ) is defined as follows:

• Its domain D" is the union D ∪ D of the domains of cs(B(a)) and cs(M ).

• Its set of variables V is the disjoint union of cs(B(a)) and cs(M ) except that each pair of variables of the form v, ρ(v) or v, ρ(v, w ) gives rise to a single variable denoted v|ρ(v) or v|ρ(v, w ), respectively -the variable involved in the negotiation. Notice that, if owner(v) is a wire w : i↔R, then we may end up with several 'aliases' v|ρ(v, w ), one for each wire w ∈ ρ(w), i.e., that ρ pairs with w. We denote by neg(R, ρ) the set of such variables. The combined set of constraints is defined by 'lifting' the constraints of sla(B(a)) and sla(M ) to the new constraint system, for which two aspects need to be accounted for. On the one hand, we have to take into account that variables may have multiple aliases, which requires constraints to be replicated (one for each alias). On the other hand, we have to account for the fact that constraints lifted from any of the modules involve variables from the other module; in such cases, we define that the degree of satisfaction of any tuple assigning new domain elements to old variables is 0. Formally, the lifting operates as follows: Definition 4.2 (Combined set of constraints). The combined set of constraints sla(B(a)) ⊕ R,ρ sla(M ) is defined by:

• Lifting every constraint con, def over cs(B(a)) as follows:

-If con does not involve any variable being negotiated (i.e., neg(R, ρ)) we lift the constraint to con, def " where def " coincides with def on D |con| and assigns the value 0 elsewhere. -For every v∈con that belongs to neg(R, ρ) and alias v|v , we lift the constraint to con", def " where con" is obtained from con by replacing each such variable by the chosen alias, and def " coincides with def on D |con| and assigns the value 0 elsewhere.

• Performing the same lifting on the constraints of cs(M ).

It remains to discuss what we mean by consistency of the combined set of constraints.

Definition 4.3 (Consistency of a set of constraints). The consistency of a set of constraints is defined in terms of the notion best level of consistency, which assigns an element of the c-semiring to every set of constraints C as follows (for more details see [START_REF] Bistarelli | Semiring-based constraint satisfaction and optimization[END_REF]):

blevel(C) = t c∈C def c (t ↓ con(c))
Intuitively, this notion gives us the degree of satisfaction that we can expect for the set of constraints of a given problem. A set of constraints C is said to be consistent iff blevel(C) > S 0.

In order to illustrate these constructions (see Figure 18), consider the business activity A ANT0 (see also in Figure 8). Consider that, at a certain point of the corresponding workflow, the condition trigTA becomes true and triggers the unification process for TA. For the service module TravelBooking (see Figure 7) to be discovered, we would need to

• Establish a specification morphism between TravelAgent (the business protocol that types TA) and Customer (the business protocol that types the provides interface CR of TravelBooking) showing that the properties required in TravelAgent are entailed by those of Customer.

• Check that the constraint systems of A ANT0 and TravelBooking are compatible.

Entailment is handled through the logic that is adopted for Spec as discussed in Section 3.3. In order to illustrate what we mean by compatibility, suppose that the constraints imposed by the external policy SLA ANT0 involve uniquely the variables TA.PERC, TA.KD, AT.RM1, and require that:

• The reliable messaging mechanism RM1 should be used in the conversations with TA over the wire AT -a hard constraint. • The degree of satisfaction associated with a refund p and a period for revoking of duration d is given by p/(d * 100) -a soft constraint.

In this situation, it is easy to check compatibility. The constraint system of TravelBooking includes the variables CR.PERC, CR.KD, CB.RM1, CP.RM1 and, hence, their values can be negotiated establishing the pairs TA.PERC|CR.PERC, TA.KD|CR.KD, AT.RM1|CB.RM1, AT.RM1|CP.RM1. Notice that AT.RM1 has two aliases because CR is linked by two wires CB and CP. This implies that the constraint (1) over AT.RM1 is lifted to two constraints: one over AT.RM1|CB.RM1 and the other over AT.RM1|CP.RM1. That is, in the combined system, CB and CP have to use the reliable messaging mechanism RM1. Indeed, it is not difficult to conclude that no inconsistencies arise when we combine the two sets of constraints. For instance, the level of satisfaction associated with a situation in which TA.PERC|CR.PERC=55, TA.KD|CR.KD=1, AT.RM1|CB.RM1=1, AT.RM1|CP.RM1=1 would be 0.55; this would be a possible service-level agreement if TravelBooking were to be selected to be bound to the business activity A ANT0.

Finally, we can discuss how contracts are established.

Proposition and Definition 4.2 (Ranking). Together with the set neg(R, ρ) of the variables being negotiated (those in the domain of ρ), the set of constraints sla(B(a)) ⊕ R,ρ sla(M ) defines a constraint problem. The solution of this constraint problem is again a constraint and, hence, it assigns a degree of satisfaction to each possible tuple of values for the variables in neg(R, ρ). The outcome of the negotiation between the business activity a and the provider of M is any tuple whose associated degree of satisfaction is blevel(sla(B(a)) ⊕ R,ρ sla(M )), which is again a constraint. That is, a service level agreement is simply an assignment of values to the configuration parameters in neg(R, ρ). Hence, ranking a discovered service M in our framework consists in finding an assignment that maximizes the degree of satisfaction. We denote by contract(B(a) ⊕ R,ρ M ) the constraint that results from the negotiation.

In our example, there are other assignments of values to TA.PERC|CR.PERC and TA.KD|CR.KD that return a positive degree of satisfaction: for instance, 60 and 6 return 0.1. However, the previous assignment maximizes this value, which is why it represents a possible service level agreement between conf and the provider of the TravelBooking service. Definition 4.4 (Selection). Selection consists in choosing one service from the set of discovered services, taking into account its ranking -the degree of satisfaction assigned to the outcome of the negotiation. The selected service is one with maximal rank.

In our example, the value 0.55 would have to be compared with the outcome of the negotiation of A ANT0 17 with other discovered travel agency services. If all the other outcomes were worse than 0.55, TravelBooking would be the selected service.

The reconfiguration step

It remains to define the new business configuration that results from the process of discovery, ranking and selection -what we call the 'reconfiguration step'. This includes the new state configuration that results from instantiating the selected service over the current configuration and binding it to the business activity a that triggered the process, and the typing of the business activity with a new module. We start by defining the activity module that will type a in the new business configuration.

Proposition and Definition 4.3 (Composition of modules). Consider a service module M returned by the selection process upon the occurrence of trigger(R) where R is a requires-interface of B(a). The binding of R with an instance of M involves the assembly of modules B(a) and M , giving rise to a new module that corresponds to the new execution plan of a. This new module is the composition B(a) ⊕ R,ρ M defined as follows:

The graph and its labelling The graph of B(a) ⊕ R,ρ M is obtained from the sum (disjoint union) of the graphs of B(a) and M by eliminating the nodes R and provides(M ) and the edges that connect them, and adding an edge i↔j between any two nodes i and j such that w : i↔R is an edge of B(a) and provides(M )↔j ∈ ρ(w). The requires-interfaces are those of B(a), except for R, and those of M . Given that provides(M ) has been eliminated, there are no provides-interfaces; we obtain an activity module B that defines the new workflow of the activity a.

The labels of the resulting graph are inherited from the graphs of B(a) and M , except for the new edges i↔j that result from the binding of R and provides(M ) through the mapping ρ. These are calculated by composing the connectors that label w : i↔R and each provides(M )↔j ∈ ρ(w). This process of composition works as depicted in Figure 19: basically, we take the glue to be the sum ⊕ρ(w) and the roles of i↔R and provides(M )↔j. This process is repeated for every pair of wires that are connected through the mapping ρ. The external configuration policy This is given by the combined constraint system cs(B(a))⊕ R,ρ cs(M ) and the constraints of the sum sla(B(a))⊕ R,ρ sla(M ) together with contract(B(a)⊕ R,ρ M ) -the result of the negotiation as defined in Section 4.1. Owners and types are inherited except for the pairs of variables involved in the negotiation (which no longer require an owner). The internal configuration policy Triggers, initialisation and termination conditions are all inherited from B(a) and M .

We take this module to provide the reconfigured workflow of the business activity a. Notice that the composition of the wires involves only the glues of the protocols, not the components. In [Fia04, WLF01], we have shown how such forms of composition can be supported in CommUnity -an architectural description language. See also [START_REF] Bliudze | The algebra of connectors -structuring interaction in BIP[END_REF] for an algebraic formalisation of connector composition in the Behaviour-Interaction-Priority (BIP) component framework.

We can now define the new state and business configurations that result from the discovery and binding processes.

Definition 4.5 (The reconfigured state configuration). The current state configuration is modified as follows:

• New components (nodes) are added (to the service layer), which are typed by the business roles of components(M ). • New wires (edges) are added that are typed with the connectors that link together the new components introduced in the previous step. • New wires are added between the new components and the ones that were already present in the configuration, which are typed by the composed connectors that result from the bindings. • New wires are added that bind the new service components to components (of the bottom layer) that are typed by the layer protocols of uses(M ). Notice that we do not create new components (instances) in the bottom layer. • The new components and wires are chosen such that the negotiated conditions on configuration variables are enforced, and initialised so as to satisfy the internal configuration policy of M .

The state of components and wires not affected by the reconfiguration can also change during a reconfiguration step as a result of the computations that they execute. Notice how this operational semantics differentiates between the different kinds of nodes and their specifications that we introduced in Sections 2.3 and 3.1. The difference between business roles and protocols is that components that correspond to the business roles are created and bound to their interfaces when the module is instantiated (i.e., when a new session of the service is initiated) whereas the external services that correspond to the business protocols are bound to the require interfaces at run time after a process of discovery, ranking and selection triggered according to the internal configuration policy of the module. The difference with respect to layer protocols is that these bind to components of the bottom layer that persist independently of the activities performed at the service layer, whereas business roles bind to components that are added to the service layer and have no persistency beyond the session in which they are created. Hence, in the case of the TravelBooking service, a new instance of BookingAgent is generated for each new session whereas all sessions will share the same component that binds to DB (i.e., they all share the same database of users).

The new business configuration is now easy to define:

Definition 4.6 (The reconfigured business configuration). In the new business configuration, the type mapping B is the same as B except for the activity a for which the activity module (type) B (a) is B(a)⊕ R,ρ M . The homomorphism is as defined by the typing of nodes and wires discussed above.

An example of such a reconfiguration step can be given by the transition between the configurations in Figure 8 and Figure 9. As another example, the module that results from the composition indicated in Figure 18 is the one on Figure 9. This figure also illustrates the state reconfiguration step (relative to Figure 8). Notice how the component DB of the bottom layer becomes shared between the two activities ANT and LAU. The new external configuration policy is the one discussed in Section 4.1.

Related Approaches

One of the main aspects that distinguish the approach that we proposed above from other work on Web Services (e.g., [START_REF] Alonso | Web Services -Concepts, Architectures and Applications[END_REF]) and SOC in general (e.g., [START_REF] Osoa | Service component architecture: Building systems using a service oriented architecture[END_REF]) is that we address not the middleware architectural layers (or low-level design issues in general), but what we call the 'business level'. For instance, the main concern of the Service Component Architecture (SCA) [START_REF] Osoa | Service component architecture: Building systems using a service oriented architecture[END_REF], from which we have borrowed concepts and notations (as discussed in more detail in Section 3), is to provide an open specification "allowing multiple vendors to implement support for SCA in their development tools and runtimes". This is why SCA offers a middleware-independent layer for service composition and specific support for a variety of component implementation and interface types (e.g., BPEL processes with WSDL interfaces, or Java classes with corresponding interfaces). Our work explores a complementary direction: our research aims for a modelling framework supported by a mathematical semantics in which business activities and services can be defined in a way that is independent of the languages and technologies used for programming and deploying the components that will execute them. The fact that the modelling framework is equipped with a formal semantics makes it possible to support the analysis of services, service compositions and activities, a direction that we are pursuing through the use of model-checking [START_REF] Abreu | A model-checking approach for service component architectures[END_REF].

Another architectural approach to SOC has been designed [ABvH + 06] that follows SCA very closely. However, its purpose is to offer a meta-model that covers service-oriented modelling aspects such as interfaces, wires, processes and data. Therefore, as in SCA, interfaces are syntactic and bindings are established at design time, whereas our interfaces are behavioural and binding occurs at run time. Other approaches to service modelling have considered richer interfaces that encompass business protocols, e.g., [BCT04, BSBM04, DD04, Rei05, Rei08], but not the dynamic aspects.

Indeed, a characteristic that distinguishes our approach from other formal models of services such as [START_REF] Broy | A formal model of services[END_REF] is the fact that we address the dynamic aspects of SOC, namely run-time discovery and binding. Formalisms for modelling (web) services tend not to address these. For example, in BPEL, service compositions are created statically and are governed by a centralised engine. This also holds for approaches that focus on choreography (e.g., [START_REF] Carbone | Structured communication-centred programming for web services[END_REF][START_REF] Reisig | Modeling-and analysis techniques for web services and business processes[END_REF]), where it is possible to calculate which are the partners that can properly interact with a service, but the actual discovery and binding processes are not considered. Exceptions can be found among some of the process calculi that have been developed for capturing semantic foundations of SOC (e.g., [BBC + 06, BM07, LPT07]). However, such process calculi tend not to address dynamic reconfiguration separately from computation, i.e., the process of discovery and binding is handled as part of the computation performed by a service. As far as we know, Srml is the first service-modelling language to separate these two concerns.

Indeed, in our opinion, what makes SOC different from other paradigms is the fact that it concerns runtime, not design-time complexity. This is also the view exposed in [Elf07] -a very clear account of what distinguishes SOC from CBD (Component Based Development). For instance, starting from a universe of (software) components as structural entities, [BKM07] views a service as a way of orchestrating interactions among a subset of components in order to obtain some required functionality -services coordinate the interplay of components to accomplish specific tasks. Whereas in CBD component selection is either performed at design time or programmed over a fixed universe of components, SOC provides a means of obtaining functionalities by orchestrating interactions among components that are procured at run time according to given (functional) types and service level constraints.

Another area related to the work that we have presented concerns the non-functional aspects of services, namely the policies and constraints for service level agreement that have to be taken into account in the composition of services. Most of the research developed in this area has been devoted to languages for modelling specific kinds of policies (over specific non-functional features) and of selection algorithms, e.g., SCA Policy [START_REF] Osoa | Service component architecture: Building systems using a service oriented architecture[END_REF] and several others [MDSR07, MP04, MPR + 08, YL05, ea04]. These languages have been primarily designed to be part of the technology available for implementing and executing services. As such, they are tailored to the technological infrastructure that is currently enabling web services and are not appropriate for being used at high-levels of business modelling.

Concluding Remarks and Further Work

In this paper, we presented an abstract semantics of discovery and binding in service overlay computers. This is part of an effort that we started pursuing within the Sensoria project towards a methodological and mathematical characterisation of the service-oriented computing paradigm [WHar]. The formal model that we presented is being used to provide a mathematical semantics for Srml -the Sensoria Modelling Reference Language -on the basis of which we are defining an engineering environment that includes abstraction mappings from workflow languages (such as BPEL [START_REF] Bocchi | From BPEL to SRML: A formal transformational approach[END_REF]) and policy languages (such as StPowla [START_REF] Bocchi | Engineering service oriented applications: From StPowla processes to SRML models[END_REF]), and model-checking techniques that support qualitative analysis [START_REF] Abreu | A model-checking approach for service component architectures[END_REF].

Section 2 of this paper outlined methodological implications of service engineering, namely the difference between activity and service modelling, and the use of standard business protocols to facilitate service publication and delivery. A more complete account of the software engineering methodology and associated tools developed within Sensoria for service-oriented systems can be found in [WHar]. This includes research on how elements of the UML can be specialised for supporting SOAs in general, and Srml in particular [START_REF] Bocchi | A use-case driven approach to formal service-oriented modelling[END_REF], as well as re-engineering and model-driven development techniques.

The operational model that we proposed is based on algebraic, graph-based techniques [START_REF] Luiz Fiadeiro | Algebraic semantics of service component modules[END_REF][START_REF] Luiz | Structured co-spans: An algebra of interaction protocols[END_REF].

The notion of configuration and module were formalised in terms of graphs and their labelling with different kinds of components, connectors, specifications and specification morphisms. In this context, another interesting semantics of the reconfiguration process that we would like to explore is the use of graph transformations, for instance as in [START_REF] Bruni | Service oriented architectural design[END_REF] where the architectural style of Srml is defined.

A novel aspect of our configuration model is the way the operational semantics induces three layers that reflect different levels of change: what we called the middle or 'service' layer is the one that is reconfigured as a result of discovery and binding; the top layer contains components that interface with external users and launch business activities by adding new workflows to the middle layer; the bottom layer contains components that are shared by all the services executing in the middle layer and persist beyond their execution. The layers are not formally part of the architecture but help to understand the overall dynamics of the configuration of global computers and the notion of service overlay. In a sense, the bottom layer offers 'services' in the more standard terminology offered by component-based development (CBD) (e.g., [START_REF] Broy | A formal model of services[END_REF]). From our point of view, SOC deals with run-time, not design-time complexity, which is precisely what the middle layer intends to provide.

Discovery and selection at the service layer do not need to be programmed, but are provided by the underlying middleware, which is why they are reflected in the operational semantics defined in Section 4.1. Note that these activities operate over a set of services that is itself dynamically changing as service producers revise their portfolios. This added flexibility comes at a price -dynamic interactions have the overhead of selecting the co-party at each invocation -which means that the choice between invoking a service and calling a component needs to be carefully justified. This is why Srml makes a provision for both types of interaction (through requires and uses interfaces as discussed in Section 3), which is another feature that is unique to Srml.

A core aspect of our mathematical model is reflection as formalised in Section 2.3: business configurations superpose a typing mechanism over state configurations that identifies subsystems that execute according to given business activities and adds the corresponding types to the configuration itself. In a sense, our model provides an abstract virtual machine that captures the essence of SOC as a 'business overlay computer' in the sense that it abstracts away from the middleware resources e.g., the service broker and the specific platforms in which service components execute. As future work, we would like to investigate how this notion of service overlay can be implemented in reflective middleware [CBG + 08].

Another interesting aspect that we propose to investigate is the 'interleaving' of the discovery and binding process with the execution of the activity whose workflow is being reconfigured. Having offered separate models for these two processes (the latter reported in [START_REF] Luiz Fiadeiro | A formal model for service-oriented interactions[END_REF]), we intend to investigate how the reconfiguration process can be analysed in conjunction with the computations that are being performed by components and the coordination mechanisms on the interactions performed by the wires. Another avenue that we would like to explore in this respect is the use of graphs as a computational model, for instance as in [FHL + 05].

Fig. 1 .

 1 Fig. 1. Overall engineering architecture and processes

Fig. 2 .

 2 Fig. 2. The graph of a state configuration with 12 components and 13 wires decorated with the iconography of Srml (summarised in the Appendix)

Fig. 3 .

 3 Fig. 3. The sub-configurations corresponding to two business activities

Fig. 4 .

 4 Fig. 4. An activity module

Fig. 5 .

 5 Fig. 5. An activity module with a requires-interface

Fig. 6 .

 6 Fig. 6. The sub-configuration and type of the activity ANT executing in a given state configuration

Fig. 7 .

 7 Fig. 7. The structure of a module defining the booking service of a travel agency

Fig. 8 .

 8 Fig. 8. AUI adds the component Ant to the service layer, typed with FunTrav

Fig. 9 .

 9 Fig. 9. A new session of TravelBooking starts and reconfigures the workflow of ANT

  2. {CB.RM1, CB.RM2, CP.RM1, CP.RM2, BP.RM1, BP.RM2}, def 2 where def 2 (a, b, c, d, e, f ) = 1 if a = c = e = 1 and b = d = f = 0 1 if a = c = e = 0 and b = d = f = 1 0 otherwise That is, the booking agent can use exactly one of the two reliable messaging mechanisms in the conversations with the customer and the pay agent and the same mechanism has to be used with all of them. 3. {FA.BOOKFEE}, def 3 where def 3 (p) = 1 1+p

Figure 10 :

 10 Figure 10: Relating the specification domain with the other formal domains

Figure 11 :

 11 Figure 11: Interaction protocols as structured co-spans

Fig. 10 .

 10 Fig. 10. Relating the specification domain with the other formal domains

Fig. 13 .

 13 Fig. 13. The types of the wires connecting the provides-interface

Fig. 14 .

 14 Fig. 14. The types of the wires connecting a requires-interface

Fig. 16 .

 16 Fig. 16. How the signature of the business protocol of the provides-interface maps to sign(specB(M )) for a generic M

Fig. 18 .

 18 Fig. 17. Unifying wires

Fig. 19 .

 19 Fig.19. The wires that result from Figure17

Acknowledgments

We would like to thank our colleagues in the Sensoria project for many useful discussions on the topics covered in this paper (especially Emilio Tuosto for direct feedback on earlier versions), and Luís Andrade (ATX Software) in particular for his insights and suggestions on the layered approach that we proposed in the paper. We also received very useful feedback from reviewers of earlier versions of the paper. Finally, throughout the time that it took us to write and rewrite the paper, João Abreu raised many important questions on fundamental aspects of the model, which have been decisive for the version that we ended up presenting.