Formal Distributed Model for the Verification of Job-Scheduling in Cloud Environments
Imene Ben Hafaiedh, Maroua Ben Slimane, Sourour Haouala, Riadh Robbana · 2017
Cloud computing is an on-demand computing model, using virtualization technology to provide services to users in the form of virtual machines (VMs) through internet. Job-scheduling is one of the fundamental reasons to have high performance in a cloud environment. Therefore, there is a need for protocols that can efficiently allocate jobs to resources. However, due to the lack of an explicit and formal description of the resource perspective in the existing cloud platforms, the correctness of Cloud resources management can not be verified. The aim of the present work is to offer a formal description as a step towards ensuring a correct and consistent Cloud resource allocation modeling. In particular, we propose a distributed formal model for the description of a job-scheduling protocol in the cloud which considers the types of jobs and the resource availability in its scheduling decision. The formal verification of different properties of the proposed model has been performed automatically using Model-checking.