| 本文已被：浏览 1743次 下载 4096次 |
码上扫一扫！ |
|
|
| 基于TLA+形式化规约的Raft协议测试 |
|
王栋1,2, 窦文生1,2, 高钰1,2, 吴陈傲1,2, 魏峻1,2, 黄涛1,2
|
|
1.计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;2.中国科学院大学, 北京 100049
|
|
| 摘要: |
| Raft是最为流行的分布式共识协议之一. 自2014年被提出以来, Raft协议及其变体在各种分布式系统中被广泛应用. 为了证明Raft协议的正确性, 开发者使用TLA+形式化规约对协议设计进行了建模和验证. 但由于抽象的形式化规约与实际的系统实现源码间存在鸿沟, 基于Raft实现的分布式系统中仍然会违背协议设计并引入复杂的缺陷. 设计基于TLA+形式化规约的测试方法来检测Raft协议实现中的缺陷. 具体而言, 将形式化规约匹配到相应的系统实现, 并用形式化规约所定义的状态空间来指导系统实现的测试过程. 为评估所提方法的可行性和有效性, 针对两个不同的Raft实现进行系统化测试, 并发现3个未知缺陷. |
| 关键词: Raft 分布式系统 软件测试 模型检查 |
| DOI：10.13328/j.cnki.jos.007066 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金(62072444, 62302493); 国家自然科学基金联合基金(U20A6003) |
|
| Raft Protocol Testing Based on TLA+ Formal Specification |
|
WANG Dong1,2, DOU Wen-Sheng1,2, GAO Yu1,2, WU Chen-Ao1,2, WEI Jun1,2, HUANG Tao1,2
|
|
1.State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;2.University of Chinese Academy of Sciences, Beijing 100049, China
|
| Abstract: |
| Raft is one of the most popular distributed consensus protocols. Since it was proposed in 2014, Raft and its variants have been widely used in different kinds of distributed systems. To prove the correctness of the Raft protocol, developers use the TLA+ formal specification to model and verify its design. However, due to the gap between the abstract 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. |
| Key words: Raft distributed system software testing model checking |
