Proving Distributed Coloring of Forests in Dynamic Networks

Authors

  • Faten Fakhfakh ReDCAD Laboratory, University of Sfax
  • Mohamed Tounsi ReDCAD Laboratory, University of Sfax
  • Mohamed Mosbah LaBRI Laboratory, Bordeaux INP, University of Bordeaux
  • Dominique Méry LORIA, University of Lorrain, Nancy
  • Ahmed Hadj Kacem ReDCAD Laboratory, University of Sfax

DOI:

https://doi.org/10.13053/cys-21-4-2857

Keywords:

Distributed algorithms, dynamic networks, forest, formal pattern, event-B method, coloring

Abstract

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 treesindynamicnetworks. It is based one volving 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.

Downloads

Published

2017-12-23

Issue

Vol. 21 No. 4 (2017): Advances in Human Language Technologies (Guest Editor: A. Gelbukh)

Section

Articles

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.