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

Ya Nan Li; Yu Xin Deng; Jing Liu

doi:10.13328/j.cnki.jos.005960

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

Ya Nan Li
, Yu Xin Deng^*
, Jing Liu

^*此作品的通讯作者

软件工程学院

East China Normal University

科研成果: 期刊稿件 › 文章 › 同行评审

2 引用（Scopus）

摘要

Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.

投稿的翻译标题	Formal Modeling and Verification of Paxos Based on Coq
源语言	繁体中文
页（从-至）	2362-2374
页数	13
期刊	Ruan Jian Xue Bao/Journal of Software
卷	31
期	8
DOI	https://doi.org/10.13328/j.cnki.jos.005960
出版状态	已出版 - 1 8月 2020

关键词

Basic Paxos
Coq
Distributed system
Theorem proof assistant
Verification

访问文件

10.13328/j.cnki.jos.005960

其它文件与链接

链接到 Scopus 的出版物

引用此

@article{087ad0a635db4ddaaee6d284ecb9d910,

title = "基于Coq的Paxos形式化建模与验证",

abstract = "Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.",

keywords = "Basic Paxos, Coq, Distributed system, Theorem proof assistant, Verification",

author = "Li, \{Ya Nan\} and Deng, \{Yu Xin\} and Jing Liu",

year = "2020",

month = aug,

day = "1",

doi = "10.13328/j.cnki.jos.005960",

language = "繁体中文",

volume = "31",

pages = "2362--2374",

journal = "Ruan Jian Xue Bao/Journal of Software",

issn = "1000-9825",

publisher = "Chinese Academy of Sciences",

number = "8",

}

TY - JOUR

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

AU - Li, Ya Nan

AU - Deng, Yu Xin

AU - Liu, Jing

PY - 2020/8/1

Y1 - 2020/8/1

N2 - Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.

AB - Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.

KW - Basic Paxos

KW - Coq

KW - Distributed system

KW - Theorem proof assistant

KW - Verification

UR - https://www.scopus.com/pages/publications/85089909456

U2 - 10.13328/j.cnki.jos.005960

DO - 10.13328/j.cnki.jos.005960

M3 - 文章

AN - SCOPUS:85089909456

SN - 1000-9825

VL - 31

SP - 2362

EP - 2374

JO - Ruan Jian Xue Bao/Journal of Software

JF - Ruan Jian Xue Bao/Journal of Software

IS - 8

ER -

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

摘要

关键词

访问文件

其它文件与链接

指纹

引用此