Distributed systems have become increasingly prevalent in the software industry. Due to their intrinsic complexity, much research has focused on the verification of their behaviour. An active research line is around behaviour models that capture these protocols - e.g., session types, or typestates - allowing their static verification. Correctly designing distributed protocols is not trivial. Their communication behaviour is typically implicitly defined via asynchronous message handlers, making errors harder to detect until execution. While typestates can ease the design process by explicitly defining correct sequences of operations, they struggle in two ways: they lack the expressiveness to define quantitative constraints that govern distributed protocols (i.e., number of acknowledgements for a quorum); and they assume strict sequencing of operations, failing to capture concurrent input/output actions in a state, typical of the distributed setting. Furthermore, runtime network failures cannot be statically verified. We present a probabilistic runtime solution extending typestates with: (i) an internal mutable state for the expression of quantitative constraints; (ii) mixed sessions to represent concurrent input and output actions; (iii) expected ratios for the number of actions in a state, with monitoring semantics to detect deviations from an expected behaviour at runtime. We demonstrate the suitability of our solution with two examples that motivated our approach: an acknowledgement protocol with a participant that sends several messages while waiting for a response, effectively modelling input and output operations in a state; and a voting protocol whose participants try to achieve consensus on a single bit using a quorum, thus, requiring an internal mutable state, while respecting a pre-defined distribution for the volume of exchanged messages.

翻译：分布式系统在软件行业中日益普遍。由于其固有的复杂性，大量研究聚焦于其行为的验证。一个活跃的研究方向是围绕捕获这些协议（例如，会话类型或类型状态）的行为模型，从而允许对其进行静态验证。正确设计分布式协议并非易事。其通信行为通常通过异步消息处理器隐式定义，使得错误在运行时才更易被发现。虽然类型状态可以通过显式定义正确的操作序列来简化设计过程，但它们在两个方面存在不足：缺乏定义支配分布式协议的量化约束（例如，法定人数的确认数）的表达能力；并且假设操作严格顺序执行，无法捕获分布式环境中典型的并发输入/输出动作。此外，运行时的网络故障无法静态验证。我们提出了一种概率运行时解决方案，扩展了类型状态，具体包括：(i) 用于表达量化约束的内部可变状态；(ii) 表示并发输入和输出动作的混合会话；(iii) 状态中动作数的预期比率，并配备监控语义以在运行时检测与预期行为的偏差。我们通过两个激发我们方法动机的示例来证明我们解决方案的适用性：一个确认协议，其中参与者在等待响应时发送多条消息，从而有效模拟了状态中的输入和输出操作；以及一个投票协议，其参与者试图使用法定人数在单个比特上达成共识，因此需要内部可变状态，同时遵守预定义的交换消息量分布。