Modeling and Verifying Microservice Autoscaling Using Probabilistic Model Checking

Abstract Microservices can independently adjust their capacity to match demand while the autoscaling feature in cloud computing facilitates the users (i.e., developers) to provision resources required by their applications with less human intervention. Kubernetes is one of the well-known technologies used to deploy microservice-based applications and many autoscaling methods have been proposed to improve the behavior of its Horizontal Pod Autoscaler (HPA). Despite many research efforts have been recently devoted to investigate microservice autoscaling, there is still a lack of studies that consider the correctness of the scaling decision as well as the effect of the scaling process on host energy consumption and system scalability factors. Therefore, in this work we aim to take into account formal verification in the microservice autoscaling decision-making process by utilizing Markov Decision Process (MDP) and probabilistic model checking. To this end, we propose five MDP model variations, inspired by the scaling behavior of Kubernetes-based HPA, analyze the performance of the models from a combination of metrics. The Base Model is built by considering the CPU utilization metric in decision making, while the other models extend it by including several additional metrics to enhance the decision (i.e., latency, response time, energy consumption, and performance change). We use the PRISM-games model checker for the analysis purpose by verifying the properties specified in Probabilistic Computation Tree Logic (PCTL). Through our experiments, the decision made by the Full Model which considers all the metrics has outperformed the other models in terms of minimizing the energy consumption and leading to a good scalability level (i.e. scalability near to 1).