Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi

Microservice autoscaling is one of the critical mechanisms in a cloud system that needs to be analyzed and verified to ensure that it is working as expected. This is a challenging task for the cloud engineer at design time especially if they need to understand the impact on the energy consumption since the actual request demands are unknown which causes non-deterministic scaling action. Probabilistic model checking (PMC), a branch of formal verification has been widely recognized as a suitable technique to analyze stochastic systems exhaustively. Since microservice autoscaling can be characterized as a stochastic system, this technique is naturally suitable to be applied for verification and analysis purposes. However, the application of this technique is not a straightforward implementation since the autoscaling behavior needs to be formally specified, and the objective to be measured needs to be formally quantified. Therefore, this research addresses this challenge by proposing a formalism of microservice autoscaling decision process to enable verification and analysis of the decision in relation to energy efficiency level. Four formal models based on the Markov decision process (MDP) have been developed by embedding distinct scaling constraints. The models are then encoded, verified, and analyzed using a PMC model checker, known as PRISM. The analyses conducted focus on the efficiency measures by comparing the four models that consider different sets of scaling constraints to drive the autoscaling decision-making process. The measures determine how far the models can minimize the host energy consumption and how frequently the decisions made by the models cause energy violations. The inputs of each model are based on the variation of incoming workloads at a normal hour and peak hour.