摘要:Raft是最为流行的分布式共识协议之一. 自2014年被提出以来, Raft协议及其变体在各种分布式系统中被广泛应用. 为了证明Raft协议的正确性, 开发者使用TLA+形式化规约对协议设计进行了建模和验证. 但由于抽象的形式化规约与实际的系统实现源码间存在鸿沟, 基于Raft实现的分布式系统中仍然会违背协议设计并引入复杂的缺陷. 设计基于TLA+形式化规约的测试方法来检测Raft协议实现中的缺陷. 具体而言, 将形式化规约匹配到相应的系统实现, 并用形式化规约所定义的状态空间来指导系统实现的测试过程. 为评估所提方法的可行性和有效性, 针对两个不同的Raft实现进行系统化测试, 并发现3个未知缺陷.