Proving Distributed Coloring of Forests in Dynamic Networks
Título del documento: Proving Distributed Coloring of Forests in Dynamic Networks
Revue: Computación y sistemas
Base de datos: PERIÓDICA
Número de sistema: 000423277
ISSN: 1405-5546
Autores: 1
1
2
3
1
Instituciones: 1University of Sfax, ReDCAD Laboratory, Sfax. Túnez
2Universite de Bordeaux I, LaBRI Laboratory, Bordeaux, Gironde. Francia
3Universite de Lorraine, Nancy, Meurthe-et-Moselle. Francia
Año:
Periodo: Oct-Dic
Volumen: 21
Número: 4
País: México
Idioma: Inglés
Tipo de documento: Artículo
Enfoque: Aplicado, descriptivo
Resumen en inglés 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
Disciplinas: Ciencias de la computación
Palabras clave: Redes,
Algoritmos distribuidos,
Redes dinámicas,
Patrones formales,
Coloración
Keyword: Networks,
Distributed algorithms,
Dynamic networks,
Formal pattern,
Coloring
Texte intégral: Texto completo (Ver HTML) Texto completo (Ver PDF)