Carnegie Mellon: The Rare Glitch Project                                                          E. Clarke and D. Kroenig
Membership Service
Verifying Protocol Properties
lUses implicit acknowledgement scheme
lEncoded in CRC that protects the frames
lA node that sends no or false data looses membership lAfter sending a frame, a node watches the following frames to determine if it is still considered a member of the cluster
CRC = cyclic redundancy check; a code used for error detection (no error correction is done)
In case of TTP/C, the length is fixed to 16 bits, which is a very small number. Another bit of accuracy is lost by encoding membership information in the code, which leaves 2^15 = 32768 codes.

The membership service works as follows in detail:
 * all nodes watch all messages on the bus,
 * if a node does not transmit a correct message, it looses membership

The node itself notices this by observing the messages of the subsequent nodes in the TDMA round. It can decide whether the others consider it a member or not using the error detection code

“consistent membership information”: Each node encodes its membership vector in the CRC. Any other node with different membership vector will therefore fail at the CRC.