In this paper, we present a playful digital activity for primary school classrooms that promotes sustainable and active mobility by leveraging the daily journey to school into a collaborative educational experience. In the class game, stretches of distance travelled in a sustainable way by each child contributes to the advancement of the whole school on a collective virtual trip. During the trip, several virtual stops are associated with the discovery of playful learning material. The approach has been evaluated in a primary school with 87 pupils and 6 teachers actively involved in the learning activity for 12 continuous weeks. The findings from the questionnaires with parents and the interviews with teachers show a positive effect in terms of children's behavioural change as well as educational value. Indications on the use of class and school collaborative gamification activities for supporting sustainable behavioural change are discussed.

A key challenge posed by the Internet of Services is that applications need to cope with a continuously changing environment, both in terms of the context in which they operate and of the services, users and providers involved. Differently from applications where traditional change detection and adaptation mechanisms can be used, the Internet of Services requires systems that are adaptive by design. In this paper we present a design for adaptation framework supporting the modeling, development and operation of service based applications operating in highly dynamic environments. The approach exploits advanced techniques for dynamic and incremental service composition, allowing to effectively deal with changes occurring at different levels in the system. An implementation of the proposed solution is presented and evaluated on a real-world scenario from the Smart Urban Mobility domain.

The idea to build systems based on services, by reusing and combining software made available independently via different technologies and channels and dynamically organizing them into coherent processes, has a very well recognized potential. Achieving this potential stands crucially on the ability to recognize and exploit the context in which such applications operate, in terms of the available services, of the actual setup at run-time, and of the interaction with human actors. Changing contexts require run-time reaction, by adapting the ongoing overall process enacted by the service-based system to unexpected deviations. Continuous context-aware adaptation is hencefore a strong requirement in this setting. In this paper, we propose a service delivery platform designed for the continuous context-aware adaptation of service-based systems, based on the idea of monitoring the underlying context via a hierarchical model, and using the context to drive the choice and execution of adaptive pervasive flows. We describe the approach through an example from the smart cities e-mobility domain.

Data-flow requirements is an important aspect of service composition. Although several approaches have been proposed to specify data-flow requirements, they cannot be efficiently exploited in dynamic setting, for example, where the composition participants (i.e., component services) need to be dynamically replaced. In this paper, we propose a new modeling methodology for data-flow requirements, in which we explicitly distinguish a data model of a composite service from data models of component services. We show that following our methodology, a composition can be adjusted to various dynamic changes with significantly less effort. We implement our solution using planning techniques and make its basic evaluation on a scenario from the travel domain.

We propose a comprehensive framework for adaptivity of service-based applications, which exploits the concept of process fragments as a way to model reusable process knowledge and to allow for the dynamic, incremental, context-aware composition of such fragments into adaptable service-based applications. The framework provides a set of adaptation mechanisms that, combined through adaptation strategies, are able to solve complex adaptation problems. An implementation of the proposed solution is presented and evaluated on a real world scenario from the logistics domain.

Adaptivity is a key feature of service-based systems to fully exploit the advantages offered by the service paradigm. In this paper we present a comprehensive framework that can be used to define and support highly adaptable context-aware service-based business processes. In our approach, all the adaptation-related tasks, from detecting an adaptation problem to finding a solution and applying it to a running process instance, are performed automatically at run time. We also show how the framework has been implemented and applied to a real-world scenario from the logistics domain.

A critical aspect for pervasive computing is the possibility to discover and use process knowledge at run time depending on the specific context. This can be achieved by using an underlying service-based application and exploiting its features in terms of dynamic service discovery, selection, and composition. Pervasive process fragments represent a service-based tool that allows to model incomplete and contextual knowledge. We provide a solution to automatically compose such fragments into complete processes, according to a specific context and specific goals. We compute the solution by encoding process knowledge, domain knowledge and goals into an AI planning problem. We evaluate our approach on different scenarios stress testing the main characteristics of pervasive process fragments.

Adaptation of service-based applications (SBA) is not trivial in their heterogeneous and dynamic execution context. While different approaches exist, most of them focus on a specific part of the SBA ignoring the overall impact of the adaptation on the whole application. In this paper we propose a cross-layer adaptation manager (CLAM) that tackles this problem.

Service-oriented systems have attracted great interest from industry and research communities worldwide. Service integrators, developers, and providers are collaborating to address the various challenges in the field. PESOS 2010 is a forum for all these communities to present and discuss a wide range of topics related to service-oriented systems. The goal of PESOS was to bring together researchers from academia and industry, as well as practitioners working in the areas of software engineering and service-oriented systems to discuss research challenges, recent developments, novel applications, as well as methods, techniques, experiences, and tools to support the engineering and use of service-oriented systems.

