%0 Journal Article
%T 基于Coq的Paxos形式化建模与验证
%A 刘静
%A 李亚男
%A 邓玉欣
%J -
%D 2020
%R 10.13328/j.cnki.jos.005960
%X Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用，比如区块链系统以及谷歌文件系统等，其安全性证明越来越重要.本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法，并且证明了其满足共识性
%K 分布式系统 Basic Paxos 定理证明工具 Coq 验证
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=5960&flag=1