https://doi.or g/10.31449/inf.v47i6.4622 Informatica 47 (2023) 75–96 75 ASM-based Formal Model for Analysing Clou d Auto-Scaling Mechanisms Ebenezer Komla Gavua 1 , Gabor Kecskemeti 2 1 Institute of Information T echnology , Miskolc-Egyetemvaros, 3515, Miskolc, Hungary 1 Department of Computer Science, Koforidua T echnical University , Koforidua, Ghana 2 Department of Computer Science, Liverpool John Moores University , Liverpool, UK E-mail: gavua@iit.uni-miskolc.hu, g.kecskemeti@ljmu.ac.uk Keywords: auto-scaling, abstract state machines, cloud computing algorithms; formal modelling Received: January 18, 2023 The pr ovision of r esour ces to meet workloads demands has become a crucial r esponsibility for auto-scaling mechanisms (auto-scalers) on cloud infrastructur es. However , implementing auto-scaling mechanisms on cloud frameworks has pr esented numer ous technical challenges. A typical challenge is that, these auto- scalers ar e often designed on differ ent cloud systems making their evaluation, comparisons and wider applicability pr oblematic. T o addr ess this issue, we pr opose an Abstract State Machine (ASM) model as a solution. Our ASM model was developed systematically accor ding to the behaviours of several auto- scalers, covering the necessary system pr ocesses. Rigor ous validation and evaluation of our model have been conducted using the Cor eASM Model Checker . The r esults demonstrate that our model can effectively analyze and generate accurate ASM r efinements for auto-scalers, even without the need for r eal-life exper - iments. Our model, ther efor e, pr ovides the platform to evaluate the behaviours of algorithms executed on clouds. Povzetek: Razvit je model ASM, ki analizira in generira izboljšave ASM za avtomatske skalirnike. 1 Intr oduction The dynamic provisioning of computational resources has emer ged as a critical objective for many cloud applications designers. T o achieve this, auto-scaling mechanisms (auto- scalers) are employed to ensure that resources ef fectively meet workload demands while upholding the reliability of virtual infrastructures [1, 2]. Research has identified many challenges with auto-scalers [3, 5]. These challenges pre- dominantly stem from limited understanding of the behav- iors exhibited by auto-scalers, particularly when they are developed across dif ferent frameworks. In this paper , we advocate the use of Abstract State Machines (ASMs [8]) as a mathematically well-founded framework for analyzing and comparing auto-scalers de- signed on dif ferent cloud systems. ASMs, initially intro- duced by Gurevich as evolving algebras [4], have proven successful in cloud systems for formally designing adap- tivity components [22]. The main contribution of this work is to introduce new ways of analysing and comparing auto-scalers designed on dif ferent clouds. The modelling process of our ASM model is presented in five steps. These are (i) design and analy- sis of the framework of our model. (ii) design and imple- mentation of five ASM transition rules to reflect typical job execution phases. (iii) comparisons of auto-scalers of fered alongside the DISSECT -CF cloud simulator [10], with our transition rules. (iv) validation of our model with test cases created from existing auto-scalers. (v) evaluation of our model with our transition rules, ASM refinement method, and evaluation goals. T o accomplish these steps, first, we created the blueprint of our model while detailing state tran- sitions during job processing. This blueprint comprises of a framework that represents categories of auto-scalers. Sec- ond, we described the details of our ASM rules and how they were implemented to reflect our model. Third, we ex- amined algorithms developed from available auto-scalers to identify similar behaviours among them. Fourth, we vali- dated test cases developed from available auto-scalers. The validation processes were accomplished with goals created from our model’ s transition rules. Our model was checked and validated with test cases using the CoreASM Model Checking T ool. Fifth, we evaluated our model with criteria developed from ASM definitions and methods to highlight the ef ficiency of our model. The results of our validation and evaluation demonstrate that our model provides valuable insights into the behavior of auto-scalers, even without the need for real-life or sim- ulated experiments. It of fers a robust approach to analyze and compare auto-scalers designed for dif ferent cloud sys- tems. The remaining sections of this paper are structured as fol- lows: In Section 2, we review relevant research on auto- scaling techniques and the application of ASMs in cloud and distributed systems. Section 3 presents our methodol- ogy for analysing these techniques. W e then validate and evaluate the results of our modeling through ASM simula- tions in Section 4. Finally , in Section 5, we conclude the 76 Informatica 47 (2023) 75–96 E.K. Gavua et al. paper and provide recommendations for future work. 2 Related works and backgr ound This section discusses past research ef forts to provision re- sources during auto-scaling, and the application of ASM on distributed and cloud systems. 2.1 Overview of auto-scaling r esear ch The quest for auto-scaling of computing resources on clouds, has been due to deviations in expected resources versus actual resource usage [2, 13]. This deviation was analysed by [3], and in their work, auto-scaling techniques were classified into demand-oriented categories. These works propelled research activities into the provision of cloud resources to meet workload demands. Ghanbari et al. [1 1] employed a stochastic, Model Pre- dictive Control problem (MPC) technique to formulate an auto-scaling approach that exploits the trade-of f be- tween performance-related objectives and cost minimiza- tion. Y ang et al. [7] investigated the problem of cost- aware auto-scaling along with predicted workloads in ser - vice clouds. They proposed an approach to scale service clouds in both real-time scaling and pre-scaling modes. Gandhi et al. [12] proposed a new cloud service, Depend- able Compute Cloud (DC2), that automatically scales user applications in a cost-ef fective manner to provide perfor - mance guarantees. DC2 determines scaling actions for an application deployed in the cloud. Saxena et al. [14] pro- posed an integrated proactive auto-scaling and allocation of VMs approach. The solution allows load consolidation on few ener gy-ef ficient physical machines without af fecting user application performance. Al-Dulaimy et al. [15] pro- posed a Service Level Agreement provisioning approach (MUL TISCALER) that aims at the control of the contention and scaling of resources amongst co-hosted VMs. MUL TI- SCALER handles changes in workloads auto-scaling in the presence of noisy neighbours. Ullah et al. [16] proposed a Cartesian genetic programming (CPG) based neural net- work (ANN) for resource utilisation estimation. The pro- posed system utilises a rule-based scaling system for elastic scaling of cloud resources. Most of the auto-scaling research discussed above used statistical and experimental procedures. Less attention have been given to devising a flexible and formal approach [17] (such as ASMs) for evaluating auto-scalers. Let us now dis- cuss the application of ASMs in clouds and other distributed systems. 2.2 Prior art with ASMs for clouds and other distributed systems A few auto-scaling works have been undertaken relating to ASM modelling. LakshmiPriya et al. [19] proposed a for - mal framework based on ASMs, for specifying and defining an autonomous network layer grid. The model serves as a guideline to identify the minimum functionalities required of a grid. Bianchi et al. [20] proposed an ASM model to rep- resent the standard mechanisms defined in Open Grid Ser - vice Architecture (OGSA) for job management and execu- tion capability . The approach describes the components of a grid system, dynamical properties and relations between them in a service-oriented view . Bianchi et al. [21] pro- posed a formal framework for job execution management in grid systems and implemented it on the coreASM tool. The framework expresses the composition of interopera- ble, always refineable building blocks, which is an ef fec- tive choice for defining a precise semantic foundation of a grid system. Arcaini et al. [22] proposed a ASM solution to tackle the problem of making cloud services usable to dif ferent end-devices. The framework consists of a server that intercepts requests from the clients and forwards them to the cloud. The above discussion demonstrates limited research re- lating to formalizing auto-scalers. Thus we set out to devise a formal ASM model, which allows comparison of auto- scalers. But first, let us carry out a comparative analysis of the above related works with our proposed solution. 2.3 Comparative discussion of overview of r elated works This section presents the comparative analyses of the re- search activities discussed in sub-sections 2.1 and 2.2 with our proposed approach. T able 1 discusses the summary of the results of the overview of the auto-scaling approaches. Ghanbari et al. [1 1] formulated an approach that exploits the trade-of f between performance-related objectives and cost minimization. However , the technique experiences challenges in resource provision due to delays associated with boot-up, running the initial installation scripts, and the initial warm-up. Also, the algorithms utilised have not been made public and not suf ficiently analyse to foster compre- hension and improvement. Therefore, an approach which allows in-depth analyses and comparisons of scaling algo- rithms will foster the ef ficient evaluation of auto-scaling ap- proaches. Y ang et al. [7] investigated the problem of cost- aware auto-scaling along with predicted workloads in ser - vice clouds. However , the approach is only applicable to service clouds. This inherent challenge limits the strategy’ s extension to several cloud platforms. Gandhi et al. [12] pro- posed DC2 that scales the infrastructure to meet the user - specified performance requirements. However , the method applied does not of fer optimal estimates of the state of pro- cesses. Therefore, an approach that models the state tran- sition of processes will allow users to evaluate state transi- tions during job processing. Saxena et al. [14] developed an integrated proactive re- source provisioning and allocation approach. However , the approach requires further work on tasks prediction and scheduling of VMs to reduce network traf fic. Therefore, an approach that allows the modelling of the auto-scaling ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 77 Auto-Scaling Appr oaches Results Design Deficiency / Up- grade Suitable for Analysis and Adaptability Cost Minization [1 1] This approach models appli- cation dynamics in clouds via the MPC technique. This approach experiences delays linked with boot-up, running the initial installa- tion and warm-up. The shortfalls identified in this approach with resource provision does not foster ex- tension to other platforms. W orkloads Prediction [7] This approach predicts workload to scale virtual re- sources at dif ferent resource levels in service clouds. Key state transitions during resource provision are omit- ted in the algorithms. The design is limited to only service clouds and not ex- tensible to other cloud plat- forms. DC2 Approach [12] DC2 scales the infras- tructure to meet the user - specified performance requirements. The service time estimated at runtime becomes prob- lematic with some work- loads. This approach lacks opti- mal estimates of process states which prevents in- depth analysis. Proactive Auto-Scaler [14] This approach consolidates load on few PMs without af- fecting user application per - formance. T asks are scheduled on VMs which are distant. This causes excess network traf- fic, resulting in high ener gy usage. The VMs locations af fects resources provisions evalua- tion. Also, the algorithms are analysed into details to foster extension. MUL TISCALER Approach [15] MUL TISCALER allocates resources to VMs based on the SLA requirements. Only vertical scaling is ap- plied to meet applications performance goals by as- signing the resources re- quired. The skewed nature of this approach af fects its applica- bility to several situations. Resource Estimation [16] This approach estimates re- sources with recurrent CGP and ANN. This strategy is designed with of fline evolvability and coarse-grained scaling mak- ing it inaccessible. The scaling algorithms are not analysed and integrated to workloads analysis, which is inimical to extension. T able 1: Summary results of overview of related works. of resources and the scheduling of VMs will improve the current design. Al-Dulaimy et al. [15] developed a novel Multi-Loop Control approach to allocate resources to VMs based on Service Level Agreements (SLA). However , their approach is limited to the provision of platform metrics such as CPU utilisation as input for scaling. Therefore, an approach that promotes the modelling of hybrid scal- ing will help service providers to design their platforms to meet the demands of a lar ger section of users. Ullah et al. [16] proposed a Cartesian genetic programming based neural network for resource utilisation estimation. How- ever , the method utilized is not integrated with predictive scaling mechanisms for the analysis of workloads. There- fore, an approach that is capable of analysing auto-scalers with emphasis on VMs provisions, will enable authors to evaluate the shortfalls in their approach, for the upgrade of their current design. Furthermore, table 2 discuss the summary of results of the state-of-the-art applications of ASM to clouds and other distributed systems discussed in sub-section 2.2. LakshmiPriya et al. [19] developed a formal framework for an autonomous Network-Infrastructure for grids. How- ever , the authors did not include validation techniques and refinement schemes for grids. Therefore, a model with flex- ible transition rules that includes formal framework with validation and refinement schemes will foster the applica- tion the modelling and validation processes to grids. Bianchi et al. [20] utilized ASM modelling to study Grid systems as a composition of interoperable building blocks. However , the architectural specifications provided did not capture user requirements for performance monitor - ing. Therefore, a model that provides ASM refinements on user service requests and response for vertical and horizon- tal scaling will be essentially required for model adaptabil- ity and enhancements. Bianchi et al. [21] also developed an ASM-based model for grid job management. However , the resource dispatch- ing policy of the model requires further works. Therefore, an model that focuses on resources provisions behaviours and allows the comparisons of several situations will enable researchers and practitioners to evaluate all aspects of dis- tributing computing and to provide the upgrades required. Arcaini et al. [22] employed ASM to formally analyse a Client-Server (CS) adaptivity component for clouds. How- ever , their design was limited to communications between client-server applications. Extensions were not provided to auto-scaling mechanisms. Therefore, a model that focuses on the auto-scaling of resources during job processing will allow users to examine their work for improvement. 78 Informatica 47 (2023) 75–96 E.K. Gavua et al. ASMs on Clouds & Distributed Systems Results Design Deficiency / Up- grade Suitable for Adapting to Other Frameworks Autonomous Network- Infrastructure [19] A formal framework for the minimum functionalities re- quirements for grids was proposed. Model validation techniques and refinements schemes are unavailable. This framework is not suit- able for modelling resource provision behaviours in grids and clouds. Grid Systems [20] ASM was utilised to model the standard mechanisms de- fined in OGSA for job man- agement and execution ca- pability . Complete architectural spec- ification with requirements for grids to foster adaptabil- ity is unavailable. The incomplete specifica- tions in this approach makes the framework unadaptable to architectures. Grid Job Management. [21] A formal framework for job execution management in grid systems was developed. The resource allocation pol- icy which monitors resource provisions is incomplete. The deficiencies in this ap- proach makes it unadaptable to the frameworks of other distributed systems. Client-Server Adaptivity Component. [22] A formal framework was de- veloped for cloud service provisioning to dif ferent de- vices with dif ferent profiles. The design was limited to CS applications interactions. The Auto-Scaling of Re- sources on clouds was not considered. The transition rules are not formalized to foster the flex- ible adaptation of the frame- work to cloud auto-scalers. Proposed Model A formal framework capable of analysing the virtual ma- chine provision behaviours of auto-scaling mechanisms. Model validation techniques and refinements schemes are available. Complete archi- tectural specification with requirements for clouds. This approach allows adop- tion of auto-scalers with ex- tra features besides vertical and horizontal scaling to fos- ter their evaluation. T able 2: Summary results of overview of related works continuation co nd 1 co nd n rule 1 rule n j 1 . . . . ifctl_state = i the n ifcond 1 the n rule 1 ctl_state:= j 1 . . . ifcond n the n rule n ctl_state:= j n j n i Figure 1: Control state ASMs 2.4 Abstract state machine theory This sub-section reviews the theoretical background for ASMs. The ASM theory encompasses a formal system en- gineering technique that guides software development. 2.4.1 Abstract state machines Abstract State Machines (ASM) are systems based on the concept of state transitions. They represent the rapid con- figurations of a system under development with transition rules. ASM transition rules express how function inter - pretations are modified from one state to another to reflect system changes. The basic form of a transition rule is the guar ded update : “ if condition then updates ”, where up- dates is a set of function of the form f(t 1 ,...,t n ) := t . These updates are executed when a condition is true. Definition 1. A Contr ol State ASM is a given contr ol state i , wher e only one of the conditions cond k can be true for all1≤ k≤ n . If the machine executesrule k andcond k to true. It changes the contr ol state fr omi toj k . These ASMs ar e mostly applied in the ASM r efinement method. 2.4.2 The ASM r efinement method The ASM refinement method is a stepwise refinement for crossing levels of abstraction. This method links models through well-documented incremental development steps. The steps start from ground models and turn them piece- meal into executable codes [23, 24]. Now , let us define a theorem for checking equivalence in our model. Definition 2. Bör ger ’ s refinement : Given a notion ≡ of equivalence, an ASMM ∗ is a corr ect r efinement of an ASM M if and only if, for each M ∗ -run S 0 ∗ , S 1 ∗ ,…, ther e is an M -run S 0 , S 1 , …and sequences i 0 ≤ i 1 ≤ ... and j 0 ≤ j 1 ≤ ... such thati 0 =j 0 = 0 andS ik ≡ S jk for each k and either , as seen in figur e 3. ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 79 Figure 2: Architectural view of Auto-Scaling Mechanisms (ASMs) on DISSECT -CF . S 0 S 1 S 0 * S 1 * ≡ ≡ S 3 M M * S 2 S 2 * S 4 S 5 S 3 * S 4 * S 5 * S6 * ≡ ≡ Figure 3: Bor ger ’ s refinement 2.4.3 Gr ound model, universes and signatur es A gr ound model is a rigorous high-level system blueprint specification using domain-specific terms. All stakehold- ers can understand this model as it reflects the initial re- quirements and removes ambiguities of the initial textual conditions. The ground model is designed with universes and signatur es . ASM depicts universes as basic sets with functions and relations. These sets require signatur es for modelling state transitions. A signature is a finite set of function names, each of fixed arity . Now let’ s discuss our model’ s design in the next section. 3 Methodology This section discusses our ASM model developed accord- ing to the following goals. First, we review the auto- scalers of fered alongside DISSECT -CF . Second, we discuss our ground model, universe and signatures developed fol- lowing the ground model discussion in sub-section 2.4.3. Third, we discuss our model’ s ASM functions developed per definition 1. Fourth, we discuss our model’ s develop- ment process per method 2.4.2 while comparing the cate- gories of auto-scalers. 3.1 Auto-scalers on DISSECT -CF This sub-section discusses the auto-scalers whose be- haviours were utilized to establish our model. Many auto- scalers are evaluated through simulations. So, we have in- vestigated one such simulation environment based on the DISSECT -CF simulator . W e chose it as it has been shown through research to be ef ficient for auto-scaling experi- ments. In our model building, we have examined the sim- ulator ’ s auto-scaling related examples 1 . The chosen examples were built on several components. The auto-scalers observed can be grouped into two cate- 1 available at https://github.com/kecskemeti/ dissect- cf- example s and at https://github.com/kecskemeti/ dcf- exercises gories (i.e. simple and multimode auto-scalers). The sim- ple auto-scalers respond to demands by either increasing or decreasing the VM instance counts. The scaling ad- justments ensure that the quantity of VMs instances meets workload demands. The multimode auto-scalers also ex- hibit simple auto-scaler features. Furthermore, the multi- mode auto-scalers monitor the VM counts during scaling operations, which also influences the schedule resulting in the utilization of VMs. All auto-scalers are founded on a handful of classes including the V irtual Infrastructure (VI), JobArrivalHandler , BasicJobScheduler (BJS), GenericT ra- ceProducer (GTP) and Simscaler . VIs have the dedicated role of managing VMs belonging to particular applications. JobArrivalHandlers abstract the application model with the help of replaying customizable parts of pre-recorded workload traces. BasicJobScheduler combines with the job arrival handler functionality to pro- cess jobs. JobLaunchers and JobT oVmSchedulers focus on the model for cluster scheduling techniques over the VMs of fered by a particular VI. Now let’ s discuss the auto-scalers of fered with the simu- lator: Thr esholdBasedVI Mechanism is governed by a lower and an upper threshold. It observes VM utilisation and makes decisions based on how it relates to the two thresholds. It removes VMs not used to some extent to the lower threshold. In contrast, it adds new VMs when most of the VMs in the managed infrastructure are utilised more than the upper threshold. VMCr eationPriorityBasedVI Mechanism is a variation of the above approach, by anticipating growth in the infrastructure utilisation. It focuses on creating VMs mainly and only removes VMs as a last resort. PoolingVI Mechanism is designed to keep a given num- ber of completely unused VMs for newly arriving jobs. Hence, it can accept a new job anytime. VMOptimisationBased Mechanism allows VMs created for one kind of executable to be repurposed to execute others, fostering VM reuse. FixedVM Mechanism is designed to provision VMs for scaling jobs at minimal system resources. It uti- lizes a scaling mechanism (simscaler) on a production cloud infrastructure. The simscaler combines with the GenericT raceProducer to provision VMs for jobs. 80 Informatica 47 (2023) 75–96 E.K. Gavua et al. Figure 4: Basic elements of the ASM model for Auto- Scaling For ease of discussion, the above mechanisms will be referred to as Threshold, Vmopt, Vmcreate, Pooling and FixedVM. 3.2 Model design This sub-section discusses the modelling processes of our approach. This is presented in five design stages: Design and Analysis of the model’ s framework as dis- played in figures 4 and 5. The framework shows our model’ s ground model for the two categories of auto- scalers. Figure 4 shows the basic elements ( universes interacting with signatur es with arrows) utilised in de- signing our model. The arrows represent the relations between the signatur es and the universes while pro- visioning resources during multimode or simple auto- scaling. The signatur es are declared through func- tion created in accordance with sub-section 2.4.3. Fig- ure 5 shows universes interacting with unidirectional and bidirectional arrows. The bidirectional arrows represents information flow between universes while the unidirectional arrow represent the expected state changes during ASM runs. Design and implement the model’ s ASM T ransition Rules to reflect the job execution phases. Five ASM rules were defined and discussed in conjunction with the ASM method 2.4.2 and definitions 1 and 2. Compare algorithms from the two categories of auto- scalers of fered with DISSECT -CF , with T ransition Rules . This step was modelled simultaneously with the previous step to ensure model coherence. Model V alidation with validation goals on test cases cre- ated from existing auto-scalers. The test cases are ab- stracted from the formalized algorithms of our auto- scalers to determine if the algorithms satisfy the re- quirements of our ground model. Evaluation of the model with the T ransition Rules and evaluation goals. This process was achieved in con- junction with the ASM refinement method (an ASM benchmark). The evaluation goals were employed to foster the applicability of our model to existing auto- scalers and to foster their equivalence to our ground model. The evaluation goals were selected in ac- cordance to our transition rules and the control state ASMs. Now let’ s describe our identified universes: The JOBHANDLER is the universe that processes traces and sends its jobs to a joblauncher in the multimode auto-scaling mechanisms. In the simple auto-scalers, it is in char ge of sending jobs to VMs for processing. The JOBLAUNCHER is the universe that emits jobs for processing for the multimode auto-scalers. This deals with the ordering and timing of new jobs before they are released for processing. A JOB The data submitted by a Jobhandler to be executed on a node. It contains binaries of an application, li- braries and resource descriptions. The ARESOURCE represent the major resources re- quired for job processing. These include virtual infras- tructures, cloud service, and hardware disk require- ments. Dif ferent categories of resources (i.e. hetero- geneous nodes) are also part of Ar esour ces . The TIME The duration a submitted job must spend being processed by virtual machines. This is usually mea- sured in seconds. The VM The virtual machine required for processing jobs in an auto-scaled infrastructure. The VI This universe is responsible for managing VMs for applications in multimode environments. The PROCESS This universe is responsible for ensur - ing that installed tasks receive the necessary attention from the Ar esour ces and the VM. The SER VICE This universe is responsible for service provision in multimode environments. Services are supplied per user requests at specific times on service clouds. The SIMSCALER This universe is responsible for ensur - ing basic scaling activities in simple auto-scaled envi- ronments. ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 81 Figure 5: Ground model for ASM auto-scaling Submitted Running Waiting Done Failed Figure 6: Job state transitions The BASICJOBSCHEDULER utilises clustering pat- terns to monitor VMs for simple auto-scalers. The GENERICTRACEPRODUCER provisions sets of jobs for processing for specific durations in simple auto-scaled environments. 3.3 ASM functions Our ASM functions and corresponding state diagrams are depicted in tables 3 and figures 7 and 6 respectively . JobState depicts the state transitions of job during data Figure 7: Process state transitions processing. Jobs’ states transition from submitted to either done or failed as shown in figure 6. JobT ime depicts periods reflective of job states during task processing. It combines with JobState to describe at what period a particular state change occurred. Pr ocessState illustrates process state transitions from new to stopped during job processing as shown in figure 7. JobRequest invokes jobs generation which are mapped to VMs for task processing. It combines with pr ocess- Request to maintain a job and process requests during job initialising and handling. 82 Informatica 47 (2023) 75–96 E.K. Gavua et al. MappedVM monitors the state of VMs and jobs connec- tion for job processing. It combines with MappedJob to maintain the link between jobs and VMs. Belongsto ensures that there is enough aresources to sup- port a VM before it is selected. Compatible ensures that the VM selected is the appropriate one. This is done to prevent the selection of VMs with less utilisa- tion which can be destroy within a short period. AddVM combines with Compatible , and BelongsT o to fos- ter VMs selection during job queuing. Destr oyVM is activated by auto-scalers to monitor VM utilisation and to remove unused VMs. Additionaly , it is used by certain auto-scalers to monitor the dura- tion VM utilisation. SystemRequest is the refinement for ProcessRequest and JobRequest. ReqResour ces is the refinement for MappedVM and MappedJob. JobPr ocessing is the refinement function for the provision and monitoring of the vital portion of the job handling. It ensures that suf ficient time is allocated for tasks. It also models the outputs of job processing. VMCount is applied in the queuing phase to monitors the number of VMs provisioned for task processing. InitReslist and QueReslist are the refinements for the pro- vision and monitoring of the universes and functions required for the first and second phases of our model. SystemState is a the refinement for Pr ocessState , JobState , and JobT ime to reflect system state changes. VMRequest is the refinement for the VM selection process during job queuing. InitReqFunctions is the refinement for the provision and monitoring of the universes and functions required for the second phase (job initialising) of our model. JobHandReslist is the refinement for the provision and monitoring of universes and functions required for the fourth phase of our model. It combines with a derived function called jobhandling module to process jobs. Auto-scaler design is focused on optimizing metrics about the virtual infrastructure. Functions designed to model these metrics are described as follows. TLevel defines the VMs threshold required for certain auto-scalers. The threshold could be t min , t avg , or t max for minimum, average and maximum thresholds respectively . VMUL defines VM utilization levels during job processing. The VM utilization levels could beVMut min ,VMut avg , orVMut max . VMPool defines VM provisions in VM pools. Also, VM- Pool implements R VM to monitor VM optimisation levels for reusable VMs. The quantity of VMs in the pool could be q min ,q avg orq max for minimum, av- erage and maximum quantities respectively . VMPost defines VMs’ position in the VI during job pro- cessing. VMs positions could be vm f ,vm l for first and last positions which depicts the particular vir - tual machine that is being monitored by certain auto- scalers. These auto-scalers destroy VMs with less util- isation, unless the VM is the last one to be processed. These functions and universes were combined to create the algorithms in our model. 3.4 Comparison between multimode and simple mechanisms Our ASM model comprises of five T ransition Rules . These rules are designed to reflect the execution phases an auto- scaler under goes during job processing. The rules enable users to analyse the VM provision behaviours of auto- scaling mechanisms. W e utilised algorithms to express the details of our gr ound model shown in figure 5. These algo- rithms were further refined according to the ASM refine- ment method into lower levels of abstractions. Our ground model and the refinements are later compared for equiva- lence according to Bör ger ’ s r efinement to check for the con- sistency of state transitions. The ASM T ransition rules are: (i) Initial Phase(ii) Job Initialising(iii) Job Queuing(iv) Job Handling and(v) Job T ermination. The initial phase is the first transition rule of our model. This is the phase where all requisite resources are availed for job processing to commence. The system state is idle in this phase. The job initialising phase is the stage where job processing commences with the activation of system requests, and the mapping of jobs to VMs. The system state transitions to active in this phase. The job queuing phase is the stage where jobs queue due to the unavailabil- ity of VMs. The system state transitions to waiting in this phase. The job handling stages is the actual job processing stage where all the requisite resources are availed and jobs are processed till completion. The system state transitions to busy in this phase. The job termination phase is the fi- nal phase of our transition rules. This is the stage where all upload jobs are completely processed or a system interrupt causes job processing to halt. The system state transitions to either done or stopped in this phase. The ASM rules are described in conjunction with algo- rithms 1 to 15 to identify the similarities existing between auto-scalers developed from dif ferent frameworks. Also, derived functions (ASM modules) were developed and ap- plied to the rules of our model to ensure modularisation. Let us discuss our model’ s rules in the next sub-section. ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 83 JobState: Job→ {idle ,submitted ,waiting ,running ,failed ,done } JobT ime: T ime→ {idle ,started ,processing ,stopped ,completed } ProcessState: Process→ {new ,ready ,waiting ,running ,stopped } SystemRequest: Request× AResource→ {true ,false } SystemState: InfraState→ {idle ,active ,waiting ,busy ,stopped ,done } JobOutcome: Job→ {success ,failure } Compatible: Select(attr(j),attr(vm))→ {undef ,true ,false } AddVM: VM× Job→ {undef ,true ,false } MappedJob: Job× VM→ {undef ,true ,false } MappedVM: Job× Process→ {undef ,true ,false } ReqResources: SystemRequest× AResource→ {undef ,true ,false } JobRequest: Job× AResource→ {undef ,true ,false } ProcessRequest:Process× AResource→ {undef ,true ,false } Event: T ask→ {start ,aborted ,terminated } InitReslist: IReslist→ {IRL active ,IRL idle ,IRL busy } QueReslist: QRlist→ {QRL active ,QRL idle ,QRL busy } JobHandReslist: JobhReslist→ {JHRL active ,JHRL idle ,JHRL busy } InitReqFunctions: InitReqFun→ {IRF active ,IRF idle ,IRF busy } JobProcessing: Jobproc→ {JP active ,JP idle ,JP busy } Job: Process→ Job Jobhandler: Job→ Joblauncher , Job→ VM Submitted: Job× VM→ {undef ,true ,false } BelongsT o: AResource× VM→ {undef ,true ,false } DestroyVm: VM→ {undef ,true ,false } ThresholdLevel: TLevel→ {undef ,T min ,T avg ,T max } VmPosition: VMPost→ {undef ,VM F ,VM L } ReusableVm: R VM→ {undef ,Q min ,Q avg ,Q max } VmPool: Vmpool→ {undef ,Q min ,Q avg ,Q max } VMCount: NumofVMs→ {Num min ,Num avg ,Num max } VmUtilLevel: VmUL→ {undef ,UtVM min ,UtVM avg ,UtVM max } SimulationDuration: SimDur→ {SD min ,SD avg ,SD max } A veragQueT ime: A vgQT→ {AQT min ,AQT avg ,AQT max } A veragUtilPM: A vgUPM→ {AUPM min ,AUPM avg ,AUPM max } T able 3: List of ASM functions 3.4.1 Rule 1, initial phase Algorithms 1 and 2 depict the first phase of our model, for both Simple and Multimode auto-scalers as seen in figure 5. At this phase, all universes are provisioned for job pro- cessing to commence, however the process state is updated to idle as seen in lines 1 to 2 of algorithms 1 and 2. The system is inactive due to the absence of an ASM rule that initialises job processing. The Simple auto-scaler utilises the SimScaler (j,vm), BJS (j,vm) and GTP (j) to monitor jobs and VMs provisions; while the Multimode auto-scaler applies the VI (j, vm) and the joblauncher to do same as seen in lines 4. Also, jobs and process requests are acti- vated but no response is received. Jobs are not submitted to VMs, but the VMs remain unmapped. The Multimode auto-scalers activate specific functions to monitor key in- dicators during auto-scaling as seen in lines 13 to 15 of al- gorithm 2. However , in the absence of job processing, they are all updated to undef . Algorithms 1 and 2 are refined in algorithm 3. Initial phase r efinement: The InitReslist function is utilised to check for the provision of universes for this phase. InitReslist is a refinement for all required universes and functions for this phase. Systemstate is updated to idle as seen in lines 2. Since there are no activities at this stage. Systemr equests and ReqResour ces are mapped to false , as jobs are not submitted to VMs. Also, jobs and VMs are not installed as tasks. This causes systemstate to remain up- dated to idle . This refinement is equivalent to our ground model’ s algorithms discussed in algorithms 1 and 2. As the state changes of algorithm 3 are equivalent to the state tran- sitions of our model. 3.4.2 Rule 2, job initialising The second phase of our model (shown in figure 5) be- gins with a system call activated by the application of an ASM contr ol state rule. The universes provisioned from the previous phase are assigned. This transitions pr o- cessState from new to r eady as seen in lines 2 of our 84 Informatica 47 (2023) 75–96 E.K. Gavua et al. Algorithm 1Simple Initial Phase 1: if ∃ vm ∈ VM ∧∃ p ∈ PROCESS ∧∃ ar ∈ ARESOURCE∧∃ j∈ JOB∧∃ t∈ Time then 2: processState(p) :=idle 3: end if 4: while SimScaler(j,vm ) ∧ BJS(j,vm ) ∧ GTP(j) do 5: if jobRequest(j,ar ) = true ∧ processRequest(p,ar ) =true then 6: JobTime(j) :=idle 7: end if 8: if mappedVM(j,p ) = false ∧ mappedJob(j,p ) =false then 9: JobTime(j) :=idle 10: end if 1 1: if installed(j,vm ) = false ∧ Jobhandler(j,vm ) =undef then 12: JobState(j) := idle∧ JobTime(j) := idle 13: end if 14: end while ground model algorithms 4 and 5. Specific universes are provisioned to monitor the activities of jobs and VM in line 4. The Simple auto-scalers utilise SimScaler (j,vm), BJS (j,vm) and GTP (j); while Multimode auto-scalers ap- ply VI (j,vm) and the joblauncher . JobRequests and pr o- cessRequests are activated to connect VMs to Jobs. Job- time transitions to started . Jobs are mapped to VMs and installed as tasks as seen in lines 6 to 1 1. The jobhan- dler is activated to process the tasks in the Simple scalers whilst the joblauncher is activated for the Multimode auto- scalers. Jobstate is updated to submitted as seen in line 12. Algorithms 4 and 5 are refined in algorithm 6. Job Initialising Refinement utilised the InitReqFunc- tions ASM derived function to check for the provisioning of requisite universes for this phase as seen in line 1 of al- gorithm 6. InitReqFunctions is a refinement for all required universes and functions for job initialising. The authenti- cation of the universes updates Systemstate to active . Sys- temRequest is activated to initiate job requests and to pro- vision VMs, which causes systemstate to be updated to ac- tive as seen in line 3 to 4. ReqRequest is applied to map jobs to VMs to be installed as tasks for the Jobhandler and Joblauncher to enforce their task processing. These activities cause the Systemstate to be updated to active as seen in line 7. This refinement is equivalent to the algo- rithms 4 and 5 of the second phase of our ground model as seen in figure 5. As the state changes of algorithm 6 are equivalent to the state transitions of our ground model. 3.4.3 Rule 3, job queuing: The job queuing phase commences when there is a short- age of VMs during job processing. The phase is modelled as part of our ground model as seen in algorithms 7 and 8, and figure 5 for Simple and Multimode auto-scalers. In this phase, universes from the previous phases are provi- Algorithm 2Multimode Initial Phase 1: if ∃ vm ∈ VM ∧∃ p ∈ PROCESS ∧∃ ar ∈ ARESOURCE∧∃ j∈ JOB∧∃ t∈ Time then 2: processState(p) :=idle 3: end if 4: while VI(j,vm ) ∧ Joblauncher(Jobhandler(j,vm )) do 5: if jobRequest(j,ar ) = false ∧ processRequest(p,ar ) =false then 6: JobTime(j) :=idle 7: end if 8: if mappedVM(j,p ) = false ∧ mappedJob(j,p ) =false then 9: JobTime(j) :=idle 10: end if 1 1: if installed(j,vm ) = false ∧ Joblauncher(Jobhandler(j,vm ),vm ) = false then 12: JobState(j) := idle∧ JobTime(j) := idle 13: numofSerReq(s i ) :=undef 14: VmUL =undef 15: Vmpool :=undef∧ RVM :=undef 16: end if 17: end while Algorithm 3Refined Initial Phase Requir e: AResource 1: if InitReslist = IRL idle ∧ ReqResources = false then 2: SystemState(j,p ) :=idle 3: end if 4: while SystemRequest = false ∧ ReqResources =false do 5: SystemState(j,p ) :=idle 6: end while 7: if installed(j,vm ) = false ∧ Jobhandler(j,vm ) =undef then 8: SystemState(j,p ) :=idle 9: end if sioned. This causes jobT ime and pr ocessState to transi- tioned to started and r eady as seen in lines 1 to 5. Job and process requests are activated to foster VM provisions. The VM count is monitored to determine the quantity of VMs available. When the quantity is below the required threshold for task processing; the MappedVM , Jobhandler and joblauncher are updated to false to confirm low VM count. This causes the jobs to queue as seen in lines 9 to 12 of both algorithms. JobState transitions to waiting to sig- nify the current state of the modelling process. Our ground model algorithms are refined in algorithm 9. Job Queuing Refinement is achieved by activating the InitReqFunctions and ReqRequest functions to foster resource provisions, and the mapping of VMs to jobs. This causes SystemState to be updated to active as seen in lines 1 to 2. The QueReslist derived function is applied to provision universes and functions for job queuing. Ad- ditionally , SystemRequest is activated to initiate jobs and ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 85 Algorithm 4Simple Jobs Initialising 1: if ∃ vm ∈ VM ∧∃ p ∈ PROCESS ∧∃ ar ∈ ARESOURCE∧∃ j∈ JOB∧∃ t∈ Time then 2: processState(p) :=ready 3: end if 4: while SimScaler(j,vm ) ∧ BJS(j,vm ) ∧ GTP(j) do 5: if jobRequest(j,ar ) = true ∧ processRequest(p,ar ) =true then 6: JobTime(j) :=started 7: end if 8: if mappedVM(j,p ) = true ∧ mappedJob(j,p ) =true then 9: JobTime(j) :=started 10: end if 1 1: if installed(j,vm ) = true ∧ Jobhandler(j,vm ) =true then 12: JobState(j) :=submitted 13: end if 14: end while Algorithm 5Multimode Jobs Initialising 1: if ∃ vm ∈ VM ∧∃ p ∈ PROCESS ∧∃ ar ∈ ARESOURCE∧∃ j∈ JOB∧∃ t∈ Time then 2: processState(p) :=ready 3: end if 4: while VI(j,vm ) ∧ Joblauncher(Jobhandler(j,vm )) do 5: if jobRequest(j,ar ) = true ∧ processRequest(p,ar ) =true then 6: JobTime(j) :=started 7: end if 8: if mappedVM(j,p ) = true ∧ mappedJob(j,p ) =true then 9: JobTime(j) :=started 10: end if 1 1: if installed(j,vm ) =true then 12: JobState(j) :=submitted 13: end if 14: end while VMs requests as seen in lines 3 to 4. The VM count is monitored to check for the quantity of VMs. A reduction in the VM count causes ReqRequest and Jobhandler to be updated to false , which causes the SystemState to transition to waiting as seen in lines 5 to 7. This refinement is equiv- alent to our ground model algorithms, as their system states transitioned to waiting as seen in figure 5. 3.4.4 Rule 4, job handling Job handling is the fourth phase of our model. This phase requires a derived function called the Jobhandling Module to optimise job processing, and the VM selection during job queuing. This function is created for each category of auto- scalers (i.e. Simple and Multimode Jobhandling module) as seen in algorithms 10 and 1 1. These modules perform sim- ilar functions with dif ferent structural features. The Simple Jobhandling Module utilise InitReqFunctions and QueRes- Algorithm 6Refined Job Initialising Requir e: AResource 1: if InitReqFunctions =IRF active then 2: SystemState(j,p ) :=active 3: while SystemRequest = true ∧ ReqResources =true do 4: SystemState(j,p ) :=active 5: end while 6: if installed(j,vm ) = true ∧ Jobhandler(j,vm ) =true then 7: SystemState(j,p ) :=active 8: end if 9: end if Algorithm 7Simple Jobs Queuing 1: if ∃ j ∈ JOB∧∃ ar ∈ ARESOURCE∧∃ p∈ PROCESS∧∃ vm∈ VM∧∃ t∈ Time then 2: JobTime(j) :=started 3: end if 4: while SimScaler(j,vm ) ∧ BJS(j,vm ) ∧ GTP(j) do 5: processState(p) :=ready 6: if jobRequest(j,ar ) = true ∧ processRequest(p,ar ) =true then 7: JobTime(j) :=started 8: end if 9: if VMCount≤ Num min then 10: MappedVM( j, vm) :=false 1 1: Jobhandler( j, vm) :=false 12: JobState(j) :=waiting 13: end if 14: end while list to check for the provision for job initialising and queu- ing universes and functions. Once they are authenticated, systemState is updated to active as seen in lines 1 to 4. Auto- scaler specific universes are provisioned to foster the ex- hibitions of VM provision behaviours. VMs and jobs re- quests are activated, which causes VM counts t o be moni- tored. When the VM count falls below the required thresh- old, a system state change occurs. This causes ReqRe- sour ces and Jobhandler to be updated to false . The sys- temState transitions to waiting as seen in lines 5 to 10 of both algorithms. The ReqResour ces is rechecked period- ically , to confirm if jobs have been mapped to VMs and installed as tasks. If the response is negative, the VM se- lection mode is activated via AddVM function. Once VM selection is accomplished, jobs are then mapped to VMs as seen in lines 1 1 to 19 of algorithm 10. This process dif fers from the Multimode Jobhandling module. The VmRequest function (a refinement of the VM selection process) is ac- tivated, which causes jobs to be mapped to VMs via the ReqResour ces as seen in lines 12 to 16 of algorithm 1 1. Job handling commences with the application of InitRe- qFunctions to foster the provision of job initialising uni- verses and functions. Once these are active , the Jobhand- Mod is activated to provision all the universes and func- 86 Informatica 47 (2023) 75–96 E.K. Gavua et al. Algorithm 8Multimode Jobs Queuing 1: if ∃ j ∈ JOB∧∃ ar ∈ ARESOURCE∧∃ p∈ PROCESS∧∃ vm∈ VM∧∃ t∈ Time then 2: JobTime(j) :=started 3: end if 4: whileVI(j,vm ) do 5: processState(p) :=ready 6: if jobRequest(j,ar ) = true ∧ processRequest(p,ar ) =true then 7: JobTime(j) :=started 8: end if 9: if VMCount≤ Num min then 10: MappedVM( j, vm) :=false 1 1: Joblauncher(Jobhandler(j,vm )) := false 12: JobState(j) :=waiting 13: end if 14: end while Algorithm 9Refined Jobs Queuing Requir e: AResource 1: while InitReqFunctions = IRF active ∧ ReqResources =true do 2: SystemState(j,p ) :=active 3: if QueReslist = QRL active ∧ SystemRequest(p,ar ) =true then 4: SystemState(j,p ) :=active 5: if VMCount≤ Num min then 6: ReqResources :=false 7: Jobhandler((j,vm ) :=false 8: SystemState(j,p ) :=waiting 9: end if 10: end if 1 1: end while tions for job handling. This causes SystemState to be up- dated to active as seen in lines 1 to 3 of algorithm 12. Suf- ficient time request is made and the response granted by the AResour ces to ensure that the jobs provisioned are ad- equately processed. The SystemRequest is activated to fos- ter jobs and process requests. An authentication of this re- quest, maps jobs to VMs via ReqResour ces . This causes the mapped jobs and VMs to be installs as tasks to either continue or restart job processing as seen in lines 5 to 10. The outputs of job processing are monitored with Simulion- Duration , A verageUtilPM and A verageQueT ime . The job processing activity causes the SystemState to transition to busy as seen in lines 1 1 to 17. Our ground model’ s job han- dling algorithms are refined in algorithm 13. Job Handling Refinement is accomplished by activat- ing the the InitReqFunctions and SystemRequest functions to foster the provision of the requisite universes for job ini- tialising. This causes SystemState to be updated to active as seen in line 1 of algorithm 13. Moreover , the Jobhandling Module and the jobhandler are activated to foster VMs se- lection during job queuing, and the installing of mapped VMs and jobs as tasks for job processing as seen in lines 2 to 3 . The JobPr ocessing function is activated to foster time Algorithm 10Simple Jobhandling Module Requir e: AResource 1: whileInitReqFunctions =IRF active do 2: SystemState(j,p ) :=active 3: if QueReslist = QRL active ∧ SystemRequest(p,ar ) =true then 4: SystemState(j,p ) :=active 5: end if 6: while SimScaler(j,vm ) ∧ BJS(j,vm ) ∧ GTP(j) do 7: if VMCount≤ Num min then 8: ReqResources :=false 9: Jobhandler((j,vm ) :=false 10: SystemState(j,p ) :=waiting 1 1: end if 12: if (ReqResources = false ∧ installed(task(j,vm )) =false then 13: AddVM(vm,j ) :=true 14: Compatible(attr(j),attr (vm)) :=true 15: belongsTo(j,vm ) :=true 16: ReqResources :=true 17: end if 18: end while 19: end while requests and the mapping of jobs to VMs for job processing. Furthermore, the output of job handling are modelled as the job processing ensues. This activity causes the SystemState to transition to busy as seen in lines 5 to 12. This refinement is equivalent to our ground model’ s job handling algorithm, as SystemState transitioned to busy as seen in figure 5. 3.4.5 Rule 5, job termination Job T ermination is the fifth phase of our model. This phase requires two conditions to be initiated. First, a system fail- ure or an abrupt system call to halt job processing. Second, the exhaustion of jobs generated. This phase is a result of the activities of job handling as seen in algorithm 14 of our ground model. Hence, there must be activities on- going to demonstrate job processing, before job termina- tion occurs. Therefore, before job processing is halted, the universes and functions required for job initialising should be provisioned. This updates pr ocessState to r eady as seen in lines 1 to 2. Job processing is monitored via the allocated time, and how long jobs remain mapped to VMs. As job are being processed, pr ocessState and job- State transtion to running . Also jobT imes updates to pr o- cessing as seen in lines 3 to 10. When a system interrupt occurs which causes the job processing to halt; jobstate transitions to failed and pr ocessState to stopped as seen in lines 13 to 15. Moreover , when job processing is com- pleted; jobState transitions to done , jobT ime to completed , and event(t) to terminate as seen in lines 17 to 20 depicting the exhaustion of job generated. The system state changes can be seen in the job and process states figures 6 and 7. Job termination is refined in algorithm 15. Job T ermination Refinement is achieved by the ap- ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 87 Algorithm 1 1Multimode Jobhandling Module Requir e: AResource 1: whileInitReqFunctions =IRF active do 2: SystemState(j,p ) :=active 3: if QueReslist = QRL active ∧ SystemRequest(p,ar ) =true then 4: SystemState(j,p ) :=active 5: end if 6: whileVI(j,vm ) do 7: if VMCount≤ Num min then 8: ReqResources :=false 9: Joblauncher(Jobhandler(j,vm ),vm ) := false 10: SystemState(j,p ) :=waiting 1 1: end if 12: whileVmRequest(j,vm ) =active do 13: ReqResources :=true 14: end while 15: end while 16: end while plication of InitReqFunctions , SystemRequest and ReqRe- sour ces . This is to foster the provision of universes and functions for job initialising and job handling. This causes systemstate to transition to active as seen in lines 1 to 2 of algorithm 15. The JobHandReslist function and the job- handler are activated to foster job processing. Systemstate is updated to busy as seen in lines 3 to 4. When a sys- tem call is activated that causes job processing to halt; the systemstate is automatically updated to stopped as seen in lines 5 to 6. This event signifies an abrupt job termination. Furthermore, when systemRequest is active while there are no jobs to be processed; event and systemstate are updated to terminate and done as seen in lines 7 to 12. This signi- fies the completion of job processing. This refinement is equivalent to our ground model’ s algorithm 14 as system- state transitioned to either stopped or done aligning with the job termination conditions. Let us now discuss the evalua- tion of our model. 4 Evaluation This section is split into two parts: the validation and eval- uation of our model. The validation sub-section focuses on test cases developed from our model’ s previously dis- cussed algorithms. The evaluation sub-section focuses on examining the five auto-scalers used to construct our model. Finally , we conclude our evaluation by demonstrating our model’ s applicability to other auto-scalers from prior art. Let us now proceed to discuss the validation of our model. 4.1 V alidation Our ASM model’ s validation was achieved via the creation of test cases from our ground model’ s algorithms and their refinements. These test case were developed on CoreASM (a plug-in available for the Eclipse IDE). The test cases Algorithm 12Job Handling Requir e: AResource 1: while InitReqFunctions = IRF active ∧ SystemRequest(p,ar ) :=true do 2: JobHandMod multimode :=active 3: Jobhandler((j,vm ) :=true 4: SystemState(j,p ) :=active 5: while t ∈ TIME∧ TimeRequest(j,p ) = true do 6: mappedVM(j,vm ) :=true 7: if SystemRequest(p,ar ) =true then 8: ReqResources :=true 9: installed(j,vm ) :=true 10: event(t) :=started 1 1: SimulationDuration :=SD max 12: AveragUtilPM :=AUPM max 13: AveragQueTime :=AQT max 14: end if 15: SystemState(j,p ) :=busy 16: end while 17: end while Algorithm 13Refined Job Handling Requir e: AResource 1: while InitReqFunctions = IRF active ∧ SystemRequest(p,ar ) :=true do 2: JobHandMod multimode :=active 3: Jobhandler((j,vm ) :=true 4: SystemState(j,p ) :=active 5: whileJobProcessing =JP active do 6: SystemRequest(p,ar ) :=true 7: ReqResources :=true 8: SystemState(j,p ) :=busy 9: end while 10: end while (i.e., cor easm specifications ) were designed as interactive sequences with suitable checks to describe the expectations of our model’ s states. These test cases were checked to see if specified assertions hold in given states. The test cases were processed and checked if all the assertions were sat- isfied. A satisfied assertion finished with a pass verdict. However , as soon a s an assertion was not satisfied, the sim- ulation was interrupted, reporting a violation. At each step, the simulator performed update checking to ensure that all states were updated. Our validation goals are: T o assess the interactions of the phases of our ground model via the application of universes and signatures. T o examine the application of derived functions (modules) as refinements of our ground model. T o assess the application of guar ded updates (which are reflective of control state ASMs) to ensure equiva- lence (between ground model algorithms and their re- finements). Our validated specifications are available in the Auto- 88 Informatica 47 (2023) 75–96 E.K. Gavua et al. Algorithm 14Job Termination 1: if ∃ j ∈ JOB∧∃ ar ∈ ARESOURCE∧∃ p∈ PROCESS∧∃ t∈ Time∧ JobRequest(j,ar ) then 2: processState :=ready 3: while t ∈ TIME∧ TimeRequest(j,p ) = true∧ mappedVM(j,vm ) =true do 4: JobTime(j) :=processing 5: while processRequest(p,ar ) = true∧ jobhandler(j,vm ) =true do 6: installed(j,vm ) :=true 7: event(t) :=started 8: JobState(j) :=running 9: ProcessState(p) :=running 10: JobTime(j) :=processing 1 1: end while 12: end while 13: if jobRequest(j,ar ) = true ∧ event(task(p)) =terminate then 14: JobState(j) := failed ∧ processState(p) :=stopped 15: end if 16: end if 17: if ¬∃ j ∈ JOB ∧ ¬∃ p ∈ PROCESS ∧ JobRequest(j,ar ) then 18: Event( t) := Terminate∧ jobTime( j) := Completed 19: jobState( j) :=done 20: end if Scaling-ASM repository on Github 2 . This allows for fur - ther scrutiny and reuse of our validation approach. W e pro- vide a short overview of the validation process. 4.1.1 Model modules CoreASM modules (CoreModules) were designed with ASM rules which aligned with the control state ASM defi- nition 1 to ensure that, once the conditions for state transi- tions were met, system states were updated accordingly . Three key modules (shown in figure 8) were applied to support our model validation. These modules represents the actual file names of the modules with the ASM speci- fication file extensions (.casm). The arrows represents the levels of dependency of each file from the bottom to the top. The topmost file is the module for job initialising, which is followed by the job queuing module. The jobhandler mod- ule for Simple and Multimode auto-scalers are on the same level, which are followed by a general jobhandler module with VM selection integrated refinements. The MultiJob- HandMod and SimJobHandMod modules were validated separately , and applied to the Multimodes and Simple auto- scalers as seen in MultiJobHandMod.casm and SimJob- HandMod.casm. In order to validate the modules, the test case were checked for the provision of ar esour ces and job queuing re- 2 https://github.com/EbenezerKomlaGavua/ Auto- Scaling- ASM Algorithm 15Refined Job Termination Requir e: AResource 1: while InitReqFunctions = IRF active ∧ SystemRequest(p,ar ) =true do 2: ReqResources := true ∧ SystemState(j,p ) :=active 3: while JobHandReslist = JHRL active ∧ jobhandler(j,vm ) =true do 4: SystemState(j,p ) :=busy 5: if SystemState(j,p ) = busy ∧ event(task(p)) =terminate then 6: SystemState(j,p ) :=stopped 7: else if SystemRequest(p,ar )∧¬∃ j ∈ JOB∧¬∃ p∈ PROCESS then 8: Event( t) :=Terminate 9: SystemState(j,p ) :=done 10: end if 1 1: end while 12: end while Figure 8: ASM validation modules sources via the InitReqFunctions and QueReslist functions. It checked for the provisions of specific auto-scaling uni- verses for the two categories of auto-scalers via the JobInit- FunMod.casm module file. The result showed a check suc- ceeded assertion verdict with systemstate updated to active . Moreover , the test case checked for the number of VMs available via the VMcount . The result showed a check suc- ceeded assertion. The Jobhandler , Joblauncher and Re- qResour ce were updated to false which caused systemstate to transition to waiting . The test case checked for VM se- lection. The result showed a check succeeded assertion. The AddVM function was activated to select VMs which caused ReqResour ce to transition to true . The two special- ized modules fostered the transition of their auto-scalers from queuing to job handling. The CoreModules were then utilised to validate the other test cases representing the phases of our ground model. Initial Phase was validated following rule 1 (discussed in sub-section 3.4.1) of our model as seen in the JobInit- FunMod.casm file. A series of checks were done to validate this phase. First, the test case checked for the provision of universes and functions . The result showed a check suc- ceeded assertion. The pr ocessState function was updated to r eady . Second, the test case checked for jobs and process ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 89 requests via jobRequest and processRequest functions. An expected false result was returned with a check succeeded assertion. A false result was expected because no requests is made at the initial phase. Third, a mappedVM checks were done and an expected false result was returned with a a check succeeded assertion. Finally , the test case checked if VMs were mapped to jobs and installed as tasks. The result showed a check succeeded assertion. The above val- idation process can be seen in the SimpleInitialPhase.casm and MultimodeInitialPhase.casm files. Moreover , the test cases for the refinements of the ini- tial phase were checked to ensure equivalence with those representing our ground model. The CoreASM checked for the provision of universe and functions via InitReslist function. The results showed a check succeeded assertion. Systemstate was updated to active . The test case checked for job and process requests via SystemRequest . The re- sult showed a check succeeded assertion. The test case then checked for the mapping of VMs and jobs via ReqResour ce . The result showed a check succeeded assertion. Finally , the test case checked the status of joblauncher and jobhan- dler . The result showed a check succeeded assertion with an expected false , which showed that jobs and VMs were not installed as tasks. The checks on the refinement were equivalent to those of our ground model. The above vali- dation process can be seen in the RefinedInitialPhase.casm file. Job Initialising was validated following rule 2 (dis- cussed in sub-section 3.4.2) of our model. The Simple and Multimode auto-scalers were validated separately . The test case for job initialising checked for the provision and interaction of universes and functions from the previous phase via the InitReqFunctions function in the JobInitFun- Mod.casm module file. Also, the test case checked for the application of an ASM rule to initiate job processing and the request for jobs and processes. The result showed a check succeeded assertion verdict with jobT ime updated to started . The test case checked for the installation of mapped jobs as tasks. The result showed a check succeeded assertion with jobT ime updated to started and jobState to submitted . The job initialising validation can be seen in the SimpleJobJobInitialising.casm and MultimodeInitialis- ing.casm files. Furthermore, the test case for the refined algorithms checked for the provision of universes and functions via Ini- tReqFunctions . The result showed a check succeeded as- sertion verdict with systemstate updated to active . The test case checked for jobs and VMs request via systemRequest . A check succeeded assertion verdict was returned. Also, the test case checked for the installation of mapped jobs as tasks. The result showed a check succeeded assertion ver - dict with the jobhandler updated to true . The systemstate was updated to active which was equivalent to the checks executed on the test cases of our ground model. The refined job initialising validation can be seen in the RefinedJobIni- tialising.casm file. Job Queuing was validated per rule 3 of our model (discussed in sub-section 3.4.3). The Simple and Multi- mode auto-scalers were validated separately . The test cases checked for the provision of of universes from the first two phase of our model. It also checked for specific auto- scalers universes and functions as seen in the JobQueFun- Mod.casm module file. The result showed a check suc- ceeded assertion. JobT ime and pr ocessState were updated to started and r eady . The test cases checked for jobs and VMs requests and the VM count. The result showed a check succeeded assertion. When the VM count fell below the expected threshold, the jobhandler was updated to false in the Simple auto-scalers and the joblauncher was also up- dated to false in Multimode auto-scalers. This situation transitioned JobState to waiting . The job queuing valida- tion can be seen in the SimpleJobQue.casm and Multimod- eJobQue.casm files. Moreover , the test case for the refined job queuing was validated. The test case checked for the provision of uni- verses and functions via the QueReslist function. The result showed a check succeeded assertion which caused system- state to be updated to active . Also, the test case checked for for jobs and VMs requests, and the level of the VM count. The result showed a check succeeded assertion which caused systemstate to be updated to waiting . This showed that there was shortage of VMs. The test cases demonstrated the equivalence of the refined queuing algo- rithms to those of our ground model. The refined job queu- ing validation can be seen in the RefinedJobQue.casm file. Job Handling The test case created to validate Job handling applied rule 4 of our model (discussed in sub- section 3.4.4). This phase applied the MultiJobHand- Mod and SimJobHandMod modules discussed in sec- tion 4.1.1 to validate the two categories of auto-scalers. The test case checked for the provision and interaction of uni- verses and functions via InitReqFunctions in the JobInit- FunMod.casm file. Also, the test case checked for the job queuing and VM selection via the jobhandling mod- ules in JobHandVmReqMod.casm file. The results showed a check succeeded assertion. Moreover , the test cases checked for the request for suf ficient time for tasks pro- cessing via timeRequest and the installation of tasks. The results showed a check succeeded assertion. The system- state transitioned to busy . The Job handling validation can be seen in the JobHandling.casm file. Furthermore, the refined algorithm was also validated with the Jobhandling module . The test cases checked for the provision resources via JobInitFunMod.casm file. Also, it checked for the VMs shortage and selection at the queu- ing phase with the jobhandling module . The results showed a check succeeded assertion which caused the systemstate to transition to active . The test case checked for the map- ping VMs to jobs, time requests and systemr equest via the JobPr ocessing function. The results showed a check succeeded assertion. The refined job handling test cases showed equivalence to those our ground model, since they all caused a system state update to busy . The refined Job handling validation can be seen in the RefinedJobHan- 90 Informatica 47 (2023) 75–96 E.K. Gavua et al. dling.casm file. Job T ermination was validated following sub- section 3.4.5 of our model. The test cases developed for this phase checked the conditions for job termination. Sequential checks were employed to ensure that all the previous phases were appropriately validated. First, the test case checked for job initialising via the InitReq- Functions function in the JobInitFunMod.casm file. The results showed a check succeeded assertion which caused pr ocessstate to transition to r eady . Second, the test case checked for the mapping of VMs to jobs, time request and the status of the Jobhandler . The results showed a check succeeded assertion. Third, the test case checked for system interruptions (via universes designed to halt mid- way during task processing). The results showed a check succeeded assertion. Fourth, the test case checked for the quantity of jobs available at the end of task processing. The results showed a check succeeded assertion. The validation can be seen in the JobT ermination.casm file. Job T ermination refinement test case checked for uni- verses and functions via the InitReqFunctions function. The result showed a check succeeded assertion which caused systemstate to transition to active . Then, the test case checked for job handling via JobHandRelist . A check succeeded assertion was returned and systemstate to tran- sition to busy . Moreover , the test case checked for sys- tem state interruption. A check succeeded assertion was returned and systemstate transitioned to stopped (as ex- pected). Finally , the test case checked for systemRequest when all the jobs generated were exhausted. A check suc- ceeded assertion was returned, which caused systemstate to transitioned to done (as expected). The refined job ter - mination test cases showed equivalence to those of our ground model, since they all caused a system state transition to stopped and done per the conditions for job termination. The validation process can be seen in the RefinedJobT er - mination.casm file. In conclusion, the test cases developed from our ground model algorithms and their refinements aligned with the validation goals discussed in section 4.1. 4.2 Abstract state machine model evaluation This section describes the evaluation process of our model. Our evaluation criteria are discussed emphasizing the ASM theory described in sub-section 2.4. W e applied the follow- ing criteria to evaluate our model. – T o assess the equivalence of the refined auto-scaler al- gorithms to our ground model via the application of universes and signatur es . – T o examine the application of derived functions to spe- cific portions of auto-scaling; such as job initialising, VM selection and job handling to ensure the applica- tion of ASM Model Refinement . – T o assess the application of guar ded updates and Bör ger ’ s r efinement on auto-scalers. Algorithm 16Threshold Initial Phase Requir e: AResource 1: if InitReslist =IRL idle then 2: TLevel := undef ∧ SystemState(j,p ) := idle 3: end if 4: whileSystemRequest =false do 5: SystemState(j,p ) :=idle 6: end while 7: if ReqResources =false then 8: SystemState(j,p ) :=idle 9: end if 10: if installed(j,vm ) =false then 1 1: Joblauncher(Jobhandler(j,vm )) := false 12: SystemState(j,p ) :=idle 13: end if In order to prevent the repetition of algorithms, we will selectively utilise a few formalized algorithms for our dis- cussion. Let us discuss the evaluation of our ASM rules. 4.2.1 Rule 1, initial phase This phase was evaluated per sub-section 3.4.1 and algo- rithm 1 of our model. Algorithm 16 is used for our dis- cussion, since aside the specific function TLevel , the state changes are the same for all auto-scalers. At the initial phase, all the auto-scalers apply the InitReslist function to access universes and functions. However , no ar esour ces are provisioned. Therefore systemstate is updated to false and the threshold monitoring function TLevel is updated to undef as seen in lines 1 to 3 of algorithm 16. Also, job and process requests are initiated, but no responses are re- ceived (as expected). Hence, there was no state transitions for systemstate as seen in lines 4 to 6. Also, no VMs were mapped to jobs, and installed as tasks for processing. This caused the Joblauncher to be updated to false and system state to idle as as seen in lines 7 to 13. The refinement is equivalent to the first phase of our ground model shown in figure 5. Since the system state transitioned to idle as seen in algorithm 3. Also, the re- finement satisfies the evaluation criteria discussed in sub- section 4.2, since derived function were applied to model the refinement. Also, state transitions were observed when conditions were met, which are reflective of guar ded up- dates of control state ASMs. 4.2.2 Rule 2, job initialising Job Initialising was evaluated with sub-section 3.4.2. Al- gorithm 17 is utilised for our discussion, since all the state changes are the same for all auto-scalers (aside the spe- cific reusable VMs function R VM ). The InitReqFunctions derived function is applied to foster the provision of Ar e- sour ces via universes and functions for this phase. The Sys- temRequests and ReqResour ces functions activated jobs and VMs requests, and the mapping of VMs to jobs as seen ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 91 Algorithm 17Vmopt Jobs Initializing Requir e: AResource 1: if InitReqFunctions = IRF active ∧ SystemRequest =true then 2: Joblauncher(Jobhandler(j,vm )) := true∧ ReqResources :=true 3: ifinstalled(j,vm ) =true∧ RVM =Q min then 4: SystemState(j,p ) :=active 5: end if 6: end if Algorithm 18Vmcreate Jobs Queuing Requir e: AResource 1: whileInitReqFunctions =IRF active do 2: ReqResources :=true∧ TLevel :=T min 3: SystemState(j,p ) :=active 4: if QueReslist =QRL active then 5: SystemState(j,p ) :=active 6: end if 7: if VMCount≤ Num min then 8: ReqResources :=false 9: Joblauncher(Jobhandler(j,vm )) := false 10: TLevel :=T avg 1 1: SystemState(j,p ) :=waiting 12: end if 13: end while in lines 1 to 2. T asks are installed for job processing to commence and the function R VM is updated to minimum, which caused SystemState to transition to active as seen in lines 3 to 6. This evaluation is applicable to Thr eshold , Vm- cr eate , Pooling and FixedVM auto-scalers. In the case of the other multimode auto-scalers, thr eshold and vmcr eate transition to T min , while pooling to Q min during job ini- tialising. This refinement is equivalent to the second phase of our model shown in figure 5 and algorithm 6. Also, the re- finement satisfies our evaluation criteria discussed in sub- section 4.2, since derived function were applied to cause job processing to commence. State transitions were seen when conditions were met, which are reflective of guar ded updates of control state ASMs. 4.2.3 Rule 3, job queuing Job queuing evaluation was achieved via Rule 3 of our model discussed in sub-section 3.4.3. Algorithm 18 (rep- resenting Vmcreate auto-scaler) is used for our discussion. The InitReqFunctions function is activated for the provision of universes to foster job initialising. This caused system- State to transition to active . Tlevel transitions toT min (i.e., minimum VM threshold utilisation) as seen in lines 1 to 3. QueResList is activated to monitor process and job requests, and the mapping of VMs to jobs as seen in lines 4 to 6. The VM count are monitored. A reduction in the VM count, caused ReqResour ces and Joblauncher to be updated to false . Also, Tlevel transitions toT avg (i.e., average VM threshold utilisation). This caused SystemState to transi- tion to waiting as seen in lines 7 to 13. This evaluation is applicable to all auto-scalers. In the case of the other multi- mode auto-scalers Thr eshold transitioned toT avg , Pooling toQ avg and Vmopt toQ avg during job queuing. This refinement is equivalent to the job queuing of our model shown in figure 5 and algorithm 9. Also, the refine- ment satisfies the evaluation criteria discussed in subsec- tion 4.2. This is seen in the application of derived functions to model job queuing. Also, state changes are seen when function conditions were met, which are reflective of the guar ded updates of control state ASMs. 4.2.4 Rule 4, job handling Job handling was evaluated per Rule 4 (discussed in sub- section 3.4.4). During job handling, the auto-scalers ac- tivate the InitRequir edFunctions , JobHandRelist derived functions and the jobhandling modules (designed in algo- rithms 10 and 1 1) for job processing. Aresources are pro- visioned via universes and functions for job processing. This caused SystemState to transition to busy as seen in lines 1 to 6 of algorithm 19. The auto-scalers exhibited behaviours per their core functions. The behaviours are analysed as follows. First, thr eshold and vmcr eate applied VmUL to monitor VM utilization. VmUL is utilised dif ferently in the two auto- scalers. In the case of thr eshold , if the current VM util- isation is lower than the average VM threshold, the VMs are destroyed. However , if the current VM utilisation is lower than the average VM threshold but the VM is the last VM being processed; the duration period is extended by one hour to receive a new job before the VM is destroyed. In the case of Vmcr eate , if the maximum utilisation of VMs is greater than the expected VM threshold, more VMs added are created. Also, if the current threshold is greater than the expected VM threshold, more VMs are created. This caused SystemState to transition to busy . Second, Vmopt monitors the VM count of reusable VMs in the VI. If the number reusable VMs are more than and equal to the minimum number expected, job processing continues until all the jobs are processed. Third, Pooling monitors the VM count in its VM pool during job process- ing. If the number of VMs are more that the minimum expected, more VMs are created. Job processing contin- ues until all the jobs are processed as seen in lines 7 to 12 of algorithms 19. This causes SystemState to transition to busy . The output of job processing showed Simulation- Duration , A veragQueT ime and A veragUtilPM transitioned to maximum levels. These job handling refinements are equivalent to the al- gorithms of our ground model shown 12 to 13 which are reflective of figure 5. Also, the refinement satisfies the evaluation criteria discussed in sub-section 4.2 as derived functions were applied to model job initialising to job han- dling. 92 Informatica 47 (2023) 75–96 E.K. Gavua et al. Algorithm 19Pooling Jobs handling Requir e: AResource 1: whileInitReqFunctions =IRF active do 2: JobHandMOD multimode :=active 3: if JobHandReslist = JHRL active ∧ Vmpool =Q max then 4: ReqResources :=true ∧ 5: SystemState(j,p ) :=busy 6: end if 7: if Vmpool>=Min Q then 8: AddVM(j,vm ) :=true∧ 9: ReqResources :=true 10: Joblauncher(Jobhandler(j,vm )) := true 1 1: SystemState(j,p ) :=busy 12: SimulationDuration :=SD max 13: AveragQueTime :=AQT max 14: AveragUtilPM :=AUPM max 15: end if 16: end while 4.2.5 Rule 5, job termination: Job T ermination was evaluated per rule 5 of our model (dis- cussed in sub-section 3.4.5). The pooling auto-scaler was utilised to evaluate this phase. The evaluation of job termi- nation required a modelling that showed an interaction of the previously discussed phases. Initially , InitRequir edFunctions , jobhandling modules are activated for the provision of Ar esour ces via universes and functions towards job initialising and job handling. The JobHandRelist is triggered to foster the job han- dling. Vmpool transitions toQ max to signifying suf ficient provision of VMs for job processing. SystemState transi- tions to busy as seen in lines 1 to 4 of algorithm 20. More- over , the VM count is checked in the VM pool. If the num- ber of VMs in the VM pool is within the minimum range, more VM are provisioned. This causes the systemState to transition to busy as seen in lines 7 to 10. The SimulatioDu- ration transitions to SDmax and A verageQueT ime to AQT - max . Also A verageUtilPM transitions to AUPMmax as seen in lines 1 1 to 13. Furthermore, while jobs are being processed, a terminate event causes systemState transitions to stopped and event to terminate as seen in lines 15 to 16. Also, when the jobs generated are exhausted while System- Request is activated; event transitions to terminate and sys- temstate to done as seen in lines 17 to 21. This job termination refinement of the pooling auto- scaler is equivalent to the fifth phase of our model shown in figure 5, and algorithm 14 to 15. Also, the refinement satisfies the evaluation criteria discussed in sub-section 4.2 as derived functions were utililsed to model job initialis- ing to job termination. Also, state changes were seen when the conditions for function were met, which are reflective of guar ded updates of control state ASMs. Also, there is interaction between the phases of our model via the appli- cation of universes and functions. In conclusion, this evaluation enabled us to check the Algorithm 20Pooling Jobs Termination Requir e: AResource 1: whileInitReqFunctions =IRF active do 2: JobHandMOD multimode :=active 3: if JobHandReslist = JHRL active ∧ Vmpool =Q max then 4: ReqResources :=true 5: SystemState(j,p ) :=busy 6: end if 7: if Vmpool>=Min Q then 8: AddVM(j,vm ) :=true 9: ReqResources :=true 10: SystemState(j,p ) :=busy 1 1: SimulationDuration :=SD max 12: AveragQueTime :=AQT max 13: AveragUtilPM :=AUPM max 14: end if 15: if SystemState(j,p ) = busy ∧ event(task(p)) =terminate then 16: SystemState(j,p ) :=stopped 17: else if SystemRequest(p,ar ) ∧ ¬∃ j ∈ JOB∧¬∃ p∈ PROCESS then 18: Event( t) :=Terminate 19: SystemState(j,p ) :=done 20: end if 21: end while applicability of our model to the auto-scalers of fered with DISSECT -CF , and also the flexibility of the transition rules of our model. 4.3 Evaluation of our model with another auto-scaling mechanism The literature in section 2 analysed past auto-scalers mech- anisms, and selected [7] for in-depth analysis with our model. The algorithms of Y ang et al.’ s work have been made public; hence it was possible to apply our model. This auto-scaler presents a typical auto-scaling approach using workload prediction, as well as horizontal and vertical scal- ing. Therefore, it was possible to analyse and classified it as a multimode auto-scaler due to its specific features. W e discuss only the job handling phase since the other phases apply features similar to those discussed per the multimode auto-scalers above. Job Handling: In order to evaluate this auto-scaler , the jobhandling module for multimode auto-scalers is adopted and applied to optimize VM selection. VM selec- tion was activated via VmRequest . This caused VMs and jobs to be mapped and installed as tasks to continue job pro- cessing. The auto-scaler by [7] applies InitReqFunctions to initi- ate job processing. This activates the W orkload prediction function and jobhandling module . This causes systemstate to be updated to active as seen in lines 1 to 5 of algorithm 21. JobHandReslist is activated to foster the provision of resources via universes and functions for job handling. This activity causes the VMs utilisation levels to in- ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 93 Algorithm 21LoadPredict Jobs handling Requir e: AResource 1: if InitReqFunctions = IRF active ∧ SystemRequest(p,ar ) =true then 2: WorkloadPrediction := PWL active ∧ ReqResources :=true 3: JobHandMod L := active ∧ Joblauncher(Jobhandler(j,vm )) := true 4: SystemState(j,p ) :=active 5: end if 6: whileJobHandReslist =JHRL active do 7: if VmUL t >VMut max then 8: SystemState(j,p ) :=busy 9: end if 10: for all vm∈ VM do 1 1: if VmUL t >VMut max then 12: selfhealing SU :=active 13: end if 14: if VmUL t >VMut max then 15: AR SU :=active 16: end if 17: if VmUL t VMut max then 7: Cost− Aware P− SU :=active 8: end if 9: SystemState(j,p ) :=busy 10: end while 1 1: end while the resource level scaling down is activated as seen in lines 7 to 9. SystemState remains updated to busy through- out this operation. Pr e-scaling at (t + 1) th interval: Also, the number of service requests are predicted during job handling. This activates the computation of VM utilisation threshold at (t + 1) th intervals as seen in lines 3 to 5 of algorithm 23. When the VM utilisation threshold at (t + 1) th interval is greater than the maximum VM utilisation threshold, cost aware scaling up is activated as seen in lines 6 to 8. System- State remains updated to busy throughout this operation. Cost-awar e Pr e-scaling up: Moreover , during VM level scaling up; when the number of user requests is greater than zero, and the Ar esour ces provisioned are not suf fi- cient to handle user requests. The VM with the smallest capacity is activated as seen in lines 3 to 7 of algorithm 24. Conversely , if the Ar esour ces are suf ficient, a compari- son between resource level scaling up or VM level scal- ing up is made to select the appropriate option as seen in lines 8 to 1 1. SystemState remains updated to busy through- out this operation as seen in line 12. This refinements satisfies our evaluation criteria dis- cussed in sub-section 4.2 since derived functions were ap- plied to evaluate job handling of [7]. Also, the systemstate transitioned during the modelling of the phase including the specialised operations which are equivalent to our ground model. 94 Informatica 47 (2023) 75–96 E.K. Gavua et al. Algorithm 24Cost− aware Pre− scaling up Requir e: AResource 1: whileJobHandMod L =busy do 2: SystemState(j,p ) :=busy 3: whileJobHandReslist =JHRL active do 4: VmLevel SU :=active 5: if NumOfRequests> 0 then 6: if Aresource < NumOfRequests then 7: SmallestVM SU :=active 8: else 9: Rlevel SU := active ∨ VMlevel SU :=active 10: end if 1 1: end if 12: SystemState(j,p ) :=busy 13: end while 14: end while 5 Conclusion In this paper , we investigated the issues with evaluating auto-scaling mechanisms. W e proposed an ASM model to formalize newly proposed or pre-existing auto-scaling techniques. The development of our ASM model in- volved meticulous construction, comprising a comprehen- sive ground model and a set of five ASM Rules. These ele- ments served to capture the fundamental structure of auto- scalers and their essential execution phases. The refine- ment process employed within our model allowed for thor - ough scrutiny , ensuring its validity by enabling equivalence checks and formalization of the algorithms. Rigorous vali- dation was carried out using the esteemed CoreASM Sim- ulator , confirming the model’ s accurate response to various dynamic scenarios and system states. In future work, we will focus on further fortifying the verification of our model by applying comprehensive tem- poral properties test cases. This verification process aims to establish the correctness and equivalence of our specifi- cations. T o achieve this goal, we will explore and integrate additional model-based testing and verification approaches, harnessing their capabilities to enhance the reliability and robustness of our model. Acknowledgement This research was supported by the Hungarian Scientific Research Fund under the grant number OTKA FK 131793. Refer ences [1] N. Herbst, S. Kounev , and R. Reussner (2013). Elas- ticity in cloud computing: What it is, and what it is not. In Pr oceedings of the 10th International Confer - ence on Autonomic Computing (ICAC 13) pp. 23–27, 2013. [2] M. A. Netto, C. Cardonha, R. L. Cunha, and M. D. Assunçao (2014). Evaluating auto-scaling strategies for cloud computing environments, In 2014 IEEE 22nd International Symposium on Mod- elling, Analysis and Simulation of Computer and T elecommunication Systems . IEEE pp. 187–196. https://doi.or g/10.1 109/mascots.2014.32. [3] T . Lorido-Botran, J. Miguel-Alonso, and J. A. Lozano (2014). A review of auto-scaling techniques for elastic applications in cloud environments. Journal of grid computing , vol. 12, no. 4, pp. 559–592. https://doi.or g/10.1007/s10723-014-9314-7. [4] Y . Gurevich (1993) Evolving algebras: an at- tempt to discover semantics. Curr ent T r ends in Theor etical Computer Science, eds. G. Rozenber g and A. Salomaa, W orld Scientific. pp. 266–292 https://doi.or g/10.1 142/9789812794499 _0 021 [5] N. Roy , A. Dubey , and A. Gokhale (201 1). Ef ficient autoscaling in the cloud using predictive models for workload forecasting. In 201 1 IEEE 4th International Confer ence on Cloud Computing , IEEE, pp. 500–507. https://doi.or g/10.1 109/cloud.201 1.42. [6] C. Qu, R. N. Calheiros, and R. Buyya (2018). Auto- scaling web applications in clouds: A taxonomy and survey . ACM Computing Surveys (CSUR) , vol. 51, no. 4, pp. 1–33. https://doi.or g/10.1 145/3148149. [7] J. Y ang, C. Liu, Y . Shang, Z. Mao, and J. Chen (2013). W orkload predicting-based automatic scaling in ser - vice clouds. In 2013 IEEE Sixth International Con- fer ence on Cloud Computing , IEEE, pp. 810–815. https://doi.or g/10.1 109/cloud.2013.146. [8] E. Bör ger (2010). The abstract state machines method for high-level system design and anal- ysis. In Formal Methods: State of the Art and New Dir ections , Springer , 2010, pp. 79–1 16. https://doi.or g/10.1007/978-1-84882-736-3 _3 . [9] P . Arcaini, R.-M. Holom, and E. Riccobene (2016). Asm-based formal design of an adap- tivity component for a cloud system. Formal Aspects of Computing , vol. 28, no. 4, pp. 567–595. https://doi.or g/10.1007/s00165-016-0371-5. [10] G. Kecskemeti (2015). Dissect-cf: a simu- lator to foster ener gy-aware scheduling in infrastructure clouds. Simulation Modelling Practice and Theory , vol. 58, pp. 188–218. https://doi.or g/10.1016/j.simpat.2015.05.009. [1 1] H. Ghanbari, B. Simmons, M. Litoiu, C. Barna, and G. Iszlai (2012). Optimal autoscaling in a iaas cloud. In Pr oceedings of the 9th international confer - ence on Autonomic computing . ACM, pp. 173–178. https://doi.or g/10.1 145/2371536.2371567. ASM-based Model for Analysing Cloud… Informatica 47 (2023) 75–96 95 [12] A. Gandhi, P . Dube, A. Karve, A. Kochut, and L. Zhang (2014). Adaptive, model-driven autoscaling for cloud applications. In 1 1th International Confer - ence on Autonomic Computing ({ ICAC} 14) , pp. 57– 64. [13] M. Dhaini, M. Jaber , A. Fakhereldine, S. Ham- dan and R. Haraty (2021). Green computing approaches-A survey . Informatica , vol. 45, 2021. https://doi.or g/10.31449/inf.v45i1.2998. [14] D. Saxena and A. K. Singh (2021). A proactive au- toscaling and ener gy-ef ficient vm allocation frame- work using online multi-resource neural network for cloud data center . Neur ocomputing , vol. 426, pp. 248– 264. https://doi.or g/10.1016/j.neucom.2020.08.076. [15] A. Al-Dulaimy , J. T aheri, A. Kassler , M. R. H. Fara- habady , S. Deng, and A. Zomaya (2020). Multiscaler: A multi-loop auto-scaling approach for cloud-based applications. IEEE T ransactions on Cloud Comput- ing . https://doi.or g/10.1 109/tcc.2020.3031676. [16] Q. Z. Ullah, G. M. Khan, and S. Hassan (2020). Cloud infrastructure estimation and auto-scaling us- ing recurrent cartesian genetic programming-based ann. IEEE Access , vol. 8, pp. 17 965–17 985. https://doi.or g/10.1 109/access.2020.2966678. [17] A. Belkacem and Z. Houhamdi (2022). Formal ap- proach to data accuracy evaluation, Informatica , vol. 46, https://doi.or g/10.31449/inf.v46i2.3027. [18] H. Debbi (2021). Modeling and Performance Analysis of Resource Provisioning in Cloud Computing using Probabilistic Model Checking, Informatica , vol. 45, https://doi.or g/10.31449/inf.v45i4.3308. [19] T . LakshmiPriya and R. Parthasarathi, “An asm model for an autonomous network-infrastructure grid,” in International Confer ence on Networking and Services (ICNS’07) . IEEE, 2007, pp. 29–29. https://doi.or g/10.1 109/icns.2007.29. [20] A. Bianchi, L. Manelli, and S. Pizzutilo (201 1), A distributed abstract state machine for grid sys- tems: A preliminary study . In Pr oceedings of the Second International Confer ence on Parallel, Dis- tributed, Grid And Cloud Computing For Engi- neering, Civil-Comp Pr ess, Ajaccio, France, Paper , vol. 84. https://doi.or g/10.4203/ccp.95.84. [21] A. Bianchi, L. Manelli, and S. Pizzutilo (2013). An asm-based model for grid job management. Informat- ica , vol. 37, no. 3, 2013. [22] P . Arcaini, R.-M. Holom, and E. Riccobene (2016), Asm-based formal design of an adap- tivity component for a cloud system, Formal Aspects of Computing , vol. 28, no. 4, pp. 567–595. https://doi.or g/10.1007/s00165-016-0371-5. [23] E. Bör ger (2003). The asm refinement method. For - mal aspects of computing , vol. 15 (2-3): pp. 237–257. https://doi.or g/10.1007/s00165-003-0012-7. [24] J. Fitzgerald and P . Larsen (2009). Modelling systems: practical tools and techniques in soft- ware development, Cambridge University Press. https://doi.or g/10.1017/cbo978051 1626975. 96 Informatica 47 (2023) 75–96 E.K. Gavua et al.