Are there any software guarantees in critical systems?

Question

Are there systems or is there software out there that is developed with a proof of correctness to back it up? Or are all critical systems developed merely with an aggressive code review and test cycle?

Answer 1

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.

Answer 2

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.

Answer 3

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.