ASM-based Formal Model for Analysing Cloud Auto-Scaling Mechanisms.

The provision of resources to meet workloads demands has become a crucial responsibility for auto-scaling mechanisms (auto-scalers) on cloud infrastructures. However, implementing auto-scaling mechanisms on cloud frameworks has generated many technical challenges. A typical challenge is that, these auto-scalers are often designed on different cloud systems making their evaluation, comparisons and wider applicability problematic. We propose an Abstract State Machine (ASM) model to address this problem. Our ASM model was developed systematically according to the behaviours of several auto-scalers, covering the necessary system processes. Our model was checked and validated with the CoreASM Model Checker. The validation and evaluation proves that our model can be used to analyse auto-scaling mechanisms, even without conducting real-life experiments. Our model, therefore, provides the platform to evaluate the behaviours of algorithms executed on clouds.