Abstract
Proving the correctness of distributed algorithms is a difficult challenge in dynamic networks. In these networks, topological changes can take place due to unexpected appearance and disappearance of devices and communication links. The existing studies in the literature lack a general model for their development and their proof. Besides, most of the proofs which have been introduced are handwritten. Our work aims at providing a reusable approach which reduces the specification and verification efforts of distributed algorithms. At the first stage, we present a basic pattern which aims to deal with topological events. At the second stage, we extend this pattern to construct and maintain a spanning forest in a dynamic network. We illustrate the extended pattern through the leader election algorithm. We show the efficiency of our approach by presenting the number of proofs associated with the development of the algorithm with and without using the pattern.
•A general approach to prove distributed algorithms for dynamic networks.•Topological events are specified by a general pattern.•Incremental refinement and local computations are combined to obtain general proofs.•The approach is illustrated by computing and proving the leader election in a tree.