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

唐瑞泽 等: 分布式系统模型检验技术研究进展 2195

成规约的可能性 [142] . 尽管生成的规约尚存在语法错误、幻觉及处理长代码片段时准确率下降的问题, 但可预见未
来 LLM 生成规约的质量将持续提升. 结合代码-模型互动机制, 还可进一步增强生成规约的正确性.
(4) 面向一致性检查的轻量级形式化方法设计: 规约语言与真实代码之间的差异是导致分歧分析成本高的关
键原因. 未来可以通过更贴近代码语义的规约语言设计与工具链建设, 减少手工适配成本. 同时, 在一致性比对中,
引入大语言模型辅助分析、自动修正规约或代码, 也将有助于降低人工成本、提升易用性.
(5) 支持持续集成的增量式 DMCK: 分布式系统在演进过程中, 其代码不断变化, 当前多数 DMCK 工具除上
手成本较高外, 往往只在一次性验证场景中使用, 缺乏持续性维护机制, 容易导致规约与代码产生分歧, 进而影响
验证结果的可信度. 随着 DevOps 与持续集成 (CI) 流程的普及, 已有研究将互动式 DMCK 与其派生方法集成至
CI 流程中, 推动规约与代码的协同演化 [122] . 未来, 结合轻量级形式化方法与自动化工具链的持续集成能力, 将成
为 DMCK 工具的重要发展方向.

References
[1] Dean J, Ghemawat S. MapReduce: Simplified data processing on large clusters. Communications of the ACM, 2008, 51(1): 107–113.
[doi: 10.1145/1327452.1327492]
[2] Corbett JC, Dean J, Epstein M, et al. Spanner: Google’s globally-distributed database. In: Proc. of the 10th USENIX Conf. on Operating
Systems Design and Implementation. Hollywood: USENIX Association, 2012. 261–264.
[3] Tanenbaum AS, van Steen M. Distributed Systems: Principles and Paradigms. 2nd ed., Upper Saddle River: Prentice-Hall, Inc., 2006.
[4] Taft R, Sharif I, Matei A, VanBenschoten N, Lewis J, Grieger T, Niemi K, Woods A, Birzin A, Poss R, Bardea P, Ranade A, Darnell B,
Gruneir B, Jaffray J, Zhang L, Mattis P. CockroachDB: The resilient geo-distributed SQL database. In: Proc. of the 2020 ACM
SIGMOD Int’l Conf. on Management of Data. Portland: ACM, 2020. 1493–1509. [doi: 10.1145/3318464.3386134]
[5] etcd. 2013. https://etcd.io/
[6] Hunt P, Konar M, Junqueira FP, Reed B. ZooKeeper: Wait-free coordination for Internet-scale systems. In: Proc. of the 2010 USENIX
Annual Technical Conf. Boston: USENIX Association, 2010. 145–158.
[7] Zaharia M, Xin RS, Wendell P, Das T, Armbrust M, Dave A, Meng XR, Rosen J, Venkataraman S, Franklin MJ, Ghodsi A, Gonzalez J,
Shenker S, Stoica I. Apache Spark: A unified engine for big data processing. Communications of the ACM, 2016, 59(11): 56–65. [doi:
10.1145/2934664]
[8] Lamport L. The part-time parliament. ACM Trans. on Computer Systems (TOCS), 1998, 16(2): 133–169. [doi: 10.1145/279227.279229]
[9] Ongaro D, Ousterhout J. In search of an understandable consensus algorithm. In: Proc. of the 2014 USENIX Annual Technical Conf.
Philadelphia: USENIX Association, 2014. 305–320.
[10] Junqueira FP, Reed BC, Serafini M. Zab: High-performance broadcast for primary-backup systems. In: Proc. of the 41st IEEE/IFIP Int’l
Conf. on Dependable Systems & Networks. Hong Kong: IEEE, 2011. 245–256. [doi: 10.1109/DSN.2011.5958223]
[11] Leesatapornwongsa T, Hao MZ, Joshi P, Lukman JF, Gunawi HS. SAMC: Semantic-aware model checking for fast discovery of deep
bugs in cloud systems. In: Proc. of the 11th USENIX Conf. on Operating Systems Design and Implementation. Broomfield: USENIX
Association, 2014. 399–414.
[12] Google Cloud. Google cloud networking incident #19009. 2019. https://status.cloud.google.com/incident/cloud-networking/19009
[13] Alibaba Cloud. Notice on the service interruption in Availability Zone C of the Alibaba Cloud Hong Kong region. 2022 (in Chinese).
https://cn.aliyun.com/noticelist/articleid/1061819219.html
[14] Alibaba Cloud. Notice on an abnormality in Alibaba Cloud console services (resolved). 2023 (in Chinese). https://cn.aliyun.com/
noticelist/articleid/1064981333.html
[15] Jepsen. Distributed systems safety research. 2013. https://jepsen.io/
[16] Chaos Monkey. 2010. https://netflix.github.io/chaosmonkey/
[17] Gao Y, Dou WS, Wang D, Feng WH, Wei J, Zhong H, Huang T. Coverage guided fault injection for cloud systems. In: Proc. of the 45th
Int’l Conf. on Software Engineering. Melbourne: IEEE, 2023. 2211–2223. [doi: 10.1109/ICSE48619.2023.00186]
[18] Graham SL, Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic
specifications. ACM Trans. on Programming Languages and Systems (TOPLAS), 1986, 8(2): 244–263. [doi: 10.1145/5397.5399]
[19] Gordon MJC, Melham TF. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. New York: Cambridge
University Press, 1993.
[20] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions.