Formal Verification of an Intrusion-Tolerant Group Membership Protocol
HariGovind V. Ramasamy, Michel Schatkin Cukier, William H. Sanders · 2003
this paper, we describe how we used the SPIN model checker to formally verify a group membership protocol that is part of an intrusion-tolerant group communication system. We describe how we successfully tackled the state-space explosion problem by determining the right abstraction level for formally specifying the protocol. The verification exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more e#cient without violating correctness. key words: intrusion tolerance, group communication systems, validation, formal methods 1.