In the literature, there exist several approaches for monitoring the execution of BPEL processes. They concentrate on different properties, adopt different languages, work at different levels of abstraction, and assume different perspectives. Even if the field is rather new, we do not think that this diversity is a limitation of current solutions; rather it is intrinsic in the problem itself. We claim that, instead of working on the definition of the ultimate approach for BPEL monitoring, we should push a cooperative approach based on the integration of different solutions.In this paper, we present a first step in this direction, and describe a monitoring framework which is obtained by integrating two well-known approaches, namely Dynamo and Astro. This integration, which happens both for the language used for expressing the properties to be monitored, and for the architecture of the monitoring framework, allows to combine the advantages of the two approaches and to obtain a general, comprehensive solutions for BPEL monitoring.

Automated composition of services is a key functionality for the adoption of the service-oriented development paradigm. Solving this problem in practice requires the ability to consider asynchronous stateful services and to express complex composition requirements which may span different phases of the life-cycle of component services. In this paper we present a novel automated service composition approach which addresses these challenges by associating so-called 'objects' to services, and by introducing a simple yet powerful notation to express composition requirements on them. We recast this view of the problem as a specific form of planning; our experiments on a prototype implementation witness the ability of our approach to deal with realistic scenarios and requirements that cannot be tackled by other current approaches.

Thanks to recent advances, AI Planning has become the underlying technique for several applications. Figuring prominently among these is automated Web Service Composition (WSC) at the "capability" level, where services are described in terms of preconditions and effects over ontological concepts. A key issue in addressing WSC as planning is that ontologies are not only formal vocabularies; they also axiomatize the possible relationships between concepts. Such axioms correspond to what has been termed "integrity constraints" in the actions and change literature, and applying a web service is essentially a belief update operation. The reasoning required for belief update is known to be harder than reasoning in the ontology itself. The support for belief update is severely limited in current planning tools. Our first contribution consists in identifying an interesting special case of WSC which is both significant and more tractable. The special case, which we term "forward effects", is characterized by the fact that every ramification of a web service application involves at least one new constant generated as output by the web service. We show that, in this setting, the reasoning required for belief update simplifies to standard reasoning in the ontology itself. This relates to, and extends, current notions of "message-based" WSC, where the need for belief update is removed by a strong (often implicit or informal) assumption of "locality" of the individual messages. We clarify the computational properties of the forward effects case, and point out a strong relation to standard notions of planning under uncertainty, suggesting that effective tools for the latter can be successfully adapted to address the former. Furthermore, we identify a significant sub-case, named "strictly forward effects", where an actual compilation into planning under uncertainty exists. This enables us to exploit off-the-shelf planning tools to solve message-based WSC in a general form that involves powerful ontologies, and requires reasoning about partial matches between concepts. We provide empirical evidence that this approach may be quite effective, using Conformant-FF as the underlying planner.

Several approaches have been proposed to tackle the selection of distributed processes described as semantic Web services. However, their practical applicability in real composition scenarios is still an open question. Addressing this problem requires on the one hand to deal with services described as stateful business processes and, on the other hand, to consider complex selection requirements concerning both the service interface and its behavior. In fact, in most existing approaches the selection is performed on the basis of the ldquofunctionalrdquo description of a service, i.e. in terms of its inputs, outputs, preconditions and effects. In this paper, we present our approach for the process-level service selection and evaluate it on a real world scenario that entails a high level of complexity: the eBay Web Services,the Amazon E-Commerce Services and the e-payment service offered by PayPal. The approach is based on a representation of services at the process level that is based on BPEL and WSDL specifications and that extends these standard specifications with minimal semantic annotations that permit to perform an efficient and yet useful, semantic reasoning for the process-level selection of Web services.

Service-centric systems are developed by composition and configuration of services, i.e., "software components that can be used but that are not owned". Services are most often not under control of consumers. They are indeed made available by third parties, they are autonomously developed and managed, and can in principle change without notification. Service Level Agreements (SLAs) define the exact conditions under which services are provided and consumed. From the point of view of the consumer, SLAs make explicitly available all the technical information required for using a service: interfaces and data structures, interaction protocols, security-related information, quality of services parameters and so on. They are therefore key elements for the development of software-centric systems. In this article we discuss one of the most interesting open challenges in the area of services and of SLAs: how to enable the usage of SLAs to support service adaptation and evolution. We discuss in particular two key roles that SLAs can play to this purpose, namely "SLAs for monitoring" and "SLAs for adaptation".

