Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

MERY-2011-579252

Dominique Méry, Mohamed Mosbah, Mohamed Tounsi. Refinement-based Verification of Local Synchronization Algorithms. In Formal Methods FM2011, Lecture Notes in Computer Science, Limerick, Irlande, June 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

Synchronization algorithms are mandatory for simulating local computation models of distributed algorithms. Therefore, correctness of these algorithms becomes crucial, because it gives confidence that local computations are simulated as designed and do not behave harmfully. However, these algorithms are considered to be very complex to prove since they are integrating both distributed and probabilistic aspects. We derive proofs of synchronization algorithms relied upon the correct-by-construction paradigm; it is supported by a progressive and incremental process controlled by the refinement techniques. We illustrate our approach by examples like the Handshake and the LC1 algorithms. These algorithms are designed for an asynchronous distributed network of anonymous processes which use the message-passing feature as a model for the communication

Contact

Dominique Méry
Mohamed Mosbah
Mohamed Tounsi

BibTex Reference

@InProceedings{MERY-2011-579252,
   Author = {Méry, Dominique and Mosbah, Mohamed and Tounsi, Mohamed},
   Title = {Refinement-based Verification of Local Synchronization Algorithms},
   BookTitle = {Formal Methods FM2011},
   Series = {Lecture Notes in Computer Science},
   Publisher = {Springer},
   Address = {Limerick, Irlande},
   Month = {June},
   Year = {2011}
}

EndNote Reference [help]

Get EndNote Reference (.ref)