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

作     者：王栋 窦文生 高钰 吴陈傲 魏峻 黄涛 WANG Dong;DOU Wen-Sheng;GAO Yu;WU Chen-Ao;WEI Jun;HUANG Tao

作者机构：计算机科学国家重点实验室(中国科学院软件研究所)北京100190 中国科学院大学北京100049 

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2024年第35卷第12期

页      码：5363-5381页

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

主 题 词：Raft 分布式系统 软件测试 模型检查 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.13328/j.cnki.jos.007066

馆 藏 号：203155707...