Current Web service choreography proposals, such as BPEL4WS, BPSS, WSFL, WSCDL or WSCI, provide notations for describing the message flows in Web service collaborations. However, such proposals remain at the descriptive level, without providing any kind of reasoning mechanisms or tool support for checking the compatibility of Web services based on the proposed notations. In this paper we present the formalization of one of these Web service choreography proposals (WSCI), and discuss the benefits that can be obtained by such formalization. In particular, we show how to check whether two or more Web services are compatible to interoperate or not, and, if not, whether the specification of adaptors that mediate between them can be automatically generated ---hence enabling the communication of (a priori) incompatible Web services.

A common feature of ambient intelligence is that many objects are inter-connected and act in unison, which is also a challenge in the Internet of Things. There has been a shift in research towards integrating both concepts, considering the Internet of Things as representing the future of computing and communications. However, the efficient combination and management of heterogeneous things or devices in the ambient intelligence domain is still a tedious task, and it presents crucial challenges. Therefore, to appropriately manage the inter-connection of diverse devices in these systems requires: (1) specifying and efficiently implementing the devices (e.g., as services); (2) handling and verifying their heterogeneity and composition; and (3) standardizing and managing their data, so as to tackle large numbers of systems together, avoiding standalone applications on local servers. To overcome these challenges, this paper proposes a platform to manage the integration and behavior-aware orchestration of heterogeneous devices as services, stored and accessed via the cloud, with the following contributions: (i) we describe a lightweight model to specify the behavior of devices, to determine the order of the sequence of exchanged messages during the composition of devices; (ii) we define a common architecture using a service-oriented standard environment, to integrate heterogeneous devices by means of their interfaces, via a gateway, and to orchestrate them according to their behavior; (iii) we design a framework based on cloud computing technology, connecting the gateway in charge of acquiring the data from the devices with a cloud platform, to remotely access and monitor the data at run-time and react to emergency situations; and (iv) we implement and generate a novel cloud-based IoT platform of behavior-aware devices as services for ambient intelligence systems, validating the whole approach in real scenarios related to a specific ambient assisted living application.

Adaptation is of utmost importance in systems developed by assembling reusable software services accessed through their public interfaces. This process aims at solving, as automatically as possible, mismatch cases which may be given at the different interoperability levels among interfaces by synthesizing a mediating adaptor. In this paper, we present a toolbox that fully supports the adaptation process, including: (i) different methods to construct adaptation contracts involving several services; (ii) simulation and verification techniques which help to identify and correct erroneous behaviours or deadlocking executions; and (iii) techniques for the generation of centralized or distributed adaptor protocols based on the aforementioned contracts. Our toolbox relates our models with implementation platforms, starting with the automatic extraction of behavioural models from existing interface descriptions, until the final adaptor implementation is generated for the target platform.