A formal quantitative analysis of elastic cloud systems based on PSMaude

Abstract

Cloud computing, with its various extensions, is a significant IT evolution aiming to provide on-demand IT services with an efficient resource usage, but still ensuring service availability and Quality of Service (QoS). Resource elasticity is an effective feature to deal with such issues; it provides the ability to adjust rapidly the deployed resource capacity according to the time-varying workload in order to meet the intended QoS requirements. However relying only on service provider strategies as horizontal and vertical elasticity, seems insufficient to ensure the QoS requirements, since resource usage patterns in Elastic Cloud Systems (ECS) are inherently non-deterministic. This causes difficulties while selecting the elasticity strategy to be applied with respect to QoS parameters. In this paper, we supply solutions for the challenging task of managing ECSs by quantifying the non-determinism on the basis of QoS parameters. Therefore, we define a formal model for specifying cloud systems structure and its dynamics in terms of quality driven elasticity strategies. Besides, a quantitative analysis is performed to evaluate the effectiveness of the proposed model with regard to QoS parameters.

Keywords

• Cloud Computing
• Elasticity
• Formal methods
• PSMaude
• Quantitative verification