| Summary: | Cloud autoscaling is an important mechanism to dynamically manage cloud system resources with uncertain workload demands. The common goal in developing such a mechanism is to produce correct-by-design scaling policies that contribute to a reliable autoscaling component. A promising approach is formal verification, specifically probabilistic model checking (PMC), used to model and assess cloud scaling processes and policies. Utilizing the appropriate formal models effectively for carrying out verification tasks is one of the important factors in gaining significant insights. This is a great challenge dealt by the responsible party (e.g., cloud architects, engineers) in maximizing the benefits of PMC for their further decision-making (e.g., deploying the verified policies). In response to this challenge, we propose an approach to formalize and assess the cloud scaling process based on two formal models, namely, Markov Decision Process (MDP) and discrete-time Markov Chain (DTMC), and using PMC. We treat these two models independently for modeling similar cloud scaling contexts and assess the relevant aspects for gaining significant insights. Our approach consists of three main phases: modeling, encoding, and assessment. In our assessment, which includes complexity, performance, and sensitivity analyses, we have identified distinct sensitivities in the DTMC and MDP models. Specifically, DTMC is more sensitive to over-provisioning events, while MDP is more sensitive to under-provisioning events. These sensitivities are mainly influenced by two critical parameters: the initial number of VMs and the minimum number of VMs. Across various sample sizes, DTMC showed an increase in average latency violations from 53 to 209 for over-provisioning events, while MDP demonstrated a decrease in average latency violations from 88 to 23 for under-provisioning events. © The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature 2023.
|
|---|