Record Details

<p>Distributed systems, Formal methods, Load balancing, Proof obligations, Rodin, Verification</p>

Online Publishing @ NISCAIR

View Archive Info
 
 
Field Value
 
Authentication Code dc
 
Title Statement <p>Distributed systems, Formal methods, Load balancing, Proof obligations, Rodin, Verification</p>
 
Added Entry - Uncontrolled Name Yadav, Pooja ; Dr A P J Abdul Kalam Technical University, Lucknow 226 031, India
Suryavanshi, Raghuraj ; Dr A P J Abdul Kalam Technical University, Lucknow 226 031, India
Yadav, Divakar ; Institute of Engineering and Technology Lucknow 226 021, India
 
Uncontrolled Index Term Distributed systems, Formal methods, Load balancing, Proof obligations, Rodin, Verification
 
Summary, etc. <p>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.</p>
 
Publication, Distribution, Etc. Journal of Scientific & Industrial Research
2022-01-13 13:07:16
 
Electronic Location and Access application/pdf
http://op.niscair.res.in/index.php/JSIR/article/view/49532
 
Data Source Entry Journal of Scientific & Industrial Research; ##issue.vol## 80, ##issue.no## 12 (2021): Journal of Scientific and Industrial Research
 
Language Note en