Résumé | Proving the correctness of distributed algorithms is a hard task due to the lack of global state knowledge and the non-determinism in the processes execution. In dynamic networks, this task becomes more difficult because of dynamic behavior and time complexity. In this talk, we propose a reuse based approach for specifying and proving distributed algorithms in dynamic networks. It consists in developing a formal pattern using Event-B method, based on refinement technique. Our pattern allows to handle topological events in dynamic networks and to characterize the concept of time. The proposed solution relies on evolving graphs, as a powerful model to record the evolution of a network topology. To illustrate it, we investigate an example of a distributed algorithm encoded by local computations models.
|