Record Details

Formal Verification of Receiver Initiated Load Distribution Protocol with Fault Tolerance and Recovery using Event-B

NOPR - NISCAIR Online Periodicals Repository

View Archive Info
 
 
Field Value
 
Title Formal Verification of Receiver Initiated Load Distribution Protocol with Fault Tolerance and Recovery using Event-B
 
Creator Yadav, Pooja
Suryavanshi, Raghuraj
Yadav, Divakar
 
Subject Distributed systems
Formal methods
Load balancing
Proof obligations
Rodin
Verification
 
Description 1078-1090
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.
 
Date 2021-12-27T10:34:00Z
2021-12-27T10:34:00Z
2021-12
 
Type Article
 
Identifier 0975-1084 (Online); 0022-4456 (Print)
http://nopr.niscair.res.in/handle/123456789/58738
 
Language en
 
Publisher NIScPR-CSIR, India
 
Source JSIR Vol.80(12) [December 2021]