Telecommunication is a key area where the use of web services has an enormous potential to facilitate the development of powerful and complex functionalities on top of existing ones. At the same time, the specific features of TelCo applications (asynchronous, event-driven communications, handling concurrent, long-running transactions, dynamically evolving sets of partners) pose difficult challenges to the adoption of standard languages and tools for web services. In this work, based on our analysis of TelCo standards and applications, we discuss a set of orchestration patterns, and show how these can be modeled using the WS-BPEL language. We also address the issue of guaranteeing the correctness of such applications, providing an automated support for the formal analysis of their behavior.

Web services are conveniently advertised and published based on (stateless) functional descriptions, while they are usually realized as (stateful) processes. Therefore, the automated enactment of complex Web services on the basis of pre-existing ones requires the ability to handle services described at very different abstraction levels. This is the main reason behind the current lack of approaches capable to perform automated end-to-end composition, starting from semantic requirements to obtain executable orchestrations of stateful processes. In this paper we achieve such a challenging goal, by modularly integrating a range of incrementally more complex techniques that cover the necessary discovery and composition phases. By gradually bridging the gap between the high-level requirements and the concrete realization of services, our architecture manages sensibly the complexity of the problem: incrementally more complex techniques are provided with incrementally more focused input. The tests of our architecture on a deployed scenario witness the functionality of the platform and its integrability with standard service engines.

Several works address the problem of the automated composition of stateful services, e.g., specified in WS-BPEL. However, the key problem of their practical applicability in real composition scenarios is still open. Addressing this problem requires to provide an easy and affordable way to specify behaviors of component services and composition requirements, as well as composition techniques that are powerful enough to scale to scenarios of realistic size. In this paper we provide a first step towards addressing this problem by evaluating the feasibility and efficiency of a state-of-the art approach to automating the composition task on a real scenario that entails a high level of complexity: the Amazon e-commerce services and an e-payment service offered by an important Italian banking Group (Monte dei Paschi di Siena). We show the feasibility of the specification of composition requirements and of the automated generation of complex executable WS-BPEL processes, and analyze the possibility of reducing the effort in the composition task.

Linear Temporal Logic (LTL) is widely used for defining conditions on the execution paths of dynamic systems. In the case of dynamic systems that allow for nondeterministic evolutions, one has to specify, along with an LTL formula f, which are the paths that are required to satisfy the formula. Two extreme cases are the universal interpretation A.f, which requires that the formula be satisfied for all execution paths, and the existential interpretation E.f, which requires that the formula be satisfied for some execution path. When LTL is applied to the definition of goals in planning problems on nondeterministic domains, these two extreme cases are too restrictive. It is often impossible to develop plans that achieve the goal in all the nondeterministic evolutions of a system, and it is too weak to require that the goal is satisfied by some execution. In this paper we explore alternative interpretations of an LTL formula that are between these extreme cases. We define a new language that permits an arbitrary combination of the A and E quantifiers, thus allowing, for instance, to require that each finite execution can be extended to an execution satisfying an LTL formula (AE.f), or that there is some finite execution whose extensions all satisfy an LTL formula (EA.f). We show that only eight of these combinations of path quantifiers are relevant, corresponding to an alternation of the quantifiers of length one (A and E), two (AE and EA), three (AEA and EAE), and infinity ((AE)* and (EA)*). We also present a planning algorithm for the new language that is based on an automata-theoretic approach, and study its complexity.

In this paper we present an approach for modelling and analyzing time-related properties of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web service timed state transition systems (WSTTS), to capture the timed behavior of the composite Web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system's behavior. Building upon of this formalization, we provide techniques and tools for model checking BPEL4WS compositions against time-related requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of the e-government case study.

The run-time monitoring of Web service compositions has been widely acknowledged as a significant and challenging problem. In this paper, we propose a novel solution to the problem of monitoring Web services implemented in BPEL. We devise an architecture that clearly separates the business logic of a Web service from its monitoring functionality. The architecture supports both "instance monitors" that deal with the execution of a single instance of BPEL process, as well as "class monitors" that report aggregated information about all the instances of a BPEL process. We also define a language for the specification of instance and class monitors. The language allows for specifying boolean, statistic, and time-related properties. Finally, we devise a technique for the automatic translation of all these kinds of monitors to Java programs

The data exchanged among the Web services participating to a composition are clearly very relevant for a correct behavior of the composition. Nevertheless, most of the approaches existing in the literature for the static verification of Web service compositions ignore data, or require very small ranges to be associated to the data types. In this paper, we propose an approach for the verification of Web service compositions that takes into account the dataflows among the component process. The approach exploits abstraction techniques for modeling those aspects of data that are relevant for the correctness of the composition and hiding the aspects that are irrelevant. We show that building the right abstraction corresponds to defining those assumptions on the data manipulations performed by the component services which are crucial for the correctness of the composition

