@inproceedings{1e0b130c253a40a4b5a32726b55ae380,
title = "Formal specification and verification of a group membership protocol for an intrusion-tolerant group communication system",
abstract = "We describe a group membership protocol that is part of an intrusion-tolerant group communication system, and present an effort to use formal tools to model and validate our protocol. We describe in detail the most difficult part of the validation exercise, which was the determination of the right level of abstraction of the protocol for formally specifying the protocol. The validation exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.",
keywords = "Broadcasting, Contracts, Delay, Educational institutions, Fault tolerant systems, Formal specifications, Logic, Power system modeling, Protocols, Scheduling",
author = "Ramasamy, {Hari Govind V.} and Michel Cukier and Sanders, {William H.}",
note = "Publisher Copyright: {\textcopyright} 2003 IEEE.; Foundations of Intrusion Tolerant Systems, OASIS 2003 ; Conference date: 01-12-2003 Through 01-12-2003",
year = "2003",
doi = "10.1109/FITS.2003.1264937",
language = "English (US)",
series = "Foundations of Intrusion Tolerant Systems, OASIS 2003",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "251--260",
editor = "Lala, {Jaynarayan H.}",
booktitle = "Foundations of Intrusion Tolerant Systems, OASIS 2003",
address = "United States",
}