Cover Image

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
https://ir.uitm.edu.my/id/eprint/88754/
Tags: Add Tag
No Tags, Be the first to tag this record!
id my.uitm.ir.88754
record_format eprints
spelling my.uitm.ir.887542024-07-22T07:48:05Z https://ir.uitm.edu.my/id/eprint/88754/ Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi 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 NonPeerReviewed text en https://ir.uitm.edu.my/id/eprint/88754/1/88754.pdf Verification of energy-driven microservice autoscaling policies in cloud environment using probabilistic model checking / Siti Nuraishah Agos Jawaddi. (2023) Masters thesis, thesis, Universiti Teknologi MARA (UiTM). <http://terminalib.uitm.edu.my/88754.pdf>
institution Universiti Teknologi Mara
building Tun Abdul Razak Library
collection Institutional Repository
continent Asia
country Malaysia
content_provider Universiti Teknologi Mara
content_source UiTM Institutional Repository
url_provider http://ir.uitm.edu.my/
language English
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
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
publishDate 2023
url https://ir.uitm.edu.my/id/eprint/88754/1/88754.pdf
https://ir.uitm.edu.my/id/eprint/88754/
_version_ 1806422069802434560
score 13.250246

Similar Items