algorithm - 关键系统中是否有任何软件保证？

Question

是否有系统或有开发的带有正确性证明的软件来支持它？还是所有关键系统都只是通过积极的代码审查和测试周期开发的？

Answer 1

在现实世界中，为高完整性应用程序编码通常涉及跳过一堆 QA 圈。有时，这些箍实际上与正确使用软件有关。

美国的医疗器械行业受 FDA 监管。他们发布了一系列涵盖“设计”的法规，其中包括所有软件开发。这些法规基本上是关于类固醇的 ISO 9000。你必须有一堆文件，这些文件是由审阅者编写、标记、更新审阅意见并由高级经理签署的。由于法规有法律支持，因此 FDA 希望看到这些记录未被篡改的证据，例如，在您看到测试给出的结果后写下测试的“预期结果”。因此，您要么必须拥有一个完全安全的 CM 系统，要么必须在纸上签名并注明日期（包括源代码）。FDA检查员拥有真正的执法权力；如果他们认为合适，他们可以与武装的联邦元帅一起检查您的源代码。然而他们不是软件专家：他们的工作不是判断你的代码质量，只是确保你遵守了所有的规定。

航空业必须遵循 DO-178B，这也是 ISO-9000 的类固醇。您必须制作大量文档并证明它们之间的可追溯性。我不知道 FAA 是否采用与 FDA 相同的 QA 方法。

问题在于，没有人真正知道如何生产能够完成预期工作的软件。因此，我们有一种货物崇拜的方法，我们制作大量文档，希望这将使我们的软件充满质量。质量软件通常具有明确的需求和简单的逻辑架构，这是事实，但这并不意味着编写“需求文档”或“架构文档”会改善问题。

证据表明，对代码正确性影响最大的因素是创建它的团队。但是，您不能为团队编写法律约束。因此，负责要求质量的人不得不写下对流程的限制，模糊地希望这会产生类似的效果。

Answer 2

请参阅他们编写正确的东西，以有趣地了解他们如何为航天飞机开发软件。

摘抄：

但该软件做了多少工作并不是让它引人注目的原因。它的显着之处在于该软件的运行效果。这个软件永远不会崩溃。它永远不需要重新启动。该软件没有错误。它是完美的，就像人类已经达到的那样完美。考虑一下这些统计数据：该程序的最后三个版本——每个 420,000 行长——每个都只有一个错误。该软件的最后 11 个版本共有 17 个错误。同等复杂度的商业程序会有 5,000 个错误。

Answer 3

是的，有一些系统开发了正确性证明。Praxis 多年来一直使用 SPARK Ada 来做这件事，现在我们使用 C 和 Escher C Verifier 来做这件事。它不是万能的，因为即使我们证明代码满足规范，通常也很难确定规范是否适合相关应用程序。

更广泛地采用形式证明的障碍之一是现有的航空软件标准 DO-178B 对形式技术不友好。目前正在进行的 DO-178C 重写应该可以解决这个问题。

Answer 4

查看 Walter Bright 的这篇专栏文章，他基本上认为编写完美的软件几乎是不可能的，所以最好的办法是快速失败并建立冗余。