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

Raft Protocol Testing Based on TLA+Formal

作　　者：王栋[1,2] 窦文生 高钰[1,2] 吴陈傲 魏峻 黄涛 WANG Dong;DOU Wen-Sheng;GAO Yu;WU Chen-Ao;WEI Jun;HUANG Tao(State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [2]中国科学院大学,北京100049

出　　处：《软件学报》2024年第12期5363-5381,共19页Journal of Software

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

摘　　要：Raft是最为流行的分布式共识协议之一.自2014年被提出以来,Raft协议及其变体在各种分布式系统中被广泛应用.为了证明Raft协议的正确性,开发者使用TLA+形式化规约对协议设计进行了建模和验证.但由于抽象的形式化规约与实际的系统实现源码间存在鸿沟,基于Raft实现的分布式系统中仍然会违背协议设计并引入复杂的缺陷.设计基于TLA+形式化规约的测试方法来检测Raft协议实现中的缺陷.具体而言,将形式化规约匹配到相应的系统实现,并用形式化规约所定义的状态空间来指导系统实现的测试过程.为评估所提方法的可行性和有效性,针对两个不同的Raft实现进行系统化测试,并发现3个未知缺陷.formal specification and practical implementation,distributed systems that implement the Raft protocol can still violate the protocol design and introduce intricate bugs.This study proposes a novel testing technique based on TLA+formal specification to unearth bugs in Raft implementations.To be specific,the study maps the formal specification to the corresponding system implementation and then uses the specification-defined state space to guide the testing in the implementations.To evaluate the feasibility and effectiveness of the proposed approach,the study applies it on two different Raft implementations and finds 3 previously unknown bugs.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]