一句话：提出以 TLA+ 抽象形式模型覆盖率为引导的分布式系统模糊测试算法，更快发现更多缺陷。
分布式系统实现的状态空间巨大，纯随机测试难以触及协议设计者关心的关键状态。本文提出覆盖率引导的测试算法，核心创新是用系统在协议设计早期常被构建的抽象形式模型来定义覆盖率。作者以 TLA+ 编写抽象模型并实现模糊测试器，用模型覆盖率引导随机测试生成，以覆盖实现状态空间中有意义的点。在 Two-Phase Commit、Etcd-raft 与 RedisRaft 等共识协议实现上的评估表明，相较纯随机探索和基于不同调度器覆盖率与变异概念的随机探索，该方法持续获得更高覆盖率并更快发现缺陷，共发现 12 个此前未知的缺陷，其中 4 个只能由模型引导的模糊测试检出。
We present a coverage-guided testing algorithm for distributed systems implementations. Our main innovation is the use of an abstract formal model of the system that is used to define coverage. Such abstract models are frequently developed in the early phases of protocol design and verification but are infrequently used at testing time. We show that guiding random test generation using model coverage can be effective in covering interesting points in the implementation state space. We have implemented a fuzzer for distributed system implementations and abstract models written in TLA+. Our algorithm achieves better coverage over purely random exploration as well as random exploration guided by different notions of scheduler coverage and mutation. In particular, we show consistently higher coverage on implementations of distributed consensus protocols such as Two-Phase Commit and the Raft implementations in Etcd-raft and RedisRaft and detect bugs faster. Moreover, we discovered 12 previously unknown bugs in their implementations, four of which could only be detected by model-guided fuzzing.
@article{paperbot3004,
title = {Model-Guided Fuzzing of Distributed Systems},
author = {Ege Berkay Gulcan and Burcu Kulahcioglu Ozkan and Rupak Majumdar and Srinidhi Nagendra},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763060}
}