关键系统是否有软件保障?[关闭]

在现实世界中,为高完整性应用程序编码通常需要跳过一系列的QA环。有时这些圈套实际上与正确使用软件有关。

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

航空工业必须遵循DO-178B,也就是ISO-9000类固醇。您必须生成大量的文档并证明它们之间的可追溯性。不过,我不知道联邦航空局是否和FDA有同样的质量保证方法。

问题是,没有人真正知道如何生产出能够实现预期效果的软件。因此,我们有一种货物崇拜的方法,在这种方法中,我们产生大量的文档,希望这能为我们的软件注入质量。事实上,质量软件通常具有清晰的需求和简单的逻辑体系结构,但这并不意味着编写“需求文档”或“体系结构文档”将改善问题。

有证据表明,对代码正确性影响最大的因素是创建它的团队。但是,您不能为团队编写法律约束。因此,相反,负责质量管理工作的人必须在流程上写下限制条件,模糊地希望这会产生类似的效果。

见 They Write The Right Stuff 有趣的是,看看他们是如何为航天飞机开发软件的。

Excerpt:

但是这个软件能做多少工作 不是什么让它与众不同。什么 使之引人注目的是 软件工作。这个软件从来没有 撞车事故。它永远不需要 重新启动。这个软件没有漏洞。 它是完美的,和人类一样完美 人类已经实现了。考虑这些 状态:最后三个版本的 程序——每42万行 每个都只有一个错误。最后11 此软件的版本总数为 17个错误。商业计划 等效复杂度为5000 错误。

是的,有一些系统是用正确性证明开发的。Praxis使用spark ada已经做了很多年了,现在我们用c和escher c验证器来做这个。这不是万能药,因为即使我们证明代码满足规范,通常也很难确定规范是否适合相关应用。

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

看看Walter Bright的这篇专栏文章,基本上认为要写出完美的软件几乎是不可能的,所以 the best thing to do is fail fast and build in redundancy.