Why Buran Had Four Computers, Not Three
12 hours ago
- 暴风雪号飞行计算机使用了四台相同的Biser-4机器，同步运行相同的程序，通过输出比较来阻止故障通道，并要求在任意两次故障后仍能生存。
- 如果只有输出比较可用，则需要四个通道：三个通道可以处理一次故障，但在第二次故障时会因1-1对峙而失败；四个通道允许顺序隔离两次故障。
- 暴风雪号的设计并非拜占庭协议（需要3f+1个节点）的实例，因为它处理的是输出投票，而不是确保潜在故障节点之间的输入一致性。
- 所有通道上的相同程序无法检测共模软件故障；历史上的案例，如STS-1、波音787发电机控制器、阿丽亚娜501和澳航72，说明了这一局限性。
- 作者创建了一个四通道投票器的Rust模型，并通过Aeneas提取流水线在Lean 4中证明了五个定理和两个推论，涵盖了无恐慌、正确屏蔽最多两次顺序故障以及成对阶段行为等属性。
- 这些证明仅适用于投票器实现，而非飞行代码；所有通道共享的飞行程序中的常见错误仍会通过投票器而未被检测到。
- 工具链（Charon、Aeneas、Lean）未通过DO-330认证，也未发现关于已完成DO-178C或ECSS认证的飞行软件Rust工具链的公开记录。