Coding for high integrity applications, in the real world, generally involves jumping through a bunch of QA hoops. Sometimes these hoops actually have something to do with getting the software right.
The medical device industry in the USA is regulated by the FDA. They publish a bunch of regulations covering "design", which includes all the software development. These regulations are basically ISO 9000 on steroids. You have to have a bunch of documents which are written, marked up by reviewers, updated with the review comments and signed off by a senior manager. Because the regulations are backed by law the FDA want to see evidence that these records have not been tampered with, for instance by writing the "expected result" of a test after you saw what result the test gave. So you either have to have a locked down totally secure CM system, or it all has to be signed and dated on paper (including the source code). The FDA inspectors have real law enforcement powers; if they see fit they can inspect your source code with an armed federal marshal. However they are not software specialists: their job is not to judge the quality of your code, just to make sure you have complied with all the regulations.
The aviation industry has to follow DO-178B, which is also ISO-9000 on steroids. You have to produce lots of documents and demonstrate traceability between them. I don't know if the FAA has the same approach to QA as the FDA though.
The problem is that nobody really knows how to produce software that does what it is supposed to. So instead we have a kind of cargo cult approach where we produce lots of documentation in the hope that this will imbue our software with quality. Its true that quality software generally has clear requirements and a simple logical architecture, but that doesn't mean that writing a "Requirements Document" or an "Architecture Document" will improve matters.
The evidence suggests that factor with the biggest impact on code correctness is the team that created it. However you can't write a legal constraint on a team. So instead the people with the job of mandating quality have to write constraints on process instead, in the vague hope that this will have a similar effect.
See They Write The Right Stuff for an interesting look at how they develop software for the Space Shuttle.
Excerpt:
But how much work the software does is not what makes it remarkable. What makes it remarkable is how well the software works. This software never crashes. It never needs to be re-booted. This software is bug-free. It is perfect, as perfect as human beings have achieved. Consider these stats : the last three versions of the program -- each 420,000 lines long-had just one error each. The last 11 versions of this software had a total of 17 errors. Commercial programs of equivalent complexity would have 5,000 errors.
Yes, there are systems out there developed with proof of correctness. Praxis have been doing this for years using SPARK Ada, and now we're doing it with C and Escher C Verifier. It's not a panacea, because even though we prove that the code satisfies the specification, it's usually difficult to be certain that the specification is appropriate for the application concerned.
One of the barriers to more widespread adoption of formal proof is that the existing aviation software standard DO-178B is not friendly to formal techniques. The DO-178C rewrite currently in progress is supposed to fix that.
发布评论
评论（4）
在现实世界中，高完整性应用程序的编码通常涉及跳过一堆 QA 环节。 有时，这些障碍实际上与软件的正确性有关。
美国的医疗器械行业受 FDA 监管。 他们发布了一系列涵盖“设计”的法规，其中包括所有软件开发。 这些法规基本上是 ISO 9000 的强化版。 你必须有一堆由审阅者编写、标记、用审阅意见更新并由高级经理签署的文件。 由于这些法规受到法律支持，FDA 希望看到这些记录未被篡改的证据，例如在看到测试给出的结果后写下测试的“预期结果”。 因此，您要么必须拥有一个锁定的完全安全的 CM 系统，要么必须在纸上签名并注明日期（包括源代码）。 FDA检查员拥有真正的执法权； 如果他们认为合适，他们可以与武装联邦元帅一起检查您的源代码。 然而，他们不是软件专家：他们的工作不是判断您的代码质量，只是确保您遵守所有规定。
航空业必须遵循 DO-178B，它也是 ISO-9000 的强化版。 您必须生成大量文档并证明它们之间的可追溯性。 我不知道 FAA 的质量保证方法是否与 FDA 相同。
问题是没有人真正知道如何开发能够实现预期功能的软件。 因此，我们采用了一种货物狂热的方法，我们制作大量文档，希望这能够提高我们的软件的质量。 确实，高质量的软件通常具有明确的需求和简单的逻辑架构，但这并不意味着编写“需求文档”或“架构文档”就能改善问题。
有证据表明，对代码正确性影响最大的因素是创建代码的团队。 但是你不能对团队制定法律约束。 因此，负责质量管理工作的人员必须对流程编写约束条件，并模糊地希望这会产生类似的效果。
Coding for high integrity applications, in the real world, generally involves jumping through a bunch of QA hoops. Sometimes these hoops actually have something to do with getting the software right.
The medical device industry in the USA is regulated by the FDA. They publish a bunch of regulations covering "design", which includes all the software development. These regulations are basically ISO 9000 on steroids. You have to have a bunch of documents which are written, marked up by reviewers, updated with the review comments and signed off by a senior manager. Because the regulations are backed by law the FDA want to see evidence that these records have not been tampered with, for instance by writing the "expected result" of a test after you saw what result the test gave. So you either have to have a locked down totally secure CM system, or it all has to be signed and dated on paper (including the source code). The FDA inspectors have real law enforcement powers; if they see fit they can inspect your source code with an armed federal marshal. However they are not software specialists: their job is not to judge the quality of your code, just to make sure you have complied with all the regulations.
The aviation industry has to follow DO-178B, which is also ISO-9000 on steroids. You have to produce lots of documents and demonstrate traceability between them. I don't know if the FAA has the same approach to QA as the FDA though.
The problem is that nobody really knows how to produce software that does what it is supposed to. So instead we have a kind of cargo cult approach where we produce lots of documentation in the hope that this will imbue our software with quality. Its true that quality software generally has clear requirements and a simple logical architecture, but that doesn't mean that writing a "Requirements Document" or an "Architecture Document" will improve matters.
The evidence suggests that factor with the biggest impact on code correctness is the team that created it. However you can't write a legal constraint on a team. So instead the people with the job of mandating quality have to write constraints on process instead, in the vague hope that this will have a similar effect.
请参阅他们写出正确的内容了解有趣的内容看看他们如何为航天飞机开发软件。
摘抄：
See They Write The Right Stuff for an interesting look at how they develop software for the Space Shuttle.
Excerpt:
查看 Walter Bright 的这篇专栏，基本上认为编写完美的软件几乎是不可能的，因此 最好的办法就是快速失败并建立冗余。
Check out this column by Walter Bright, basically arguing that it's virtually impossible to write perfect software, so the best thing to do is fail fast and build in redundancy.
是的，有些系统已经开发出来并具有正确性证明。 Praxis 多年来一直使用 SPARK Ada 来做到这一点，现在我们正在使用 C 和 Escher C Verifier 来做到这一点。 它不是万能的，因为即使我们证明代码满足规范，通常也很难确定规范是否适合相关应用程序。
更广泛采用形式化证明的障碍之一是现有的航空软件标准 DO-178B 对形式化技术不友好。 目前正在进行的 DO-178C 重写应该可以解决这个问题。
Yes, there are systems out there developed with proof of correctness. Praxis have been doing this for years using SPARK Ada, and now we're doing it with C and Escher C Verifier. It's not a panacea, because even though we prove that the code satisfies the specification, it's usually difficult to be certain that the specification is appropriate for the application concerned.
One of the barriers to more widespread adoption of formal proof is that the existing aviation software standard DO-178B is not friendly to formal techniques. The DO-178C rewrite currently in progress is supposed to fix that.