MET：基于模型检查的 CRDT 设计与实现探索性测试
分布式、并行与集群计算
2022-05-02 v1 软件工程
摘要
互联网规模的分布式系统常在多个地理位置复制数据，以提供低延迟和高可用性。无冲突复制数据类型（Conflict-free Replicated Data Type，CRDT）是一种为数据副本间维护最终一致性提供原则性方法的框架。CRDT 的设计与实现正确与否历来极为困难。细微的深层缺陷隐藏于对所有冲突数据更新可能情形的复杂而繁琐的处理中。我们认为 CRDT 设计应被形式化规约并模型检查，以揭示深层缺陷。其实现还需被系统性测试。一方面，测试需继承模型检查的穷尽性并确保测试覆盖；另一方面，测试应发现设计层验证无法检测到的编码错误。针对上述挑战，我们提出模型检查驱动的探索性测试（Model Checking-driven Explorative Testing，MET）框架。在设计层，MET 使用 TLA+ 规约并模型检查 CRDT 设计。在实现层，MET 实施模型检查驱动的探索性测试，即测试用例由模型检查轨迹自动生成。系统执行被控制为沿模型检查轨迹确定性推进。该探索性测试系统性地控制并置换所有非确定性消息重排。我们将 MET 应用于 CRDT 的实际开发中，发现了设计与实现中的缺陷。对于传统测试技术可发现的缺陷，MET 大幅降低了修复成本。此外，MET 能以合理成本发现现有技术无法发现的细微深层缺陷。我们进一步讨论了 MET 如何使我们对 CRDT 设计与实现的正确性获得充分信心。
引用
@article{arxiv.2204.14129,
title = {MET: Model Checking-Driven Explorative Testing of CRDT Designs and Implementations},
author = {Yuqi Zhang and Yu Huang and Hengfeng Wei and Xiaoxing Ma},
journal= {arXiv preprint arXiv:2204.14129},
year = {2022}
}