Formal Modelling of Cluster-Coordinator-Based Load Balancing Protocol Using Event-B

Distributed system is a set of autonomous nodes or sites. Due to uneven distribution of work, some sites may become overloaded and other may be underloaded or ideal. Proper load balancing is required for better resource utilization. It will be more effective when sites are arranged in the form of a cluster. In cluster-coordinator-based approach, group of site construct clusters and each cluster will have one coordinator. The coordinator site keeps track of information of each site with its load value in the form of vector. If any site of the particular cluster transfer load to other site is present in same or different cluster, it will inform to coordinator to update its vector value. If none of the sites is available to adjust load, then the coordinator site must balance the load to transfer load to different clusters. In this paper, we formalize the cluster-coordinator-based load balancing using Event-B. Event-B is a formal method to mathematically verify the correctness of protocol in a distributed environment.