A formal pattern for dynamic networks through evolving graphs
Faten Fakhfakh, Mohamed Tounsi, Ahmed Hadj Kacem, Mohamed E. Mosbah · 2015
One of the most important issues in dynamic networks is to prove the correctness of distributed algorithms. This issue has been widely studied in the literature. Nevertheless, we note a lack of consensus about the development and proof of these algorithms. Moreover, the proofs which have been presented are usually done manually. In this paper, we introduce a formal pattern based on evolving graphs which allows to record the dynamic behavior of a network topology. To specify the proposed pattern, we use the Event-B formal method which supports a refinement-based incremental development using RODIN platform.