Multi-Grained Specifications for Distributed System Model Checking and Verification

Lingzhi Ouyang, Xudong Sun, Ruize Tang +4

This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained…