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

摘要：

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

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

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家重点研发计划;国家自然科学基金;北京航空航天大学软件开发环境国家重点实验室开放课题

在线出版日期：2023-11-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共19页

页码：4989-5007