TOUNSI-2011-644187
Mohamed Tounsi, Mohamed Mosbah, Dominique Méry. Proving Distributed Algorithms by Combining Refinement and Local Computations. Electronic Communications of the EASST, 35:0-2122, November 2011.
Download
Download paper:
Follow the link
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Abstract
Distributed algorithms are considered to be very complex to design and to prove; our paper contributes to the design of correct-by-construction distributed algorithms. The main idea relies upon the development of distributed algorithms following a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use refinement for proving the correctness of the resulting algorithms. However, the link between the problem and the first model remains to be expressed and the refinement is a real help to justify in a very progressive way the choices of design. We propose in this work a framework combining local computations models and refinement to prove the correctness of a large class of distributed algorithms. Local computations models define abstract computing processes for solving problems by distributed algorithms and can be integrated into a the Event-B modelling language to define proof-based patterns for the design of distributed algorithms. We illustrate our approach by examples like the leader election protocol or the distributed coloring algorithm. Our proposal is integrated into an environment called ViSiDiA
Contact
Mohamed Tounsi
Mohamed Mosbah
Dominique Méry
BibTex Reference
@article{TOUNSI-2011-644187,
Author = {Tounsi, Mohamed and Mosbah, Mohamed and Méry, Dominique},
Title = {Proving Distributed Algorithms by Combining Refinement and Local Computations},
Journal = {Electronic Communications of the EASST},
Volume = {35},
Pages = {0--2122},
Month = {November},
Year = {2011}
}
EndNote Reference [help]
Get EndNote Reference (.ref)