Composition of Cloud services is necessary when a single component is unable to satisfy all the user's requirements. It is a complex task for Cloud managers which involves several operations such as discovery, compatibility checking, selection, and deployment. Similarly to a non Cloud environment, the service composition raises the need for design-time approaches to check the correct interaction between the different components of a composite service. However, for Cloud-based service composition, new specific constraints, such as resources management, elasticity and multitenancy have to be considered. In this work, we use Symbolic Observation Graphs (SOG) in order to abstract Cloud services and to check the correction of their composition with respect to event-and state-based LTL formulae. The violation of such formulae can come either from the stakeholders' interaction or from the shared Cloud resources perspectives. In the former case, the involved services are considered as incompatible while, in the latter case, the problem can be solved by deploying additional resources. The approach we propose in this paper allows then to check whether the resource provider service is able, at run time, to satisfy the users' requests in terms of Cloud resources.

Composition of Cloud services is necessary when a single component is unable to satisfy all the user's requirements. It is a complex task for Cloud managers which involves several operations such as discovery, compatibility checking, selection, and deployment. Similarly to a non Cloud environment, the service composition raises the need for design-time approaches to check the correct interaction between the different components of a composite service. However, for Cloud-based service composition, new specific constraints, such as resources management, elasticity and multi-tenancy have to be considered. In this work, we use Symbolic Observation Graphs (SOG) in order to abstract Cloud services and to check the correction of their composition with respect to event-and state-based LTL formulae (Hybrid LTL). The violation of such formulae can come either from the stakeholders' interaction or from the shared Cloud resources perspectives. In the former case, the involved services are considered as incompatible while, in the latter case, the problem can be solved by deploying additional resources. Using our approach, one can check then, if the resource provider service can supply sufficient Cloud resources w. r. t. the users' requests.

In this paper, we propose a bottom-up approach to check the correct interaction between workflows distributed over a number of organizations. The whole system's model being unavailable, an up-down analysis approach is not appropriate. We consider two correctness criteria of inter-organizational work-flows communicating asynchronously and sharing resources: a generic one expressed with the soundness property, and a specific one expressed with any temporal property expressed with the LTL logic. Each part of the whole organization exposes its abstract model, represented by a Symbolic Observation Graph (SOG), to allow the collaboration with possible partners. The SOG is then revisited and adapted in order to reduce the verification of the entire composite model to the verification of the composition of the SOG-based abstractions. We illustrate our approach with a case study and give preliminary results of our implemented prototype.

For automatically composing Web services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) is possible without including any additional information that can be used to disclose the privacy of these services. The compatibility property is defined by different variants of the well known soundness property on open workflow nets. These properties guarantee the absence of livelocks, deadlocks and other anomalies that can be formulated without domain knowledge. In this paper we address the automatic abstraction of Web services and the checking of their compatibility using their abstract models only. To abstract Web services, we use the symbolic observation graph (SOG) approach that preserves necessary information for service composition and hides private information. We show how the SOG can be adapted and used so that the verification of different variants of compatibility can be performed on the composition of the abstract models (SOGs) of Web services instead of the original composite service.

This work deals with services composition. We propose an approache based on Symbolic Observation Graphs (SOG) allowing to decide whether two (ore more) web services can cooperate safely. The compatibility between two web services is defined by the well known soundness property on open workflow nets and checked on the composition of SOGs instead of the original web services composition. This allows to respect the privacy of the services since SOGs are base on collaborative activities only and hide the internal structure and behavior of the corresponding service.