摘要: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.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/5960
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
基于Coq的Paxos形式化建模与验证
本站小编 Free考研考试/2022-01-02
相关话题/系统 过程 网络 分布式 共识
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19基于Coq的操作系统任务管理需求层建模及验证
摘要:为确保星上操作系统中任务管理设计的可靠性，利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度，基于星上操作系统任务管理的基本机制，提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模，并在Coq中实现.针对建立的需求层模型，提出6条与实际星上 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向医学图像分割的半监督条件生成对抗网络
摘要:医学图像分割是计算机辅助诊断的关键技术.青光眼作为全球第二大致盲眼病，其早期筛查和临床诊断依赖于眼底图的视盘和视杯的准确分割.但传统的视盘和视杯分割方法采用人工构建特征，模型泛化能力差.近年来，基于卷积神经网络的端对端学习模型可通过自动发现特征来分割视盘和视杯，但由于标注样本有限，模型难以训练 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于意图的网络研究综述
摘要:随着互联网规模的不断增大，网络管理和运维变得极其复杂，网络自治成为未来网络发展的趋势，基于意图的网络（intent-basednetworking，简称IBN）应运而生.首先从IBN的定义入手，介绍学术界及产业界对IBN范畴及体系结构的描述，并概述IBN实现的闭环，包括意图获取、意图转译、策略 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于多尺度生成对抗网络的遮挡行人重识别方法
摘要:行人重识别是指在多个非重叠摄像头拍摄的场景下，给定一幅查询行人图像，从大规模行人图像库中检索出具有相同身份的行人图像，是一类特殊的图像检索任务.随着深度学习的不断发展，行人重识别方法的性能得到了显著提升.但是行人重识别在实际应用中经常遭遇遮挡问题（例如，背景遮挡、行人互相遮挡等）.由于遮挡图像 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02面向细粒度草图检索的对抗训练三元组网络
摘要:将草图作为检索示例用于图像检索称为基于草图的图像检索，简称草图检索.其中，细粒度检索问题或类内检索问题是2014年被研究者提出并快速成为广受关注的研究方向.目前研究者通常用三元组网络来解决类内检索问题，且取得了不错的效果.但是三元组网络的训练非常困难，很多情况下很难收敛甚至不收敛，且存在着容易 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02联合姿态先验的人体精确解析双分支网络模型
摘要:人体解析旨在将人体图像分割成多个具有细粒度语义的部件区域，进行形成对人体图像的语义理解.然而，由于人体姿态的复杂性，现有的人体解析算法容易对人体四肢部件形成误判，且对于小目标区域的分割不够精确.针对上述问题，联合人体姿态估计信息，提出了一种人体精确解析的双分支网络模型.该模型首先使用基干网络表 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于日志数据的分布式软件系统故障诊断综述
摘要:基于日志数据的故障诊断是指通过智能化手段分析系统运行时产生的日志数据以自动化地发现系统异常、诊断系统故障.随着智能运维（artificialintelligenceforIToperations，简称AIOps）的快速发展，该技术正成为学术界和工业界的研究热点.首先总结了基于日志数据的分布式软 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02分布式追踪技术综述
摘要:随着分布式软件系统在各个行业的广泛应用，如何提升系统运维效率，保障其服务的可靠与稳定，得到了学术界与工业界的关注.分布式软件系统其规模庞大、结构复杂、持续更新且大量服务请求并发执行的特点，给分布式软件系统的运维任务带来了严峻的挑战.传统的以组件/节点/进程/线程为中心的系统监控与追踪方法难以支 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于神经网络的机器阅读理解综述
摘要:机器阅读理解的目标是使机器理解自然语言文本，并能够正确回答与文本相关的问题.由于数据集规模的制约，早期的机器阅读理解方法大多基于人工特征以及传统机器学习方法进行建模.近年来，随着知识库、众包群智的发展，研究者们陆续提出了高质量的大规模数据集，为神经网络模型以及机器阅读理解的发展带来了新的契机. ...中科院软件研究所 本站小编 Free考研考试 2022-01-02深度学习在软件定义网络研究中的应用综述
摘要:数据转发与控制分离的软件定义网络（softwaredefinednetworking，简称SDN）是对传统网络架构的彻底颠覆，为网络各方面的研究引入了新的机遇和挑战.随着传统网络研究方法在SDN中遭遇瓶颈，基于深度学习的方法被引入到SDN的研究中，在实现实时智能的网络管控上成果颇丰，推动了SD ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
