主要观点：软件工程中常从小部件构建大系统，部分设计问题仅在系统级才明显，如 2023 年 3 月 8 日的全球中断促使设定新目标，要解决分布式系统分析挑战，需多种测试方法，文中以新消息队列服务 Courier 为例，介绍了形式化建模、轻量级模拟和混沌测试等技术。
关键信息：

• 2023 年 3 月 8 日全球中断，促使重视系统级问题。
• 分布式系统虽能提升规模和可用性，但更复杂且有新故障模式，需多种测试。
• Courier 需满足多租户、至少一次交付等要求，通过多 FoundationDB 集群和代理层实现。
• 用 TLA+形式化建模 Courier，包括定义进程、描述状态转换等，验证无消息丢失等属性。
• 用 SimPy 实施离散事件模拟，量化 Courier 在不同场景下的性能，发现并解决吞吐量振荡问题。
• 进行混沌测试，与模拟结果相似，发现潜在级联故障，便于后续混沌测试。
• 性能测试中发现 FoundationDB 热点问题，通过添加序器进程解决，更新 TLA+模型发现新情况。
• 后续需将形式化建模与实施对齐，可借助确定性模拟技术，目前应用有挑战但仍在研究。
  重要细节：
• 文中展示了 Courier 的设计图、序列图等，如初始设计图、初始和更新后的序列图等。
• 详细描述了 TLA+中对 Courier 各操作的建模，如 SendMessage、ReceiveMessage 等的代码实现和状态转换。
• 模拟中不同场景下 Courier 的吞吐量表现及与其他系统的对比图表，如乐观、悲观场景与单集群、最佳情况系统的对比。
• 混沌测试中部署 Courier 到 staging 环境诱导节点丢失的图表。
• 性能测试中 FoundationDB 热点问题及解决办法的相关图表。
• 更新 TLA+模型后出现的 NoLostMsg 属性失败的 trace 等细节。