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

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

Berlin: Springer, 2004.
[21] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin, Heidelberg: Springer, 2002.
[22] Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon Web services uses formal methods.
Communications of the ACM, 2015, 58(4): 66–73. [doi: 10.1145/2699417]
[23] Hackett F, Rowe J, Kuppe MA. Understanding inconsistency in Azure Cosmos DB with TLA+. In: Proc. of the 45th Int’l Conf. on
Software Engineering: Software Engineering in Practice. Melbourne: IEEE, 2023. 1–12. [doi: 10.1109/ICSE-SEIP58684.2023.00006]
[24] Zhou SY, Mu S. Fault-tolerant replication with pull-based consensus in MongoDB. In: Proc. of the 18th USENIX Symp. on Networked
Systems Design and Implementation. USENIX Association, 2021. 687–703.
[25] TLA+ specifications for TiDB. 2018. https://github.com/pingcap/tla-plus
[26] P specifications in DeepSeek 3FS. 2025. https://github.com/deepseek-ai/3FS/tree/main/specs
[27] Jhala R, Majumdar R. Software model checking. ACM Computing Surveys (CSUR), 2009, 41(4): 21. [doi: 10.1145/1592434.1592438]
[28] Bu L, Chen LQ, Chen Z, et al. Research progress and trend of formal methods. In: China Computer Federation, ed. CCF 2017–2018
China Computer Science and Technology Development Report. Beijing: China Machine Press, 2018 (in Chinese).
[29] Godefroid P, Sen K. Combining model checking and testing. In: Clarke EM, Henzinger TA, Veith H, Bloem R, eds. Handbook of Model
Checking. Cham: Springer, 2018. 613–649. [doi: 10.1007/978-3-319-10575-8_19]
[30] Chen YL, Ma FC, Zhou YH, Yan Z, Jiang Y, Sun JG. Survey on dynamic testing technologies for distributed systems. Ruan Jian Xue
Bao/Journal of Software, 2025, 36(7): 2964–3002 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/7334.htm [doi:
10.13328/j.cnki.jos.007334]
[31] Ge N, He YK, Zhai SM, Li XZ, Zhang L. Formal verification of consensus protocols: Survey and perspective. Ruan Jian Xue
Bao/Journal of Software, 2023, 34(11): 4989–5007 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6684.htm [doi:
10.13328/j.cnki.jos.006684]
[32] Hou G, Zhou KJ, Yong JW, Ren LT, Wang XL. Survey of state explosion problem in model checking. Computer Science, 2013,
40(6A): 77–86, 111 (in Chinese with English abstract). [doi: 10.3969/j.issn.1002-137X.2013.z1.018]
[33] Wang ZY, Wu SS, Cao QX. Survey on interactive theorem proving based concurrent program verification. Ruan Jian Xue Bao/Journal
of Software, 2024, 35(9): 4069–4099 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/7138.htm [doi: 10.13328/j.
cnki.jos.007138]
[34] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston: Addison-Wesley
Longman Publishing Co., 2002.
[35] TLC and TLA+ toolbox. TLA+. 2025. https://github.com/tlaplus/tlaplus
[36] Lamport L. TLA+ specifications for Paxos. 2019. https://github.com/tlaplus/Examples/tree/master/specifications/Paxos
[37] Ongaro D. TLA+ specifications for Raft. 2014. https://github.com/ongardie/raft.tla
[38] Lü J, Ma XX, Tao XP, Cao C, Huang Y, Yu P. On environment-driven software model for internetware. SCIENTIA SINICA
Technologica, 2008, 38(6): 864–900 (in Chinese). [doi: 10.3321/j.issn:1006-9275.2008.06.005]
[39] Lü J, Ma XX, Tao XP, Huang Y, Yu P, Xu C. Explicit environmental constructs for internetware. SCIENTIA SINICA Informationis,
2013, 43(1): 1–23 (in Chinese with English abstract). [doi: 10.1360/112012-527]
[40] Guo HY, Wu M, Zhou LD, Hu G, Yang JF, Zhang LT. Practical software model checking via dynamic interface reduction. In: Proc. of
the 23rd ACM Symp. on Operating Systems Principles. Cascais: ACM, 2011. 265–278. [doi: 10.1145/2043556.2043582]
[41] Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565. [doi:
10.1145/359545.359563]
[42] Musuvathi M, Park DYW, Chou A, Engler DR, Dill DL. CMC: A pragmatic approach to model checking real code. In: Proc. of the 5th
Symp. on Operating Systems Design and Implementation. Boston: USENIX Association, 2002. 75–88.
[43] Musuvathi M, Engler DR. Model checking large network protocol implementations. In: Proc. of the 1st Conf. on Symp. on Networked
Systems Design and Implementation. San Francisco: USENIX Association, 2004. 12.
[44] Killian CE, Anderson JW, Braud R, Jhala R, Vahdat AM. Mace: Language support for building distributed systems. In: Proc. of the 28th
ACM SIGPLAN Conf. on Programming Language Design and Implementation. San Diego: ACM, 2007. 179–188. [doi: 10.1145/
1250734.1250755]
[45] Killian C, Anderson JW, Jhala R, Vahdat A. Life, death, and the critical transition: Finding liveness bugs in systems code. In: Proc. of
the 4th USENIX Conf. on Networked Systems Design & Implementation. Cambridge: USENIX Association, 2007. 18.
[46] Fredlund. McErlang. 2007. https://github.com/fredlund/McErlang
[47] Fredlund LÅ, Svensson H. McErlang: A model checker for a distributed functional programming language. In: Proc. of the 12th ACM