TLA+相关论文
Collaborative text editing systems allow multiple users to concurrently edit the same document, which can be modeled by ......
ZooKeeper Atomic Broadcast (Zab) is an atomic broadcast protocol specially designed for ZooKeeper, which supports additi......
生产者与消费者系统（PCS）是一个经典的进程同步问题，Hocine等学者运用抽象状态机（ASMs）对该问题进行了时序规约。文中主要使用TLA语言对......
行为时序逻辑（TLA）是LeslieLamport于20世纪90年代提出的一种新的逻辑，运用这种逻辑对软件或协议系统进行建模，在一定程度上减少了由于......
根据停止等待ARQ协议的算法,用基于TLA的系统描述语言TLA+对ARQ协议进行建模,用TLC验证了ARQ协议应该满足的两条基本属性。根据ARQ......
PaxosStore是腾讯开发的高可用分布式存储系统,现已用于全面支持微信核心业务.PaxosStore实现了分布式共识协议Paxos的一种变体,称......
无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证......
分布式系统在提供强大服务能力的同时也面临着可靠性、安全性和复杂性等挑战。因资源分配与需求产生冲突而产生的死锁,在分布式系......
BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序......
