Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods

Server virtualization technologies enable the cloud to perform load balancing by migrating virtual machines from heavily loaded physical machines to lightly loaded physical machines. A range of load balancing algorithms has been proposed to reach this goal. However, to evaluate the degree of reliability for such algorithms, quantitative guarantees are needed. In this paper, we build a virtual machine migration model based on a previous load balancing algorithm and construct an MDP-based performance model in PRISM, a probabilistic model checker. We then demonstrate that we can check a range of properties described in probabilistic temporal logic languages regarding the performance of the algorithm to answer questions that are otherwise hard for traditional methods to provide. Finally, we summarized the takeaways for cloud service providers/managers based on verification results.