A Formal Approach for Verifying QoS Variability in Web Services Composition Using EVENT-B

The main issues for the fulfillment service level agreements (SLA) are concerned with problem of variability of QoS properties (vQoS). Indeed, the QoS properties may evolve frequently either because of internal changes or because of workload fluctuations. To solve the vQoS problem, we first introduced three variability operators: replicate, delete and replace. These operators will be used to reconfigure CWS when the SLA contract is violated. The first two operators are used to add and remove Web service instances, while the last one is used to substitute some faulty Web services. Then, we proposed an incremental approach for modeling and verifying the composites services (CWSs) reconfiguration using Event-B. We start by abstractly specifying the main requirements and then we refine them through several steps to model CWSs. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we used ProB model-checker to trace possible design errors. We have exploited the LTL for dynamic reconfigurations to characterize the correct behavior of CWSs reconfiguration.