基于Coq的Paxos形式化建模与验证

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

作者：李亚男，邓玉欣，刘静

单位：李亚男，上海市高可信计算重点实验室(华东师范大学), 上海 20006211,邓玉欣，上海市高可信计算重点实验室(华东师范大学), 上海 20006202,刘静，上海市高可信计算重点实验室(华东师范大学), 上海 20006203

摘要：Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用，比如区块链系统以及谷歌文件系统等，其安全性证明越来越重要.在定理证明工具Coq中，形式化描述和定义了Lamport的Basic Paxos算法，并且证明了其满足共识性.

关键词：分布式系统;Basic Paxos;定理证明工具;Coq;验证

基金资助：国家自然科学基金（61672229，61832015）