.png){kind=icon}
.png){kind=icon}
Return
Modeling and Proving Distributed Algorithms for Dynamic Graphs
.png){kind=icon}
OA
AI
DOI：10.1016/j.future.2020.03.003.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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. (C) 2020 Elsevier B.V. All rights reserved.
Keywords:
Distributed algorithms
Dynamic networks
Refinement
Formal pattern
Evolving graphs
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
F
IF:
6.1
Papers:
6.8K
Citations:
2.3W