基于TLA+形式化规约的Raft协议测试

来源：软件学报杂志2024年第12期北京时间：

作者：王栋，窦文生，高钰，吴陈傲，魏峻，黄涛

单位：王栋，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,窦文生，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,高钰，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,吴陈傲，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904,魏峻，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004905,黄涛，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004906

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

关键词：Raft;分布式系统;软件测试;模型检查

基金资助：国家自然科学基金(62072444, 62302493); 国家自然科学基金联合基金(U20A6003)