Formal Approach for QoS-Aware Cloud Service Composition

Cloud Computing based Software as a Service (SaaS) combines multiple Web Services to satisfy a SaaS request. SaaS is based on Service-Oriented Architecture and Web Service technology which are popular paradigm to design new generation of applications. One of the advantages of Web Services technology is to building distributed application on demand using existing service oriented application. Web Services Composition (WSC) in Cloud Computing is necessary when a single service is unable to satisfy all the customers requirements. WSC is a complex task in the SaaS which involves several steps like discovery, compatibility checking, selection and deployment. To reduce the complexity of WSC, we model Web Services and their composition using Boolean satisfiability problem so that a specific property of their structures is looked into behavioral compatibility. The aim of this work is the modelling and verification of Web Services Composition using a formal method based on Satisfiability (SAT). However, in some cases it may be preferable to use variations of the general SAT problem. Specifically, using the Minimally Unsatisfiable Subformula (MUS), we formally define a Web Services Composition and its validation. When we have a multiple Web Services Compositions that meet the users needs, a QoS of the resulting WSC is maximized or, in some cases, minimized.