TY - BOOK
T1 - Reconstruction and verification of group membership protocols
AU - Atif, M.
AU - Cranen, S.
AU - Mousavi, M.R.
PY - 2010
Y1 - 2010
N2 - In this paper, we present a process-algebraic speci??cation 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.
AB - In this paper, we present a process-algebraic speci??cation 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.
M3 - Report
T3 - Computer science reports
BT - Reconstruction and verification of group membership protocols
PB - Technische Universiteit Eindhoven
CY - Eindhoven
ER -