A Firefly-based Task Scheduling Algorithm for the Cloud Computing Environment: Formal Verification and Simulation Analyses

Task scheduling in the cloud environment is a critical problem and using a suitable method for task scheduling will increase resource efficiency. This will increase the satisfaction of customers due to providing their QoS requirements. The available solutions to this problem often seek to improve one of the criteria for service quality and use different methods to achieve this goal. This paper is aimed at offering an optimal solution to solve the task scheduling problem in the cloud environment using the firefly algorithm. The proposed algorithm helps not only to reduce the longest task completion time, but also to increase the utilization of virtual machines by taking into account the capabilities of each virtual machine and using the appropriate method for distributing virtual machine requests. Although, finding a proper task scheduling method is desirable, the correctness of this approach that can be checked by the automatic formal verification methods is a challenge. One of the most efficient method in this area is model checking which can verify the behavior of a system by checking some desired properties on the system model. Hence, we define a behavioral model of the task scheduling algorithm based on model checking techniques. To do so, we encode the algorithm to Abstract State Machine Metamodel-based Language (AsmetaL) and then some properties are defined for verifying the algorithm. The results obtained from the implementation of the proposed method show that the proposed method has an acceptable improvement for makespan and resource utilization.