Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Artículo científico |
| Lingua: | en |
| Pubblicazione: |
Instituto Politécnico Nacional
2017
|
| Soggetti: | |
| Accesso online: | https://www.redalyc.org/articulo.oa?id=61553900025 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
Sommario:
- Proving Distributed Coloring of Forests in Dynamic Networks Faten Fakhfakh Mohamed Tounsi Mohamed Mosbah Dominique Méry Ahmed Hadj Kacem Computación event forest B method coloring formal pattern 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. 2017 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61553900025 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.4 Vol.21