共识协议的形式化验证研究现状与展望

来源：软件学报杂志2023年第11期北京时间：

作者：葛宁，贺俞凯，翟树茂，李晓洲，张莉

单位：葛宁，北京航空航天大学 软件学院, 北京 100191;软件开发环境国家重点实验室 (北京航空航天大学), 北京 10019111,贺俞凯，北京航空航天大学 软件学院, 北京 10019102,翟树茂，北京航空航天大学 软件学院, 北京 10019103,李晓洲，北京航空航天大学 软件学院, 北京 10019104,张莉，北京航空航天大学 软件学院, 北京 100191;北京航空航天大学 计算机学院, 北京 100191;软件开发环境国家重点实验室 (北京航空航天大学), 北京 10019105

摘要：分布式系统在计算环境中发挥重要的作用, 其中的共识协议算法用于保证节点间行为的一致性. 共识协议的设计错误可能导致系统运行故障, 严重时可能对人员和环境造成灾难性的后果, 因此保证共识协议设计的正确性非常重要. 形式化验证能够严格证明设计模型中目标性质的正确性, 适合用于验证共识协议. 然而, 随着分布式系统的规模增大, 问题复杂度提升, 使得分布式共识协议的形式化验证更为困难. 采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模, 是共识协议形式化验证的重要研究问题. 对目前采用形式化方法验证共识协议的研究工作进行调研, 总结其中提出的重要建模方法和关键验证技术, 并展望该领域未来有潜力的研究方向.

关键词：共识协议;形式化验证;限界模型检测;定理证明;布尔表达式可满足性理论;可满足性模理论

基金资助：国家重点研发计划(2018YFB1402700); 国家自然科学基金(61902011); 北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)