Refinement-based verification of local synchronization algorithms

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. © 2011 Springer-Verlag.