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

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

service. In: Proc. of the 9th Int’l Symp. on Dependable Software Engineering. Theories, Tools, and Applications. Nanjing: Springer,
2023. 189–205. [doi: 10.1007/978-981-99-8664-4_11]
[125] Bornholt J, Joshi R, Astrauskas V, Cully B, Kragl B, Markle S, Sauri K, Schleit D, Slatton G, Tasiran S, van Geffen J, Warfield A.
Using lightweight formal methods to validate a key-value storage node in Amazon S3. In: Proc. of the 28th ACM SIGOPS Symp. on
Operating Systems Principles. ACM, 2021. 836–850. [doi: 10.1145/3477132.3483540]
[126] Schultz W. Fixing a MongoDB replication protocol bug with TLA+. 2019. https://youtu.be/x9zSynTfLDE
[127] Davis AJJ, Hirschhorn M, Schvimer J. Extreme modelling in practice. Proc. of the VLDB Endowment, 2020, 13(9): 1346–1358. [doi: 10.
14778/3397230.3397233]
[128] Jackson D. Software Abstractions: Logic, Language, and Analysis. Cambridge: The MIT Press, 2012.
[129] The TLA+ proof manager. 2019. https://github.com/tlaplus/tlapm
+
[130] Newcombe C. Why Amazon chose TLA . In: Proc. of the 4th Int’l Conf. on Abstract State Machines. Toulouse: Springer, 2014. 25–39.
[doi: 10.1007/978-3-662-43652-3_3]
[131] Hackett F, Hosseini S, Costa R, Do M, Beschastnikh I. Compiling distributed system models with PGo. In: Proc. of the 28th ACM Int’l
Conf. on Architectural Support for Programming Languages and Operating Systems. Vancouver: ACM, 2023. 159–175. [doi: 10.1145/
3575693.3575695]
[132] Nadal J. Stateright/Stateright. 2018. https://github.com/stateright/stateright
[133] FizzBee. FizzBee—Design reliable, scalable distributed systems. 2024. https://fizzbee.io/
[134] Abadi M, Lamport L. The existence of refinement mappings. In: Proc. of the 3rd Annual Symp. on Logic in Computer Science.
Edinburgh: IEEE, 1988. 165–175. [doi: 10.1109/LICS.1988.5115]
[135] Pressler R. Conjunction capers: A TLA+ truffle. 2020. https://conf.tlapl.us/2020/04-Ron_Pressler-TLA+_Truffle_Composition_Capers-
Slides.pdf
[136] Howard Y, Gruner S, Gravell A, Ferreira C, Augusto JC. Model-based trace-checking. arXiv:1111.2825, 2011.
+
[137] Cirstea H, Kuppe MA, Loillier B, Merz S. Validating traces of distributed programs against TLA specifications. In: Madeira A, Knapp
A. Software Engineering and Formal Methods. Cham: Springer, 2025. 126–143. [doi: 10.1007/978-3-031-77382-2_8]
[138] Zhang YQ, Huang Y, Wei HF, Ma XX. Model-checking-driven explorative testing of CRDT designs and implementations. Journal of
Software: Evolution and Process, 2024, 36(4): e2555. [doi: 10.1002/smr.2555]
[139] Rosa C, Merz S, Quinson M. A simple model of communication APIs—Application to dynamic partial-order reduction. In: Proc. of the
10th Int’l Workshop on Automated Verification of Critical Systems. Düsseldorf: AVOCS, 2010.
[140] TLA+ community modules. 2019. https://github.com/tlaplus/CommunityModules
[141] Mukherjee S, Deligiannis P, Biswas A, Lal A. Learning-based controlled concurrency testing. Proc. of the ACM on Programming
Languages, 2020, 4(OOPSLA): 230. [doi: 10.1145/3428298]
[142] Cao JL, Lu YJ, Li MZN, Ma HY, Li HK, He MD, Wen C, Sun L, Zhang HY, Qin SC, Cheung SC, Tian C. From informal to
formal—Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. In: Proc. of the 63rd Annual
Meeting of the Association for Computational Linguistics. Vienna: ACL, 2025. 26984–27003. [doi: 10.18653/v1/2025.acl-long.1310]

附中文参考文献
[13] 阿里云. 关于阿里云香港 Region 可用区 C 服务中断事件的说明. 2022. https://cn.aliyun.com/noticelist/articleid/1061819219.html
[14] 阿里云. [异常(已恢复)]阿里云云产品控制台服务异常. 2023. https://cn.aliyun.com/noticelist/articleid/1064981333.html
[28] 卜磊, 陈立前, 陈哲, 等. 形式化方法的研究进展与趋势. 见: 中国计算机学会. CCF 2017–2018 中国计算机科学技术发展报告. 北
京: 机械工业出版社, 2018.
[30] 陈元亮, 马福辰, 周远航, 颜臻, 姜宇, 孙家广. 分布式系统动态测试技术研究综述. 软件学报, 2025, 36(7): 2964–3002. http://www.
jos.org.cn/1000-9825/7334.htm [doi: 10.13328/j.cnki.jos.007334]
[31] 葛宁, 贺俞凯, 翟树茂, 李晓洲, 张莉. 共识协议的形式化验证研究现状与展望. 软件学报, 2023, 34(11): 4989–5007. http://www.jos.
org.cn/1000-9825/6684.htm [doi: 10.13328/j.cnki.jos.006684]
[32] 侯刚, 周宽久, 勇嘉伟, 任龙涛, 王小龙. 模型检测中状态爆炸问题研究综述. 计算机科学, 2013, 40(6A): 77–86, 111. [doi:
10.3969/j.issn.1002-137X.2013.z1.018]
[33] 王中烨, 吴姝姝, 曹钦翔. 基于交互式定理证明的并发程序验证工作综述. 软件学报, 2024, 35(9): 4069–4099. http://www.jos.org.cn/
1000-9825/7138.htm [doi: 10.13328/j.cnki.jos.007138]
[38] 吕建, 马晓星, 陶先平, 曹春, 黄宇, 余萍. 面向网构软件的环境驱动模型与支撑技术研究. 中国科学: 技术科学, 2008, 38(6):