文章基本信息

标题：Proving Distributed Coloring of Forests in Dynamic Networks
本地全文：下载
作者：Faten Fakhfakh ; Mohamed Tounsi ; Mohamed Mosbah 等
期刊名称：Computación y Sistemas
印刷版ISSN：1405-5546
出版年度：2017
卷号：21
期号：4
页码：863-881
语种：English
出版社：Instituto Politécnico Nacional
其他摘要：The design and the proof of correctness of distributed algorithms in dynamic networks are difficult tasks. These networks are characterized by frequent topology changes due to unpredictable appearance and disappearance of mobile devices and/or communication links. In this paper, we propose a correct-by-construction approach for specifying and proving distributed algorithms in a forest topology. In the first stage, we specify a formal pattern using the Event-B method, based on the refinement technique. The proposed pattern relies on the Dynamicity Aware-Graph Relabeling Systems (DA-GRS) which is an existing model for building and maintaining a forest of spanning trees in dynamic networks. It is based on evolving graphs as a powerful model to record the evolution of a network topology. In the second stage, we deal with distributed algorithms which can be applied to spanning trees of the forest. In fact, we use the proposed pattern to specify a tree-coloring algorithm. The proof statistics comparing the development of this algorithm with and without using the pattern show the efficiency of our solution in terms of proofs reduction.
其他关键词：Distributed algorithms; dynamic networks; forest; formal pattern; event-B method; coloring.