Analyzing Energy-Efficient and Kubernetes-Based Autoscaling of Microservices Using Probabilistic Model Checking

• Published in: JOURNAL OF GRID COMPUTING
• Main Authors: Agos Jawaddi, Siti Nuraishah; Ismail, Azlan; Sulaiman, Mohd Suffian; Cardellini, Valeria
• Format: Article
• Language: English
• Published: SPRINGER 2025
• Subjects: Computer Science
• Online Access: https://www-webofscience-com.uitm.idm.oclc.org/wos/woscc/full-record/WOS:001388451100001

Microservices are widely used to enable agility and scalability in modern software systems, while cloud computing offers cost-effective ways to provision computing resources on demand. However, ensuring the correctness of scaling decisions and their impact on energy consumption is a challenging problem that has not been sufficiently addressed in previous research. Thus, in this paper, we present an innovative approach for analyzing host energy consumption and energy violations influenced by microservice autoscaling policies using probabilistic model checking (PMC). We propose four variations of the Markov Decision Process (MDP) models that incorporate various scaling constraints inspired by Kubernetes-based Horizontal Pod Autoscaler, and we encode these models using two different approaches, namely, bounded-by-action (BBA) and bounded-by-state (BBS). We use PMC to verify the scaling policies in terms of host energy consumption and energy violations, and we conduct sensitivity analysis to demonstrate the effectiveness of our models in generating energy-efficient scaling policies. Our results show that the latency and energy-based MDP model offers the most suitable policies for ensuring energy efficiency in microservice systems. Additionally, the number of pods and the scale-out action significantly affect energy consumption and violations. Sensitivity analysis also reveals that incorporating latency into scaling decisions is key to energy efficiency, while variations in the maximum pod threshold significantly influence energy consumption and violation. Our approach provides a formal method for ensuring the correctness of microservice autoscaling decisions in cloud environments at design time and can help reduce energy consumption and violations while ensuring service-level objectives are met.