Formal specification and verification of a group membership protocol for an intrusion-tolerant group communication system

Harigovind V. Ramasamy, Michel Cukier, William H. Sanders

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings - 2002 Pacific Rim International Symposium on Dependable Computing, PRDC 2002
PublisherIEEE Computer Society
Pages9-18
Number of pages10
ISBN (Electronic)0769518524
DOIs
StatePublished - Jan 1 2002
EventPacific Rim International Symposium on Dependable Computing, PRDC 2002 - Tsukuba City, Ibaraki, Japan
Duration: Dec 16 2002Dec 18 2002

Publication series

NameProceedings of IEEE Pacific Rim International Symposium on Dependable Computing, PRDC
Volume2002-January
ISSN (Print)1541-0110

Other

OtherPacific Rim International Symposium on Dependable Computing, PRDC 2002
CountryJapan
CityTsukuba City, Ibaraki
Period12/16/0212/18/02

Keywords

  • Broadcasting
  • Contracts
  • Delay
  • Educational institutions
  • Fault tolerant systems
  • Formal specifications
  • Logic
  • Power system modeling
  • Protocols
  • Scheduling

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Science Applications
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Formal specification and verification of a group membership protocol for an intrusion-tolerant group communication system'. Together they form a unique fingerprint.

Cite this