微信服务号

微信订阅号

2025年3月30日 14:27 星期日
首页 > 过刊浏览>2020年第31卷第8期 >2362-2374. DOI:10.13328/j.cnki.jos.005960
PDF HTML阅读 XML下载 导出引用 引用提醒
基于Coq的Paxos形式化建模与验证
作者:
作者简介:

李亚男(1992-),男,硕士,主要研究领域为形式化方法;刘静(1964-),女,博士,教授,博士生导师,CCF专业会员,主要研究领域为可信软件,模型驱动式软件开发方法,面向服务的软件架构;邓玉欣(1978-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法.

通讯作者:

邓玉欣,E-mail:yxdeng@sei.ecnu.edu.cn

基金项目:

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


Formal Modeling and Verification of Paxos Based on Coq
Author:
Fund Project:

National Natural Science Foundation of China (61672229, 61832015)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [23]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    参考文献
    [1] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development:Coq' Art:The Calculus of Inductive Constructions. Springer Science & Business Media, 2013.
    [2] Gonthier G. A computer-checked proof of the four colour theorem. 2005. https://www.cl.cam.ac.uk/~lp15/Pages/4colproof.pdf
    [3] Paulin-Mohring C. Circuits as streams in Coq:Verification of a sequential multiplier. In:Proc. of the Int'l Workshop on Types for Proofs and Programs. Springer-Verlag, 1995. 216-230.
    [4] Leroy X. Formal certification of a compiler back-end or:Programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006,41(1):42-54.
    [5] Affeldt R, Kobayashi N. Formalization and verification of a mail server in Coq. In:Proc. of the Int'l Symp. on Software Security. Springer-Verlag, 2002. 217-233.
    [6] Deng YX, Monin JF. Verifying self-stabilizing population protocols with Coq. In:Proc. of the 3rd IEEE Int'l Symp. on Theoretical Aspects of Software Engineering. IEEE, 2009. 201-208.
    [7] Lamport L. The part-time parliament. ACM Trans. on Computer Systems, 1998,16(2):133-169.
    [8] Burrows M. The Chubby lock service for loosely-coupled distributed systems. In:Proc. of the 7th Symp. on Operating Systems Design and Implementation. USENIX Association, 2006. 335-350.
    [9] Isard M. Autopilot:Automatic data center management. ACM SIGOPS Operating Systems Review, 2007,41(2):60-67.
    [10] Zheng JJ, Lin Q, Xu JT, Wei C, Zeng CW, Yang PA, Zhang YF. Paxos store:High-availability storage made practical in wechat. Proc. of the VLDB Endowment, 2017,10(12):1730-1741.
    [11] Lamport L. My writings. 2019. http://lamport.azurewebsites.net/pubs/pubs.html#lamport-paxos
    [12] Lamport L, et al. Paxos made simple. ACM SIGACT News, 2001,32(4):18-25.
    [13] Lamport L. Specifying Systems:The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
    [14] Microsoft Research-Inria Joint Center. TLA+Proof System (TLAPS). 2019. http://tla.msr-inria.inria.fr/tlaps
    [15] Chand S, Liu YA, Dstoller S. Formal verification of multi-Paxos for distributed consensus. In:Proc. of the Int'l Symp. on Formal Methods. Springer-Verlag, 2016. 119-136.
    [16] Kellomäki P. An annotated specification of the consensus protocol of Paxos using superposition in PVS. Technical Report, No.36, Institute of Software Systems, Tampere University of Technology, 2004.
    [17] Jaskelioff M, Merz S. Proving the correctness of disk Paxos. In:The Archive of Formal Proofs, 2005. http://afp.sf.net/entries/DiskPaxos.shtml
    [18] Padon O, Losa G, Sagiv M, Shoham S. Paxos made EPR:Decidable reasoning about distributed protocols. In:Proc. of the ACM on Programming Languages 1(OOPSLA), 2017. 108:1-108:31.
    [19] García-Pérez Á, Gotsman A, Meshman Y, Sergey I. Paxos consensus, deconstructed and abstracted. In:Proc. of the European Symp. on Programming. Cham:Springer-Verlag, 2018. 912-939.
    [20] Lamport L. Byzantizing Paxos by refinement. In:Proc. of the Int'l Symp. on Distributed Computing. Springer-Verlag, 2011. 211-224.
    [21] The Coq Development Team. The Coq Proof Assistant Reference Manual. 2019. https://coq.inria.fr/distrib/current/refman
    [22] Lamport L. Fast Paxos. Distributed Computing, 2006,19(2):79-103.
    [23] Chandra TD, Griesemer R, Redstone J. Paxos made live:An engineering perspective. In:Proc. of the 26th Annual ACM Symp. on Principles of Distributed Computing. ACM, 2007. 398-407.
    引证文献
引用本文

李亚男,邓玉欣,刘静.基于Coq的Paxos形式化建模与验证.软件学报,2020,31(8):2362-2374

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2019-08-31
  • 最后修改日期:2019-11-02
  • 在线发布日期: 2020-04-20
  • 出版日期: 2020-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号