MERY-2010-547302
Dominique Méry, Mohammed Mosbah, Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. In AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, Michael Leuschel, Markus Roggenbach Jens Bendisposto (ed.), Dusseldorf, Allemagne, September 2010.
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
Abstract: Our approach is directly related to the design of correct-by-construction programs. The main idea relies upon the development of distributed algorithms fol- lowing a top/down approach, which is clearly well known in earlier works of Dijkstra, and to use the refinement for controlling the correctness of the resulting algorithm. It relies on a more fundamental question related to the notion of problem to solve. The methodology can be based on incremental proof-based developments. However, the link between the problem and the first model remains to be expressed and the refine- ment 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 and refinement to prove the correctness of a large class of distributed algorithms
Contact
Dominique Méry
Mohamed Mosbah
Mohamed Tounsi
BibTex Reference
@InProceedings{MERY-2010-547302,
Author = {Méry, Dominique and Mosbah, Mohammed and Tounsi, Mohammed},
Title = {Proving Distributed Algorithms by Combining Refinement and Local Computations},
BookTitle = {AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems},
editor = {Jens Bendisposto, Michael Leuschel, Markus Roggenbach},
Address = {Dusseldorf, Allemagne},
Month = {September},
Year = {2010}
}
EndNote Reference [help]
Get EndNote Reference (.ref)