Distributed systems, Formal methods, Load balancing, Proof obligations, Rodin, Verification

Abstract

Load distribution is a process that involves the allocation of tasks to various nodes in the distributed system in such a manner that overall resource utilization is maximized, and overall response time is minimized. This paper presents a formal model for verification of receiver-initiated load balancing and fault tolerance protocol with recovery in distributed systems using the eclipse-based Event-B platform called Rodin. Here, the receiver-initiated load balancing approach is demonstrated along with tolerance of node failure and recovery. In this approach, an underloaded node (receiver) initiates the process of load transfer from an overloaded node (sender). The underloaded node broadcasts a request message to obtain load from the overloaded nodes. The overloaded nodes reply with their load value. The underloaded node then selects the optimal overloaded node for load transfer. The chances of node failure are minimized by reducing the number of overloaded nodes. The process of recovery from failure is also shown in the proposed model. Formal methods are used to mathematically verify the critical properties of the system by developing a model based on its specifications. Our objective is to verify and validate the model for correctness through discharge of proof obligations using Event-B. Event-B is a formal method which is used for verification of a model based on distributed systems. The proof obligations generated by the model are discharged which ensures the correctness of our model.