Verification of cloud system elasticity using BigMC

Elasticity is one of the important characteristics of cloud computing used to manage the fluctuating real time workload in the cloud environment. Cloud providers use this approach to perform resource provisioning or de-provisioning of various computing resources to manage real workload. It is challenging task for cloud providers to implement elasticity strategies for complex system to utilize the computing resources effectively due to the fluctuating nature of workload. To address this challenge, we use the Bigraphical Reactive Systems based approach to formally model the cloud elasticity structure through bigraphs and their dynamic behavior with the help of bigraphical reaction rules. This article focuses on addressing cross-layer elasticity i.e. the elasticity at service and infrastructure level. The system elasticity strategies are described to perform horizontal and vertical scaling of cloud system’s through auto-adaption of behaviors using bigraph formalism. Further, we convert the bigraphical specifications into the framework provided by the BigMC model checker tool for horizontal and vertical scaling and verify their correctness. BigMC is a counter-example based model checking tool, it provides an autonomic executability of the behaviors in the cloud systems.