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