Abstract
Cloud computing is a revolution in how computing power is delivered to business. It offers different measured services to clients who require them by writing a simple request. These requests are becoming more and more complex so that services need to be composed to meet them. Additionally, these Cloud composite business services (CCBSs) need to be elastic, i.e. their number should be replicated or reduced according to the number of their user demands. Ensuring these two operations is done according to a well-defined strategy. We are interested in this paper in cost-effective elasticity one. Applying this strategy on CCBSs gives birth to a system that needs to be checked to insure that SLA constraints, such as deadline specified by the user, are not violated. In this paper, we present a formal model using Timed Coloured Petri nets to model, check and compare between these strategies before implementing them in real Cloud.