Raghuraj Suryavanshi¹ and Divakar Yadav², ¹GBTU, India and ²South Asian University, India

The problem of mutual exclusion arises in distributed systems whenever shared resources are concurrently accessed by several sites. For correctness, it is required that shared resource must be accessed by a single site at a time. To decide, which site execute the critical section next, each site communicate with a set of other sites. A systematic approach is essential to formulate an accurate speciation. Formal methods are mathematical techniques that provide systematic approach for building and verification of model. We have used Event-B as a formal technique for construction of our model. Event-B is event driven approach which is used to develop formal models of distributed systems .It supports generation and discharge of proofobligations arising due to consistency checking. In this paper, we outline a formal construction of model of Lamport's mutual exclusion algorithm for distributed system using Event-B. We have considered vector clock instead of using Lam-port's scalar clock for the purpose of message's time stamping.

Formal Methods, Distributed System, Vector Clock, Event-B, Formal Specifications, Mutual Exclusion.