Simulation-based test of fault-tolerant group membership services

We address the problem of gaining assurance on the correctness of fault-tolerant and real-time distributed protocols. We validate implementations of two group membership protocols by running a centralized simulation of the distributed system, and testing whether the protocols satisfy the safety and timeliness properties prescribed by their specifications. Our testing environment performs deterministic experiments that include both normal workloads and failures injected into the execution, to test protocol behavior under failure scenarios the protocols are supposed to tolerate. The Mlo membership protocols assume different system models, and depend on quite different sets of underlying services. Even though their specifications contain properties that cannot be evaluated accurately in a distributed platform, our testing environment overcomes this limitation. The tests performed uncovered several flaws in the implementations.