| 基于Coq的Paxos形式化建模与验证 |
| |
| 引用本文： | 李亚男,邓玉欣,刘静.基于Coq的Paxos形式化建模与验证[J].软件学报,2020,31(8):2362-2374. |
| |
| 作者姓名： | 李亚男 邓玉欣 刘静 |
| |
| 作者单位： | 上海市高可信计算重点实验室(华东师范大学),上海200062;上海市高可信计算重点实验室(华东师范大学),上海200062;上海市高可信计算重点实验室(华东师范大学),上海200062 |
| |
| 基金项目： | 国家自然科学基金（61672229，61832015） |
| |
| 摘 要： | Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用，比如区块链系统以及谷歌文件系统等，其安全性证明越来越重要.本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法，并且证明了其满足共识性.
|
| 关 键 词： | 分布式系统 Basic Paxos 定理证明工具 Coq 验证 |
| 收稿时间： | 2019/8/31 0:00:00 |
| 修稿时间： | 2019/12/30 0:00:00 |
Formal Modeling and Verification of Paxos Based on Coq |
| |
| LI Ya-Nan,DENG Yu-Xin,LIU Jing.Formal Modeling and Verification of Paxos Based on Coq[J].Journal of Software,2020,31(8):2362-2374. |
| |
| Authors: | LI Ya-Nan DENG Yu-Xin LIU Jing |
| |
| Affiliation: | Shanghai Key Laboratory of Trustworthy Computing(East China Normal University), Shanghai 200062, China |
| |
| Abstract: | |
| |
| Keywords: | distributed system Basic Paxos proof assistant Coq verification |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
