https://doi.org/10.31449/inf.v45i4.3308 Informatica 45 (2021) 529–541 529 Modeling and Performance Analysis of Resource Provisioning in Cloud Computing using Probabilistic Model Checking Hichem Debbi Department of Computer Science, University of M’sila, M’sila, Algeria E-mail: hichem.debbi@univ-msila.dz Keywords: cloud computing, IaaS, performance analysis, resource provisioning, probabilistic model checking, PRISM Received: September 14, 2020 Cloud computing consists of an advanced set of technologies that allow cloud providers to offer computing resources such as infrastructure, platforms and applications to be accessible over the Internet as services. Cloud computing relies on virtualization of resources in the cloud data centers, where a set of Virtual Machines (VMs) are deployed on Physical Machines (PMs) to provision and serve user requests. Due to the dynamic nature of cloud environments and complexity of resources virtualization, as well as the diversity of user’s requests, developing effective techniques to evaluate and analyze the performance of cloud centers has become highly required. In this paper, we propose the use of probabilistic model checking as an effective framework for the evaluation and the performance analysis of resource provisioning in the cloud. Based on an analytical model for resource provisioning in Infrastructure-as-a-Service (IaaS) cloud, we build a stochastic model using the probabilistic model checker PRISM and analyze it against a useful set of probabilistic and reward properties that help to measure and analyze cloud performance in an efficient way. Povzetek: Analizirane so razne komponente raˇ cunanja v oblaku, npr. modeliranje in performance virov. 1 Introduction Cloud computing is a novel information technology that provides access to different IT services on demand over the Internet. The services provided through the cloud range into three main categories: Infrastructure as a Ser- vice (Iaas), where infrastructure resources such as: servers, storage, network components are provisioned. Platform as a Service (PaaS), which provides an environment for developing, running and managing applications efficiently by reducing the complexity related to infrastructure. Soft- ware as a Service (SaaS), which represents the largest cloud market, in which the task of managing software is moved to third-party services. Cloud computing has been treated from different aspects such as: security [22], load balanc- ing [24], storage[7] and consistency [21]. In cloud computing literature, we refer usually to ser- vice providing by the technical term, provisioning. In this regard, Vaquero et al. [23] defined cloud as: the provi- sion of computing infrastructure, which aims to shift the location of the computing infrastructure to the network in order to reduce the costs associated to management and maintenance of hardware and software resources. These resources are offered to the customer by cloud providers based on specific legally binding contracts called Service Level Agreements (SLAs), which state Quality of Service (QoS) parameters, such as time, cost, availability and se- curity that should be guaranteed by service providers in or- der to meet customer’s needs and execute service requests. Buyya et al. [5] defined the cloud as: "A Cloud is a type of parallel and distributed system consisting of a collec- tion of inter-connected and virtualized computers that are dynamically provisioned and presented as one or more uni- fied computing resources based on service level agreements (SLA) established through negotiation between the service provider and the customers". In IaaS cloud, virtualization plays a crucial role in en- abling cloud computing services, in fact, it is a principal mechanism that enables cloud providers to cope with mul- tiple requests of users through virtualization of physical machines(PMs). Virtualization refers to the abstraction of computing resources in a way that a single physical ma- chine can run a set of virtual machines(VMs)[3]. However, due to dynamic nature of cloud computing en- vironments and the complexity related to managing infras- tructure resources from a side, and the diversity in cus- tomers requests from another, addressing the effective ways to instantiate, provision and deploy infrastructure resources to handle user requests and meet QoS requirements is con- sidered as a big challenge and very critical issue in cloud computing. Therefore, performance analysis and evalua- tion of cloud computing environments have attracted re- cently much attention and formed an active research area. Cloud performance analysis is beneficial for both cloud providers and consumers because it helps to get a deep in- sight on the infrastructure resources and how they should 530 Informatica 45 (2021) 529–541 H. Debbi be provisioned and scaled to execute various customers re- quests. Among various performance and evaluation meth- ods, analytical modeling-based methods represent the ma- jor research that has been done in this area [8]. Since resources provisioning and usage is highly variable and uncertain, and since the arrival of customer requests is stochastic, these methods are stochastic in general, and em- ploy queuing theory with different buffers to cope with a large number of requests given the available resources, and thus, performance measures are quantified using prob- abilistic methods. These stochastic methods can effectively capture the uncertainty beyond cloud provisioning behav- ior and estimate perfectly cloud metrics. Hence, SLA can be maintained and an overall optimization can be achieved. Continuous-time Markov Chains (CTMC), Stochastic Re- ward Net (SRN) and Stochastic Petri Nets (SPN) are all stochastic models that have been used for modeling and analyzing cloud services performance, and they showed promising results. Performance behavior in the cloud is affected by a large set of parameters, and thus many system variables must be introduced to capture every modeling detail. CTMC mod- els represent a good candidate to model every detail of the system [12, 17]. However, as the system variables under modeling grow up, the analysis could be intractable, since it results in a very large state space, which is known as the state explosion problem. To cope with such a problem, a solution based on decomposing the entire model into small interacting sub-models is proposed to facilitate and speed- up the model generation[12]. Bradley et al.[4] stated that symbolic approaches are very useful for performance and resilience modeling and analysis of massive stochastic systems, and thus they are very suitable for state space representation for cloud computing systems. Symbolic techniques such as Multi- terminal Binary Decision Diagrams are efficiently used to encode CTMCs, and enable steady-state and transient anal- ysis. These techniques are efficiently employed by the probabilistic model checker PRISM[14], whose language features synchronization between modules. These advan- tages make PRISM a suitable tool for the performance anal- ysis of cloud computing systems. In this paper, we aim to show how probabilistic model checking can be used for the performance analysis and evaluation of IaaS cloud based on analytical modeling methods using CTMCs. Probabilistic model checking has appeared as an extension of model checking for analyz- ing systems that exhibit stochastic behavior. These systems are described usually using Discrete-Time Markov Chains (DTMC), Continuous Time Markov Chains (CTMC) or Markov Decision Processes (MDP), and verified against properties specified in Probabilistic Computation Tree Logic (PCTL)[13] or Continuous Stochastic Logic (CSL) [1, 2]. Using the probabilistic model checker PRISM [14], we show that analytical models, even if they are composed of many interacting sub-models, can be easily expressed in PRISM language and analyzed in an efficient way. The en- tire model can be generated from interacting sub-models in reasonable time thanks to many numerical solution meth- ods employed by PRISM that can deal perfectly with the state explosion problem. In this paper, we chose the model proposed by [12] as a case study. With probabilistic model checking, we will not be able only to compute probabilities related to QoS metrics, but also we can verify such safety properties and analyze reward-based properties. The rest of this paper is organized as follows. In Sec- tion 2 we present some related works to cloud performance analysis. Section 3 presents some preliminaries and defi- nitions on PRISM language. In section 4, we present the analytical model and its implementation in PRISM with detailed analysis of probabilistic and reward properties. Fi- nally, we conclude the paper in Section 5. 2 Related work The performance analysis and evaluation of cloud com- puting services can be performed through two ways: measurement-based methods and analytical modeling- based methods. In measurement-based methods [19], both cloud services and performance metrics to be evaluated should be known in prior, and then the benchmark to be tested should be chosen accordingly. After that, the test- ing experiments can be executed. Actually, this technique suffers from extensive experiments that should be executed with different workloads and system configurations, which may make the construction of appropriate testbeds that can represent realistic cloud services scenarios a costly task. Despite that, some measurements become invalid when cloud service providers upgrade their software and hardware to enhance their services. Therefore, analytical modeling-based methods are considered as a good alterna- tive since they are of low cost, and can cover large param- eters of cloud services, especially that these methods can analyze features of services even in early stages of design. Li et al. [20] addressed the analysis of cloud services by modeling the service as a queuing network consisting of two tandem servers, web server and service server. After service completion at the level of the web server, the re- quest either exits the network or continues to be executed at the service server. Both servers are modelled as M/M/1 queue with an exponential distribution of arrival and ser- vice times. The main metric under evaluation in this paper was response time. Based on this measure, a relationship between the number of customers, the minimal service re- sources and the highest level of services can be easily de- rived. However, this work lakes an important feature in cloud computing modeling, which is virtualization. Chen et al. [6] have also considered queuing network to estimate two different performance metrics, which are practically needed more in the context of cloud comput- ing, request completion time (ECT) and rejection prob- ability (RP). The authors in this work consider also two Modeling and Performance Analysis of Resource Provisioning in. . . Informatica 45 (2021) 529–541 531 queues, admission queue, and PM queue. Visualization is addressed considering many parameters, such as buffer size of queues, number of virtual machines, number of physical machines and error/recovery rates. In this work, each job is denoting a VM instance, and each VM is deployed on a single PM. While previous works assume an exponential distribu- tion of requests, considering heterogeneity in cloud model- ing is actually more appropriate to better analyze some dy- namic properties. In this regard, Khazaei et all. [16] intro- duced an embedded Markov model as an approximate an- alytical model based on M/G/m/m+r queuing system with single task arrivals and a task buffer of finite capacity. By solving the approximate model, complete probability dis- tribution of the request response time, and important per- formance indicators such as the mean number of tasks in the system, the blocking probability, and the probability of immediate service can be easily estimated. Covering more cloud services parameters by perfor- mance evaluation model is highly needed. However, some- times the analysis of such a model tends to be intractable. To deal with this issue, some works [12, 17] proposed a solution based on interacting stochastic sub-models of Continuous-time Markov Chain (CTMC), thus, quantify- ing performance metrics can be realized in a scalable man- ner. In [12], the main QoS addressed was service avail- ability and provisioning response delays. The requests or jobs submitted by users can be served in different pools named (hot, warm and cold), the decision in which pool the request should be served is made by a module called resource provisioning decision model, which is a CTMC model consisting of a queue with finite length. Another queue is found at each PM, where some requests/jobs can wait for VM provisioning. While this model is limited to service requests with a single task, Kazai et all. [17] pro- posed a similar solution, but capable of dealing with batch arrival of requests, where multiple VMs can be provisioned to handle multi-tasks based on a single service request, thus realizing a high degree of visualization. Probabilistic model checking has already been used for modeling and analysis of cloud computing. Kikuchi and Matsumoto [18] have used PRISM for the performance modeling and analysis of concurrent live migration oper- ations in cloud computing systems. Live migration plays a crucial role in cloud virtualization since it guarantees trans- porting VMs from a host to another without affecting the performance of the services. The authors described the performance model of concurrent VM live migration op- erations as a CTMC in PRISM language, and it has been verified against two main quantitative properties regarding the operations that can be stacked in waiting state at sender side, and the operations that are executed at server side. In [15], the authors defined an interesting set of resource usage patterns in PRISM language as an MDP, and then in- troduced a set of reward-based properties for analyzing cost variation, and min/max probabilistic properties to analyze deployment’s resource usage. These probabilistic patterns before being generated as MDPs, are first expressed in a higher language called probabilistic pattern modeling lan- guage (PPM). Evangledis et al. [9] addressed performance modeling and formal verification of auto-scaling policies in PaaS and IaaS to provide performance guarantees to reduce SLAs violations, where two cloud services providers Amazon EC2 and Azure have been considered. The authors consid- ered rule-based auto-scaling policies, where upper and/or lower bound on performance metrics such as CPU are ex- pressed. The dynamics of auto-scaling process are ex- pressed in PRISM as DTMC, and verified against proba- bilistic properties to estimate CPU utilization and response time violation for each auto-scaling policy, thus refining QoS violation thresholds for the policies. We summarize the existing related work in Table 1 3 PRISM PRISM is a tool used for formal modeling and analyz- ing systems that exhibit random or probabilistic behav- ior [14]. It supports several types of probabilistic mod- els such as DTMCs, CTMCs and MDPs. The analysis is performed on these models against properties specified in PCTL logic [13] for DTMCs and MDPs and Continuous Stochastic Logic (CSL) [1, 2]for CTMCs. PRISM uses several numeric methods for model analysis such as Gauss- Seidel method, Backwards Gauss-Seidel method and Ja- cobi method. For MDPs and CTMCs, PRISM uses value it- eration and uniformisation, respectively. As additional fea- tures, PRISM offers a simulation framework for reasoning about probabilities and rewards. A model in PRISM consists of one or several modules that interact with each other. The module is specified using PRISM language as a set of guarded commands. []! Where the guard is a predicate over the variables of the system and the updates describe probabilistic transitions that the module can make if the guard is true. These up- dates are defined as follows: < prob >:< atomicupdate > +:::::+ < prob >:< atomicupdate> When representing CTMCs, < prob > will refer to transition rates instead of discrete probabilities. PRISM also supports rewards which are real values associated with states or transitions of the model. Where state rewards can be specified as: g : r, and transition rewards are repre- sented as: [a]g :r. The properties for a CTMC model can be specified in CSL logic that allows the specification of both transient behavior and steady state behavior. We use the P opera- tor for specifying transient properties and S operator for specifying steady state properties. Another interesting op- erator employed is the R operator that is used to reason on the expected value of rewards. Example 532 Informatica 45 (2021) 529–541 H. Debbi Analytical models Analytical Tools Properties Scope Experimental setting Ghosh et al. [12] CTMCs SPHERE service availability, provisioning response delays Infrastructure IBM SmartCloud Khazaei et al.[17] CTMCs Maplesoft rejection probability, response delays Infrastructure Artifex engine Li et al.[20] queuing net- works Matlab completion time, rejection probability, system overhead rate Infrastructure – Chen et al. [6] queuing net- works – Rejection probability, task completion time Infrastructure XenServer and OpenStack Kikuchi et al.[18] CTMCs PRISM stacked operations, executed operations Infrastructure XenServer Jhonson et al.[15] MDPs PRISM Cost variation, deployment’s resource usage Infrastructure – Evangledis et al.[9] DTMCs PRISM CPU utilization, response time violation Infrastructure, Platform Amazon EC2 and Azure Table 1: Main related work on cloud performance analysis. λ q=0 q=1 q=2 q=3 µ λ µ λ µ {Empty} {Full} Figure 1: Queue model. Let us consider the CTMC presented in Figure 1. It repre- sents a queuing system with maximum length 3. The sys- tem can move from an empty state, where there is no job to a new state with (q = 1) by the arriving of a new job wit rate , and can return to the previous state by serv- ing the job with a rate . The same thing applies for the rest of states. The corresponding module for this model is described in Figure 2. We have to declare 3 vari- ables, the integer variablelq that refers to queue length and two double variables representing the arrival and services rates. The main variable isq, which represents the possi- ble states of the system through raising two main transi- tions, Arrive and Service, with their corresponding rates. We can express probabilistic properties based on the value of time variable T . For instance, we can express a CSL property that states that the probability of the queue be- ing full with time T should not exceed the probability 0:5: P <= 0:5[trueU <= T \full"]. The property 1 ctmc 2 const int lq = 3;//queue length 3 const double lambda = 1/10;//arrival rate 4 const double mu = 1/2;//service rate 5 module Queue 6 q: [0..lq] init 0; 7 [Arive] (q lambda: (q’=q+1); 8 [Serve] (lq>0) -> mu : (q’=q-1); 9 endmodule 10 label "full"= q=3; Figure 2: Prism model for the queuing system. can be rewritten in a different way to estimate the prob- ability of the property being true within time unit T as P =?[trueU <=T \full"]. 4 Case study The model that we are going to study concerns data cen- ters that consist of a number of Physical Machines (PMs) [12]. When user requests arrive at a cloud center, a vir- tual machine or many VMs are deployed on PMs to serve this request. A single VM can be provisioned to serve a single request, however, in reality, multiple VMs can be provisioned on a single or multiple PMs to serve such com- plex request or super-task [17]. The PMs are grouped into three servers: hot (i.e., running VMs), warm (turned on, but without running VMs) and cold (turned off). It is tried first to provision the request on a hot pool if there is enough capacity, if there is no a hot PM available, there will be a Modeling and Performance Analysis of Resource Provisioning in. . . Informatica 45 (2021) 529–541 533 look-up for a warm PM, if all warm PMs are busy, a PM in the cold pool is used. In the case where no PM is avail- able in all pools, the request will be simply rejected. The strategy of regrouping the PMs into multiple pools results in a good performance by reducing VMs provisioning de- lay and operational costs. The model proposed consists of three sub-models that refer to the three main steps of cloud servicing, which are resource provisioning decision, VM provisioning, and run-time execution. The overall solution is obtained by interacting over these three sub-models. The steps of provisioning and servicing are presented in Figure 3. In the following, we will describe each of the CTMCs models. 4.1 Resource provisioning decision model (RPDM) This module is responsible for choosing the PM that can ac- cept the request and in which pool. A finite decision queue is employed, where decisions are made on FIFO basis. The arrival to RPDM is modeled as Poisson process with arrival rate . The related CTMC model is shown in Figure 5. The states in the model are presented as pairs (i;j), where i denotes the number of requests being waiting in the global queue, andj denotes the pool on which the re- quest is under provisioning. The initial state (0; 0) means that the system is in an empty state, where there is no re- quest, neither in the queue nor under provisioning. j is set to ’h’ if there is at least one hot PM that can accept the job for provisioning. Similarly, when j is set to ’w’ (or ’c’), that means that a warm (or cold) PM can accept the job for provisioning. The waiting queue for this model has a maximum numberN. From the initial state, by arriving of a new request, the system moves to the state (0;h) with rate , since it tries to find a hot PM first. From this state the following three possible transitions can occur: – A request is accepted for provisioning in a hot PM, and thus the module returns to the state (0; 0) with rateP h h . – Another request arrives, and the system moves to state (1;h) with rate . – No hot PM can accept the request for provisioning due to insufficient capacity, and thus the system tries to find a warm PM and transits to state (0;w) with rate h (1 P h ) Now, from the state (0;w), the model tries to find an available warm PM to provision the request, if one warm PM is available, the model moves back to the initial state with rateP w w , otherwise, the module tries to find a PM in cold pool by making a transition to (0;c) with rate w (1 P w ). Then, from the state (0;c), the request can be either accepted in the cold pool, and thus the model moves back to the initial state with rateP c c , or the request is rejected when there is no available cold PM, and thus the model moves to the same state with a rate c (1 P c ). The state wherei>= 1 means thati request is waiting in the queue. The related prism module of this model is depicted in Figure 6. We use two main variables, i and j, where i refers to the number of jobs waiting in the queue, and j de- notes the type of pool (j=1 for hot, j=2 for warm and j=3 for cold). The commands with wait action and rate (lines 6, 11 and 16) refer to a new request waiting and staying at the same pool, hot, warm and cold respectively. The other commands of provision refer to the provision in hot, warm and cold respectively with the appropriate rates. The rest of the commands where no action is defined refer to search- ing for a PM in the next pool. While wait actions have no control on the entire model, and they are just used for in- dication, the other actions (Provision_hot, Provision_warm and Provision_cold) are used for synchronization with the rest of provisioning models (hot, warm and cold). To build our model we need global as well as local vari- ables. While local variables are defined at each module, global variables are defined at the top of the global model, thus they can be used by all modules. The rates in CTMC models are usually defined as global variables. In addition, we can define some variables that play an important role in defining properties such as the time variableT . The set of variables with their values are presented in Figure 4. These values are basically adapted from [12, 10]. 4.2 VM provisioning models These models capture instantiation, configuration and pro- visioning of a VM on a PM. The model for provisioning a hot PM is described as a CTMC in Figure 10. In this model, requests, PMs and VMs are all assumed to be ho- mogeneous, and each request is for one VM instance. We also assume that inter-arrival time, service time and VM provisioning time are all exponentially distributed. Figure 10: VM provisioning model for each hot PM[12, 11]. States of provisioning model are controlled by three main variables i, j and k, where i presents the number of requests in PM’s queue,j presents the number of VMs currently being provisioned, andk presents the number of VMs which have already been deployed. There are also in- put parameters that control the model, L h that represents the size of PM’s queue, j can be 0 or 1 if the VMs are 534 Informatica 45 (2021) 529–541 H. Debbi Figure 3: Request provisioning and servicing steps [12]. assumed to be provisioned one at a time, otherwise, a pa- rameter can be introduced to refer to the number of VMs under provisioning. Finally, we have the maximum value ofk, which refers to the maximum number of VMs that can run in parallel (m). The other parameters concern rates: ef- fective job arrival rate ( h ), VM provisioning rate ( h ) and service rate ( ). As we see in Figure 10, when a request arrives, the model moves from state (0,0,0) to state (0,0,1) with a rate h , which means that the current request is under provi- sioning, then it moves to the state (0,0,1), with a rate h , the last state indicates that one VM is deployed, upon ser- vice completion, VM instance is removed and the model goes back state (0; 0; 0) with service rate . The related PRISM mode for a hot PM is presented in Figure 7. We use here three variables: xh that refers to the state of PM’s queue, yh that refers to the provision- ing state and zh that refers to the number of VMs being deployed. The commands refer in order to provisioning, deployment and service respectively. An additional action has been added just to use it in properties that specify the number of requests being rejected. The two other CTMCs for warm and cold PMs are sim- ilar, though, they can define different arrival and instan- tiation rates (see Figure 11 and Figure 12). The most important difference concerns provisioning step, where in both warm and cold pools, PMs are turned on but not ready to use, thus, they require additional startup time. Time to make a warm/cold PM ready for use is exponentially dis- tributed with a rate w / c . The related PRISM modules describing warm and cold provisioning models are shown in Figures 8 and 9 re- spectively. We notice that warm and cold models define the same variables and steps as the hot model does, ex- cept with the provisioning step, where the values yw and yc have a larger range, yw = 2=yc = 2 refer to 1 and yw = 3=yc = 3 refers to 1 . Thus, compared to the hot model, an additional section has to be added starting from line 11. For the following values: (lq = 6;lh = 1;lw = 1;lc = 1 andm = 2), the model generated by PRISM consists of 72859 states and 289147 transitions. The size of the model may mainly vary to the number of variables used in the module, as well as the range of their values. For instance, if we let the value ofj of warm and cold pools as the same as hot (i.e [0..1]), we had to introduce two new Boolean variables to replace the values 2 and 3 ofj. Such a solution could result in an additional large set of states. Figure 12: VM provisioning model for each cold PM[11]. 4.3 Specification In this section, we will show how we can specify quanti- tative properties in PRISM to reason about many measures of cloud performance through various operators employed by PRISM, which are the transient operatorP , the steady Modeling and Performance Analysis of Resource Provisioning in. . . Informatica 45 (2021) 529–541 535 1 //arrival and service rates 2 const double lambda; 3 const double mu; 4 // provisioning rates 5 const double betaH=1; 6 const double betaW=1/2; 7 const double betaC=1/3; 8 //max VMs deployed, time and global queu size 9 const m=2 ; 10 const double T; 11 const lq =6; 12 // buffer size hot, warm,cold 13 const lh=1; 14 const lw=1; 15 const lc=1; 16 17 const double deltaH=3; 18 const double deltaW=3; 19 const double deltaC=3; 20 // prob. off succes in hot, warm and cold 21 const double ph=0.9 ; 22 const double pw =0.8 ; 23 const double pc=0.7 ; 24 25 const double lamH =deltaH * (1-ph); 26 const double lamW=deltaW * (1-pw); 27 const double lamC =deltaC * (1-pc); 28 29 const double muH=deltaH * ph; 30 const double muW=deltaW * pw; 31 const double muC=deltaC * pc; 32 33 const double lambdaH = lambda/2; 34 const double lambdaW =lambda/4; 35 const double lambdaC =lambda/5; 36 37 const double gammaW =1; 38 const double gammaC=1; Figure 4: Global variables. Figure 5: Resource provisioning decision model[12]. operatorS and the reward operatorR. The model checking algorithm used during the analysis phase is Jacobi method, though, we can use other methods such as Gauss-Seidel method. We can use many variations in the model param- eters during the analysis, such as the number of PM’s, the number of VMs, arrival and service rates, etc. Since each PM is represented by a complete module, to ease the anal- ysis, we are going to fix the number of PMs, so no module duplication will be used. We can use the simulation framework of PRISM to pro- vide a detailed analysis based on these values. The differ- ent graphs to plot will be based on the variation of three main values, arrival rate , service rate and time variable T . All the values are considered in minutes. We will show that the main measures, job rejection probability and wait- ing time can be easily computed using probabilistic and reward properties. We will also show how to obtain addi- tional important measures. Before presenting these proper- ties, we should introduce some labels that are employed to express in a better way these properties. The set of labels that we are going to use are presented in Figure 13, and the set of rewards are presented in Figure 14. Job rejection probability As explained before, job re- jection could be at the level of the global queue, where the buffer size reaches its limit, or on the level of the pro- visioning module, where there is no sufficient resources, which means that all PMs queues are full (xh=lh & xw=lw &xc=lc). To obtain the rejection probability due to insuf- ficient capacity we use the following steady-state property : S =?["all_Pools_Full"] We fix the arrival rate by = 8, and we use different values of the mean service time to obtain the results pre- sented in Figure 15. From the Figure, we see that increas- ing the mean service time results in increasing job rejec- tion probability. It’s evident that taking more time to serve a request could result in rejecting new arriving requests. We can also use a steady property to estimate the long-run probability of the queue being more than 75% full, this in- teresting property results in 0:99 and can be expressed as the following:S =?[i=lq> 0:75]. Another important measure can be estimated using steady-state operator is the steady probability that the sys- tem is in full provision state (yh = 1&yw >= 1&yc >= 1), which means that in all pools, there is a request be- ing provisioned. This property is expressed as S = ?["all_Provision"] and returns a value of 0.94. We can reason on minimum and maximum delay time taken for provisioned requests before being served. To do so we use the following reachability reward properties that estimate the reward accumulated along a path until a certain state is reached. The time reward is denoted by "time" in Figure 14 (line 9), where every transition is counted. R"time" =?[F (j = 1&zh = 1)fj = 1&zh = 0gfmaxg] R"time" =?[F (j = 2&zw = 1)fj = 2&zw = 0gfmaxg] 536 Informatica 45 (2021) 529–541 H. Debbi 1 module rpdm 2 i: [0..lq]; 3 j:[0..3] init 0; 4 5 [] (i=0) &(j=0)-> lambda :(i’=i)&(j’=1); 6 [wait] (i lambda :(i’=i+1)&(j’=j); 7 [] (i lamh :(i’=i)&(j’=2); 8 [Provision_hot] (i>0 )& (i muH :(i’=i-1)&(j’=j); 9 [Provision_hot] (i=0)&(j=1) -> muH :(i’=0)&(j’=0); 10 11 [wait] (i lambda: (i’=i+1)&(j’=j); 12 [] (i lamw:(i’=i)&(j’=3); 13 [Provision_warm] (i>0 )&(i muW :(i’=i-1)&(j’=j-1); 14 [Provision_warm] (i=0)&(j=2) -> muW :(i’=0)&(j’=0); 15 16 [wait] (i lambda :(i’=i+1)&(j’=j); 17 [] (i>0 )&(i lamc :(i’=i-1)&(j’=j-2); 18 [Provision_cold] (i>0 )&(i muC :(i’=i-1)&(j’=j-2); 19 [Provision_cold] (i=0)&(j=3) -> muC :(i’=0)&(j’=0); 20 endmodule Figure 6: PRISM model for The RPDM module. 1 module vmpsm_hot 2 xh: [0..lh] init 0;// PM queue 3 yh: [0..1] init 0;// provision 4 zh: [0..m] init 0;// deployement 5 6 [Provision_hot] (xh=0) &(yh=0)&(j>=0)&(j<2)-> lambdaH :(yh’=1); 7 [Provision_hot] (xh lambdaH :(xh’=xh+1); 8 [] (xh>0) & (yh<1)&(j=1)-> lambdaH :(yh’=yh+1)& (xh’=xh-1); 9 [] (yh>0)& (zh betaH:(yh’=yh-1)&(zh’=zh+1); 10 [serve_hot] (zh>0)& (zh<=m)&(j=1)-> zh * mu:(zh’=zh-1); 11 [Reject_hot] (xh=lh) & (j=1) ->true; 12 endmodule Figure 7: PRISM model for hot PM. 1 module vmpsm_warm 2 xw: [0..lw] init 0;// PM queue 3 yw: [0..3] init 0;// provision 4 zw: [0..m] init 0;// deployement 5 6 [Provision_warm] (xw lambdaW :(xw’=xw+1); 7 [] (xw>0) & (yw<1)&(j=2)-> lambdaW :(yw’=yw+1)& (xw’=xw-1); 8 [] (yw>0)& (zw betaW:(yw’=yw-1)&(zw’=zw+1); 9 [serve_warm] (zw>0)& (zw<=m)&(j=2)-> zw * mu:(zw’=zw-1); 10 // provision steps different than hot 11 [Provision_warm] (xw=0) &(yw=0) &(zw=0)&(j=2)-> lambdaW :(yw’=2); 12 [Provision_warm] (xw lambdaW :(xw’=xw+1) & (yw’=2); 13 [] (xw deltaW :(xw’=xw) & (yw’=1); 14 [] (zw=0)& (yw=3)&(j=2)-> betaH:(yw’=yw-1)&(zw’=zw+1); 15 [serve_warm] (zw=1)& (yw=1)&(j=2)-> zw * mu:(zw’=zw-1) & (yw’=3); 16 17 [Reject_warm] (xw=lw) & (j=2)->true; 18 endmodule Figure 8: PRISM model for warm PM. Modeling and Performance Analysis of Resource Provisioning in. . . Informatica 45 (2021) 529–541 537 1 module vmpsm_cold 2 xc: [0..lc] init 0;// PM queue 3 yc: [0..3] init 0;// provision 4 zc: [0..m] init 0;// deployment 5 6 [Provision_cold] (xc lambdaC :(xc’=xc+1); 7 [] (xc>0) & (yc<1)&(j=3)-> lambdaC :(yc’=yc+1)& (xc’=xc-1); 8 [] (yc>0)& (zc betaC:(yc’=yc-1)&(zc’=zc+1); 9 [serve_cold] (zc>0)& (zc<=m)&(j=3)-> zc * mu:(zc’=zc-1); 10 // provision steps different than hot 11 [Provision_cold] (xc=0) &(yc=0) &(zc=0)&(j=3)-> lambdaC :(yc’=2); 12 [Provision_cold] (xc lambdaC :(xc’=xc+1) & (yc’=2); 13 [] (xw deltaC :(xc’=xc) & (yc’=1); 14 [] (zc=0)& (yc=3)&(j=3)-> betaH:(yc’=yc-1)&(zc’=zc+1); 15 [serve_cold] (zc=1)& (yc=1)&(j=3)-> zc * mu:(zc’=zc-1) & (yc’=3); 16 17 [Reject_cold] (xc=lc) & (j=3)->true; 18 endmodule Figure 9: PRISM model for cold PM. Figure 11: VM provisioning model for each warm PM[11]. label "deployed_Max_In_hot" = (zh =m & j=1); label "deployed_Max_In_warm" = (zw =m & j=2); label "deployed_Max_In_cold" = (zc =m & j=3); label "all_Provision"= (yh=1&yw>=1&yc>=1); label "all_Pools_Full" = (xh=lh &xw=lw & xc=lc); label "maximum_Deployment" = (zh=m & zw=m & zc=m); Figure 13: Labels. rewards "queue_size" true : i; endrewards rewards "Provision_queue_full" [Provision_hot](i=lq-1) : 1; [Provision_warm](i=lq-1) : 1; [Provision_cold](i=lq-1) : 1; endrewards rewards "time" true : 1; endrewards rewards "Waiting_Pools" true : xh + xw + xc; endrewards rewards "VMs_Deployed" true : zh + zw + zc; endrewards rewards "VMs_Deployed_Hot" true : zh; endrewards rewards "VMs_Deployed_Warm" true :zw; endrewards rewards "VMs_Deployed_Cold" true : zc; endrewards rewards "request_Reject_Warm" [Reject_warm]true: 1; endrewards Figure 14: Rewards. R"time" =?[F (j = 3&zc = 1)fj = 3&zc = 0gfmaxg] The properties estimate the reward that a state where a request is served can be reached starting from a state where the request is provisioned before being served. Roughly speaking, it computes the complete time between provi- sioning and service. For the hot pool, PRISM returns a 538 Informatica 45 (2021) 529–541 H. Debbi Figure 15: Job rejection probability. Figure 16: Probability of max deployment over time T. result of 3 time units, 15 for the warm pool and 37 for the cold pool. It is evident that the time taken for the request to be served in hot pool is much less than warm and cold, since the last pools require additional provisioning time, and the resource provisioning decision model tries to pro- vision the request in hot pool first. As we can compute maximum reward/probability, we can also compute mini- mum reward/probability using the feature of filter. For in- stance, we can compute the minimum probability of the global queue being not full, starting from the state where the queue has been already full. The property is presented as : P =?[trueU <=T (i0) : h_l + zh * v_a; 3 endrewards 4 rewards "Power_warm_PM" 5 (j=2 & xw=0 & yw=0 & zw=0) : w_l1; 6 (j=2 & (xw>=0 & xw<=lw) & yw=1 & zw=0) : w_l3; 7 (j=2 & (xw>=0 & xw<=lw) & yw=2 & zw=0) : w_l2; 8 (j=2 & (xw>=0 & xw<=lw) & yw=3 & zw=0) : h_l; 9 (j=2 & xw=0 & yw=0 &(zw>=1 & zw<=m) ) : h_l + zw * v_a; 10 (j=2 & (xw>=0 & xw<=lw) & yw=1 &(zw>=1 & zw<=m-1) ) : h_l + zw * v_a; 11 (j=2 & (xw>=0 & xw<=lw) & yw=0 & zw=m) : h_l + m * v_a; 12 endrewards 13 rewards "Power_cold_PM" 14 (j=3 & xc=0 & yc=0 & zw=0) : c_l1; 15 (j=3 & (xc>=0 & xc<=lc) & yc=1 & zc=0) : c_l3; 16 (j=3 & (xc>=0 & xc<=lc) & yc=2 & zc=0) : c_l2; 17 (j=3 & (xc>=0 & xc<=lc) & yc=3 & zc=0) : h_l; 18 (j=3 & xc=0 & yc=0 &(zc>=1 & zc<=m) ) : h_l + zc * v_a; 19 (j=3 & (xc>=0 & xc<=lc) & yc=1 &(zc>=1 & zc<=m-1) ) : h_l + zc * v_a; 20 (j=3 & (xc>=0 & xc<=lc) & yc=0 & zc=m) : h_l + m * v_a; 21 endrewards Figure 21: Power consumption rewards definition. 1 // Power hot pm 2 //power consumption in a hot PM (hl) 3 const double h_l=270; 4 //power consumption per VM 5 const double v_a = 16; 6 // Power warm pm 7 const double w_l1=54; 8 const double w_l2=100; 9 const double w_l3=135; 10 // Power cold pm 11 const double c_l1=0; 12 const double c_l2=50; 13 const double c_l3=108; Figure 22: Power consumption rates. Figure 23: Power Consumption. [2] BAIER, C., HAVERKORT, B., HERMANNS, H., AND KATOEN, J.-P. Model checking algorithms for continuous-time markov chains. IEEE Trans- actions on Software Engineering 29, 07 (2003), 524–541. https://doi.org/10.1109/tse. 2003.1205180. [3] BARHAM, P., DRAGOVIC, B., FRASER, K., HAND, S., HARRIS, T., HO, A., NEUGEBAUER, R., PRATT, I., AND WARFIELD, A. Xen and the art of virtualiza- tion. ACM SIGOPS Operating Systems Review 37, 05 (2003), 164–177. [4] BRADLEY, J. T., CLOTH, L., HAYDEN, R. A., KLOUL, L., REINECKE, P., SIEGLE, M., THOMAS, N., AND WOLTER, K. Resilience Assessment and Evaluation of Computing Systems. Springer, 2012, ch. Scalable Stochastic Modelling for Re- silience. https://doi.org/10.1007/ 978-3-642-29032-9. [5] BUYYA, R., YEO, C. S., VENUGOPAL, S., BROBERG, J., AND BRANDIC, I. Cloud com- puting and emerging it platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Computer Systems 25, 06 (2009), 599–616. https://doi.org/10. 1016/j.future.2008.12.001. [6] CHEN, P., XIA, Y., PANG, S., AND LI, J. A prob- abilistic model for performance analysis of cloud in- frastructures. concurrency and computation. Practice and Experience 27, 17 (2015), 4784–4796. https: //doi.org/10.1002/cpe.3462. Modeling and Performance Analysis of Resource Provisioning in. . . Informatica 45 (2021) 529–541 541 [7] DESHPANDE, P., SHARMA, S., AND PEDDOJU, S. Efficient multimedia data storage in cloud environ- ment. Informatica 39, 04 (2014), 431–442. [8] DUAN, Q. Cloud service performance evalua- tion: status, challenges, and opportunities – a sur- vey from the system modeling perspective. Digital Communications and Networks 03, 02 (2017), 101– 111. https://doi.org/10.1016/j.dcan. 2016.12.002. [9] EVANGELIDIS, A., D.PARKER, AND BAHSOON, R. Performance modelling and verification of cloud- based auto-scaling policies. Future Generation Com- puter Systems 87, 04 (2018), 629–638. https: //doi.org/10.1109/ccgrid.2017.39. [10] GHOSH, R. Scalable Stochastic Models for Cloud Services. PhD thesis, Duke University, 2012. [11] GHOSH, R., NAIKY, V., AND TRIVEDI, K. Power- performance trade-offs in iaas cloud: A scalable ana- lytic approach. In IEEE/IFIP 41st International Con- ference on Dependable Systems and Networks Work- shops (DSN-W) (2011), pp. 152–157. https:// doi.org/10.1109/dsnw.2011.5958802. [12] GHOSH, R., TRIVEDI, K., NAIK, V. K., AND KIM, D. End-to-end performability analysis for infrastructure-as-a-service cloud: An interacting stochastic models approach. In 2010 IEEE 16th Pa- cific Rim International Symposium on Dependable Computing (2010), pp. pp. 125–132. https:// doi.org/10.1109/prdc.2010.30. [13] HANSSON, H., AND JONSSON, B. logic for reason- ing about time and reliability. Formal aspects of Com- puting 6, 5 (1994), 512–535. [14] HINTON, A., KWIATKOWSKA, M., NORMAN, G., AND PARKER, D. Prism: A tool for automatic verification of probabilistic systems. In TACAS (2006), LNCS, vol. 3920, Springer, Berlin, Hei- delberg, pp. 441–444. https://doi.org/10. 1007/11691372_29. [15] JOHNSON, K., REED, S., AND CALINESCU, R. Specification and quantitative analysis of probabilis- tic cloud deployment patterns. In HVC (2012), LNCS, vol. 7261, Springer, Berlin, Heidelberg, pp. 145–159. https://doi.org/10.1007/ 978-3-642-34188-5_14. [16] KHAZAEI, H., MISIC, J., AND MISIC, B. Per- formance analysis of cloud computing centers us- ing m/g/m/m+r queuing systems. IEEE Trans- actions on Parallel and Distributed System 23, 05 (2012), 936–943. https://doi.org/10. 1109/tpds.2011.199. [17] KHAZAEI, H., MISIC, J., AND MISIC, V. A fine-grained performance model of cloud comput- ing centers. IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS 24, 11 (2013), 2138– 2147. https://doi.org/10.1109/tpds. 2012.280. [18] KIKUCHI, S., AND MATSUMOTO, Y. Performance modeling of concurrent live migration operations in cloud computing systems using prism probabilistic model checker. In IEEE 4th International Conference on Cloud Computing (2011), pp. 49–56. https: //doi.org/10.1109/cloud.2011.48. [19] LI, Z., ZHANG, H., OBRIEN, L., CAI, R., AND FLIN, S. On evaluating commercial cloud services: A systematic review. Journal of Systems and Software 86, 09 (2013), 2371–2393. https://doi.org/ 10.1016/j.jss.2013.04.021. [20] LI, Z., ZHANG, H., OBRIEN, L., CAI, R., AND FLIN, S. Stochastic modeling and quality evaluation of infrastructure-as-a-service clouds. IEEE Trans- actions on Automation Science and Engineering 12, 01 (2015), 162–170. https://doi.org/10. 1109/tase.2013.2276477. [21] MAHFOUD, Z., AND NOUALI-TABOUDJEMAT, N. Consistency in cloud-based database systems. Infor- matica 43, 03 (2019), 313–320. https://doi. org/10.31449/inf.v43i1.2650. [22] PONNURAMU, V., AND TAMILSELVAN, L. Secured storage for dynamic data in cloud. Informatica 40, 01 (2016), 53–62. [23] VAQUERO, L., RODERO-MERINO, L., CACERES, J., AND LINDNERS, M. A break in the clouds: to- wards a cloud definition. ACM SIGCOMM Com- puter Communication Review 39, 01 (2009), 50– 55. https://doi.org/10.1145/1496091. 1496100. [24] WIDED, A., AND OKBA, K. A novel agent based load balancing model for maximizing re- source utilization in grid computing. Informatica 43, 03 (2019), 355–262. https://doi.org/10. 31449/inf.v43i3.2944. 542 Informatica 45 (2021) 529–541 H. Debbi