loading...
Formal Specification and Verification of a Group Membership Protocol for an Intrusion-Tolerant Group Communication System
Tsukuba, Japan December 16-December 18
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/PRDC.2002.1185613Ninth Pacific Rim International Sympo ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
HariGovind V. Ramasamy, Michel Cukier, William H. Sanders, "Formal Specification and Verification of a Group Membership Protocol for an Intrusion-Tolerant Group Communication System," Pacific Rim International Symposium on Dependable Computing, IEEE, pp. 9, Ninth Pacific Rim International Symposium on Dependable Computing (PRDC'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/PRDC.2002.1185613,
author = {HariGovind V. Ramasamy and Michel Cukier and William H. Sanders},
title = {Formal Specification and Verification of a Group Membership Protocol for an Intrusion-Tolerant Group Communication System},
journal ={Pacific Rim International Symposium on Dependable Computing, IEEE},
volume = {0},
year = {2002},
isbn = {0-7695-1852-4},
pages = {9},
doi = {http://doi.ieeecomputersociety.org/10.1109/PRDC.2002.1185613},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Pacific Rim International Symposium on Dependable Computing, IEEE
TI - Formal Specification and Verification of a Group Membership Protocol for an Intrusion-Tolerant Group Communication System
SN - 0-7695-1852-4
SP
EP
A1 - HariGovind V. Ramasamy,
A1 - Michel Cukier,
A1 - William H. Sanders,
PY - 2002
KW - null
VL - 0
JA - Pacific Rim International Symposium on Dependable Computing, IEEE
ER -
 
HariGovind V. Ramasamy, University of Illinois at Urbana-Champaign
Michel Cukier, University of Maryland at College Park
William H. Sanders, University of Illinois at Urbana-Champaign
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.
Citation:
HariGovind V. Ramasamy, Michel Cukier, William H. Sanders, "Formal Specification and Verification of a Group Membership Protocol for an Intrusion-Tolerant Group Communication System," prdc, pp.9, Ninth Pacific Rim International Symposium on Dependable Computing (PRDC'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.