Reconstruction and verification of group membership protocols

• In this paper, we present a process-algebraic specication 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.

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Keyword

Group Membership Protocols

Formal Specification

Process Algebra

Formal Verification

Model Checking

Publication and Content Type

vet (subject category)

rap (subject category)