In: Mavronicolas, M.; Tsigas, Ph.: Lecture Notes in Computer Science, Vol. 1320: Distributed Algorithms, Proc. of 11th International Workshop, WDAG'97, Saarbrücken, Germany, pages 155-169. Springer, September 1997.
Abstract: A group membership protocol is presented and proven correct for a synchronous time-triggered model of computation with processors in a ring that broadcast in turn. The protocol, derived from one used for critical control funtions in automobiles, accepts a very restrictive fault model to achieve low overhead and requires only one bit of membership information piggybacked on regular broadcasts. Given its strong fault model, the protocol guarantees that a faulty processor will be promptly diagnosed and removed from the agreed group of processors, and will also diagnose itself as faulty. The protocol is correct under a fault-arrival assumption that new faults arrive at least n+1 time units aparat, when there are n processors. Exploiting this assumption leads to unusual real-time reasoning in the correctness proof.
Keywords: time-triggered protocol, group membership, synchronous algorithms, fault tolerance, formal modeling.