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

Ya Nan Li; Yu Xin Deng; Jing Liu

doi:10.13328/j.cnki.jos.005960

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

Translated title of the contribution: Formal Modeling and Verification of Paxos Based on Coq

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

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

Research output: Contribution to journal › Article › peer-review

2 Scopus citations

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.

Translated title of the contribution	Formal Modeling and Verification of Paxos Based on Coq
Original language	Chinese (Traditional)
Pages (from-to)	2362-2374
Number of pages	13
Journal	Ruan Jian Xue Bao/Journal of Software
Volume	31
Issue number	8
DOIs	https://doi.org/10.13328/j.cnki.jos.005960
State	Published - 1 Aug 2020

Access to Document

10.13328/j.cnki.jos.005960

Cite this

@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形式化建模与验证

Abstract

Access to Document

Other files and links

Fingerprint

Cite this