Page 289 - 《软件学报》2026年第5期

2168 软件学报 2026 年第 37 卷第 5 期

1 引 言

随着互联网、大数据和云计算的快速发展, 分布式系统已在诸多领域获得大规模的部署和应用 [1−3] . 分布
式系统由一组通过网络通信的计算节点组成, 共同完成数据存储、处理和计算等任务, 并向外提供服务. 这些
系统旨在实现高性能处理、负载均衡、高可用性和容错性等需求, 是支撑现代计算领域的基础设施. 例如, 分
布式数据库 [2,4] 、分布式协调服务 [5,6] 以及大数据处理平台 [1,7] 等, 广泛应用于电子商务、云计算和大数据处理
等领域.
然而, 正确实现分布式系统面临诸多挑战, 这体现在分布式系统所处的复杂计算环境和分布式系统自身复杂
的代码实现中. 计算环境中存在高度的不确定性, 它主要由网络和外设交互的异步性、并发性和易错性引起, 例
如, 网络消息延迟或乱序到达、异步磁盘读写、时钟超时、高度并发的客户端请求、节点宕机和网络分区故障
等. 为了应对计算环境带来的不确定性, 并向上层应用提供可理解、易编程的抽象, 分布式系统通常需要精巧的协
[9]
[8]
议设计 (例如 Paxos 、Raft 和 Zab [6,10] ) 和复杂的系统实现. 这种复杂性使得系统更容易引入细微但致命的缺陷,
而这些缺陷往往只在由计算环境的不确定性触发的极端调度条件下才会显现, 因此在测试环境中难以发现、定位
与修复. 这类依赖特定调度、触发路径极深的问题被称为深层缺陷 [11] . 尽管在测试阶段难以暴露, 深层缺陷却可
能在分布式系统大规模部署和长时间运行中被触发.
分布式系统中的深层缺陷将导致数据丢失、数据不一致和服务不可用等严重后果. 由于分布式系统支撑着众
多重要系统的运行, 任何一个细微的缺陷可能带来巨大的损失. 这些年来, 即便是成熟的工业级系统也时常出错,
并造成巨大损失. 例如, 2019 年, 美国 Google 公司由于存储服务负载均衡存在缺陷, 导致配置变更时引发级联故
障, 影响了包括北美和南美在内的多个地区, 造成谷歌服务中断超过 3 h [12] . 此外, 阿里云在 2022–2023 年期间发生
了两次重大故障, 分别导致香港地区服务中断超过 15 h、全球核心业务宕机超过 3 h, 进而影响了阿里系多个核心
产品 (如淘宝、钉钉等) 的正常使用 [13,14] .
提升分布式系统正确性的方法主要包括测试和形式化验证. 两者都能发现系统中的缺陷, 但关键的区别在于
是否能提供系统正确性保证. 决定是否采用测试或形式化验证的关键因素在于技术的使用成本. 测试技术成本较
低, 实用性较强, 能够发现大部分浅层缺陷. 然而, 由于分布式系统的复杂性和不确定性, 依赖测试人员和开发者编
[15]
写的单元测试和集成测试只能覆盖少量的执行路径. 自动化程度更高的随机测试或压力测试 (如 Jepsen 、Chaos [16]
和 Fuzzing [17] ) 能探索更多的系统执行路径, 但它们无法提供状态空间的覆盖保证, 也难以在后续测试中确定性地
重现已经发现的缺陷, 这使得分布式系统中的深层缺陷的诊断和修复变得异常困难.
形式化验证技术相较于测试成本更高, 它采用数学的方法对系统的正确性进行证明, 有效解决了测试中缺陷
发现难、复现难和修复难等问题, 主要包括模型检验 (model checking) [18] 和定理证明 (theorem proving) [19] 两种方式.
定理证明要求使用者利用程序逻辑 (如霍尔逻辑) 进行数学证明, 并借助工具 (如 Coq [20] 、Isabelle/HOL [21] ) 自动化
或半自动化地检查数学命题是否成立. 尽管这种方法提供全面的正确性保证, 但它的使用门槛较高, 且学习曲线陡
峭, 限制了它在工业界的广泛应用.
模型检验通过自动化地对系统模型进行状态空间的系统性穷尽式探索, 确保所有可能的状态都得到验证, 其
穷尽式的验证方式特别适合应对分布式系统中由不确定性引发的“缺陷难发现、难诊断、难修复”的挑战. 不过,
由于状态空间往往呈指数级增长, 模型检验仍面临严重的状态爆炸 (state explosion) 问题. 近年来, 研究者提出了对
称约减、偏序约减等多种优化技术, 配合工具链的不断成熟和计算能力的提升, 有效缓解了状态爆炸问题, 显著提
升了模型检验的实用性, 其适用范围也在持续拓展, 尤其在工业场景中正逐步落地应用 [22−26] .
1.1 分布式模型检验技术概述
模型检验具备高度自动化、严格正确性保障等优点, 但传统模型检验技术主要针对系统的抽象模型而非系统
的代码实现展开验证, 面临系统模型与真实代码之间的语义鸿沟 (semantic gap) 问题, 验证结果受到转译错误
(transcription error) 的制约, 仅针对模型的验证结果通常无法准确反映真实系统的情况. 分布式系统模型检验