CRDT协议的TLA+描述与验证

来源 :软件学报 | 被引量 : 0次 | 上传用户:yorehi
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧,不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言,构建了一个可复用的CRDT协议描述与验证框架,包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型,实现了多种类型的通信网络.协议
其他文献
为探讨交锁髓内钉内固定在四肢骨折中的应用效果,选择应用交锁髓内钉内固定治疗股骨、胫腓骨、肱骨骨折89例,结果70例骨折完全愈合并已取出内固定,14例已经有明显骨痂生长,4
为研究长江口耙吸船疏通航道工作时对长江口深水航道通航情况的影响,开展实船试验工作。确保有效开展实船试验,分析耙吸作业船组在长江口的可航水域特征,根据风流压差角、横
柘皋位于庐州西南,巢县(今巢湖境内)西北,汉代即在此置县.由于地理位置优越,使得其自古为兵家争战之地.绍兴十一年(1141年)二月,南宋与金朝在此发生激战,并且大败金军.战争对宋金
元代诗人喜欢写咏物诗,所咏之物从千奇百怪到喜闻乐见,萨都剌是元代最主要的咏物诗人.他的咏物诗代表着元代咏物诗的最高成绩。作者借所咏物或咏叹世事变迁,或表达自己的反战情绪
为提高绞吸挖泥船的生产效率,采用自动化手段代替传统的人工操作,研究疏浚作业过程中泥浆浓度的控制方法。针对泥浆浓度过程建模困难和泥浆浓度控制系统的不确定性和时滞性等
由于我国对学生思想政治教育研究起步较晚,尽管当前取得不小的成绩,但无论在理论上还是实践上都存在着诸多的问题,亟需我们进行深刻地反思。除此之外,学生思想政治教育是一个动态
聚乙烯管在燃气输配系统工程中得到了广泛的应用,聚乙烯管与钢管相比,除了具有投资省、运输便利、重量轻、施工方便等优点外,更重要的是聚乙烯管具有的一些重要性能是钢管无
"人肉搜索"自诞生以来,在社会上已是风生水起。它帮人们寻亲找友、助社会网络反腐、倡导社会道德;但同时,由于使用不当,它也侵犯了人们的隐私、伤害了无辜,甚至成了杀人的帮凶
针对海上水面自主船舶(Maritime Autonomous Surface Ship,MASS)在港内航行或自动靠离泊过程中面临的近距离典型障碍物自动检测和识别的问题,提出一种运用三维激光雷达(Light
目的分析第八师2010-2015年恶性肿瘤的疾病负担,为该地肿瘤防控提供依据。方法通过计算潜在减寿年(potential years of life lost,PYLL)、早死所致寿命损失年(years of life