A formal approach for virtual machine migration planning

Cloud computing is an emerging paradigm in information technology. Virtualization is the corner stone for this paradigm in which resources are utilized by running multiple virtual machines (VMs) on a physical host. During the VM´s life cycle, the cloud provider may migrate the VM from one host to another host. During the live migration process, some security, capacity, and dependency requirements are subject to violations due to the temporal relationship between migration steps. In this paper, we present a formal approach to plan VM migration; that is to find a sequence of migration steps such that all security, dependency, and performance requirements are met. The migration planning problem is modeled as a Constraints Satisfaction Problem and it is solved using Satisfiability Modulo Theory (SMT) solvers. We provide VMM-Planner, a formal framework that provides a VM migration plan to formally verify the given requirements in all intermediate migration steps.