In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web service timed state transition systems (WSTTS), to capture the timed behavior of the composite Web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system's behavior. Building on top of this formalization, we provide techniques and tools for model-checking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study

One of the fundamental Ideas of Weh services and service oriented architecture is the possibility to develop new applications by composing existing services that are available on the Web. Several approaches have been proposed to tackle the problem of Web service composition, but little effort has been devoted so far to the problem of modeling the requirements of the composition. However, it is clear that the possibility to express requirements specifying complex interactions patterns among the component services is an essential step to cope with a wide range of composition problems. In this paper we present a new model which addresses one of the key aspects of composition requirements, namely the dataflow among the component services. We develop graphical notations and a formal theory for the new model and we integrate it within an existing automated composition framework

In this paper we describe an approach for the verification of Web service compositions defined by sets of BPEL processes. The key aspect of such a verification is the model adopted for representing the communications among the services participating in the composition. Indeed, these communications are asynchronous and buffered in the existing execution frameworks, while most verification approaches assume a synchronous communication model for efficiency reasons. In our approach, we develop a parametric model for describing Web service compositions, which allows us to capture a hierarchy of communication models, ranging from synchronous communications to asynchronous communications with complex buffer structures. Moreover, we develop a technique to associate with a Web service composition the most adequate communication model, i.e., the simplest model that is sufficient to capture all the behaviors of the composition. This way, we can provide an accurate model of a wider class of service composition scenarios, while preserving as much as possible an efficient performance in verification.

In this paper we propose a technique for the automated synthesis of new composite Web services. Given a set of abstract BPEL4WS descriptions of component services, and a composition requirement, we automatically generate an executable BPEL4WS process that, once deployed, is able to interact with the components to satisfy the requirement. We implement the proposed approach exploiting efficient synthesis techniques, and experiment with some case studies taken from real world applications and with a parameterized domain. We show that the technique can scale up to cases in, which the manual development of BPEL4WS composite services is not trivial and is time consuming.

Linear temporal logic (LTL) is widely used for defining conditions on the execution paths of dynamic systems. In the case of dynamic systems that allow for nondeterministic evolutions, one has to specify, along with an LTL formula /spl phi/, which are the paths that are required to satisfy the formula. Two extreme cases are the universal interpretation A./spl phi/, which requires to satisfy the formula for all the possible execution paths, and the existential interpretation E./spl phi/ which requires to satisfy the formula for some execution paths. When LTL is applied to the definition of goals in planning problems on nondeterministic domains, these two extreme cases are too restrictive. It is often impossible to develop plans that achieve the goal in all the nondeterministic evolutions of a system, and it is too weak to require that the goal is satisfied by some executions. In this paper we explore alternative interpretations of an LTL formula that are between these extreme cases. We define a language that permits an arbitrary combination of the A and E quantifiers, thus allowing, for instance, to require that each finite execution can be extended to an execution satisfying an LTL formulas (AE./spl phi/), or that there is some finite execution whose extensions all satisfy an LTL formula (EA./spl phi/). We show that only eight of these combinations of path quantifiers are relevant, corresponding to an alternation of the quantifiers of length one (A and E), two (AE and EA), three (AEA and EAE), and infinity ((AE)/sup /spl omega// and (EA)/sup /spl omega//). We also present a planning algorithm for the new language that is based on an automata-theoretic approach, and studies its complexity.

Formal Tropos is a specification language for early requirements. It is based on concepts from an agent-oriented early requirement model framework (i/sup */) and extends them with a rich temporal specification language. We demonstrated through a small case study how model checking could be used to verify early requirements written in Formal Tropos. We address issues of methodology and scalability for our earlier proposal. In particular, we propose guidelines for producing a Formal Tropos specification from an i/sup */ diagram and for deciding what model checking technique to use when a particular formal property is to be validated. We also evaluate the scope and scalability of our proposal using a tool, the T-Tool, that maps Formal Tropos specifications to a language that can be handled by NUSMV, a state-of-the-art model checker. Our experiments are based on a course management case study.

This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the π-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.

We describe an attempt to bridge the gap between early requirements specification and formal methods. In particular, we propose a new specification language, called Formal Tropos, that is founded on the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) (Yu, 1997), but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, in particular model checking, to allow for an automatic verification of relevant properties for an early requirements specification. Our preliminary experiments demonstrate that formal analysis reveals gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis tools.