Reconstruction and verification of group membership protocols

M. Atif, S. Cranen, and M.R. Mousavi. . Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010), Duesseldorf, Germany, September 2010.

Abstract

In this paper, we present a process-algebraic specification of group membership protocols specified in [Y. Amir, D. Dolev, S. Kramer and D. Malki, Membership Algorithms for Multicast Communication Groups, Springer-Verlag, 1992]. In order to formalise the protocol and its properties we disambiguate the informal specification provided by the paper. This requires trying different possible interpretations in the formal model and checking the consistency of the assumption and formally verifying the correctness properties. We thus present a formal reconstruction of the membership algorithms and model-check our reconstruction.

An extended version of this paper appeared as technical report CSR-10-08 (Tech. rep. in .pdf format).

@InProceedings{MousaviAvocs10,
    author      = "Atif, Muhammad and Cranen, Sjoerd and Mousavi, MohammadReza",
    title       = "Reconstruction and verification of group membership protocols",
    booktitle   = "Proceedings of the 10th International Workshop on Automated Verification of Critical Systems ({AVoCS} 2010)"
}