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 si...

Full description

Saved in:

Bibliographic Details
Main Author:	Agos Jawaddi, Siti Nuraishah
Format:	Thesis
Language:	English
Published:	2023
Subjects:	QC Physics
Online Access:	https://ir.uitm.edu.my/id/eprint/88754/1/88754.pdf
Tags:	Add Tag No Tags, Be the first to tag this record!

id	my-uitm-ir.88754
record_format	uketd_dc
spelling	my-uitm-ir.887542024-01-02T02:17:49Z Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi 2023 Agos Jawaddi, Siti Nuraishah QC Physics 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. 2023 Thesis https://ir.uitm.edu.my/id/eprint/88754/ https://ir.uitm.edu.my/id/eprint/88754/1/88754.pdf text en public masters Universiti Teknologi MARA (UiTM) College of Computing, Informatics and Mathematics Ismail, Azlan Sulaiman, Mohd Suffian
institution	Universiti Teknologi MARA
collection	UiTM Institutional Repository
language	English
advisor	Ismail, Azlan Sulaiman, Mohd Suffian
topic	QC Physics
spellingShingle	QC Physics Agos Jawaddi, Siti Nuraishah Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
description	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.
format	Thesis
qualification_level	Master's degree
author	Agos Jawaddi, Siti Nuraishah
author_facet	Agos Jawaddi, Siti Nuraishah
author_sort	Agos Jawaddi, Siti Nuraishah
title	Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
title_short	Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
title_full	Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
title_fullStr	Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
title_full_unstemmed	Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi
title_sort	verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / siti nuraishah agos jawaddi
granting_institution	Universiti Teknologi MARA (UiTM)
granting_department	College of Computing, Informatics and Mathematics
publishDate	2023
url	https://ir.uitm.edu.my/id/eprint/88754/1/88754.pdf
_version_	1794192154737770496

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

Similar Items