Abstract
Due to the highly dynamic behavior and the time complexity in Mobile Ad-hoc NEtworks (MANETs), modeling distributed algorithms and looking at their assumptions represent a challenging research task. Also, proving the correctness of these algorithms for dynamic networks is a topic of intensive research. In fact, the solutions which have been proposed to express and prove the correctness of distributed algorithms are usually done manually. In addition, all these solutions lack a consensus about their development and their proof. The main contribution of this paper is to propose a general and formal model for dynamic networks based on evolving graphs and Event-B formal method. In fact, evolving graphs is a powerful tool to express fine-grained properties. This model allows to handle topological events and to characterize the concept of time with some particularities. We implement it with Event-B, based on refinement technique. To illustrate the proposed model, we investigate an example of a distributed algorithm encoded by local computations models.