验证标记状态转移与消息生成系统：一种用于建模故障分布式系统的理论

对带有故障的分布式系统进行建模与形式化推理是一项具有挑战性的任务。为解决此问题，我们提出了验证标记状态转移与消息生成系统（VLSMs）理论。VLSMs 理论提供了一种通用方法，用于描述和验证其执行受故障影响的分布式协议的性质，支持一种构造即正确的系统开发方法学。我们研究的核心在于 equivocation（歧义行为），这是一种故障行为模式，我们对其进行了形式化建模与推理，并进一步展示了如何根据系统组件本地可能可用的持久证据来检测它。歧义组件表现出与单轨迹系统执行不一致的行为，同时仅通过发送和接收有效消息与其他组件交互。若系统的组件的有效性约束能够验证其接收到的消息可由系统生成，则称其为该系统的验证器（validator）。我们的主要结果表明，对于由验证器组成的系统，拜占庭组件对诚实验证器所能产生的影响，与歧义组件对非歧义验证器所能产生的影响完全一致。因此，对于可能包含故障验证器的分布式系统，以歧义组件替换拜占庭组件在解析上并无实质性后果，并构成了拜占庭容错分析的一种可靠替代基础的基石。本文中的所有结果与示例均已在 Coq 证明助手中形式化并检验。