For example, see
TheChemicalEngineeringCulture.
I've often seen it said that
ExtremeProgramming is not suitable for
LifeCriticalSystems, mostly because testing need to be more rigorous. In my experience, non-
ExtremeProgramming project do far less testing than
ExtremeProgramming projects. So what's the deal?
How do you know via testing that your interrupt will always be served in X period of time? How do you know via testing that in bizarre confluences of events not covered by your testing that you won't kill anyone? It's a different standard of proof.
Testing, of course, proves nothing. If something passes the
UnitTests, then that proves that it passes the
UnitTests. Nothing more.
In many applications this may be
GoodEnough, if a comprehensive
UnitTest suite is available. Testing gives a large amount of evidence (and a high degree of confidence; though never absolute certainty) that a system, once deployed, won't fail (or fails in an expected way).
For some applications, that isn't good enough. Which is why an entirely different set of design methodologies are brought to bear. In many such applications,
TuringCompleteness is abandoned altogether (no dynamic allocation, except for maybe a bounded amount on startup; no recursive functions; etc.) in order to gain provability. (You can't prove that an arbitrary Turing machine will or won't halt; that's the
HaltingProblem. You can prove, however, that a
FiniteStateMachine will/won't halt; which is why many
LifeCriticalSystems are implemented using FSMs.)
[Note: The FDA has many, many requirements for hardware and software of Class IIB and Class III medical devices. It's just too easy to kill somebody if they are hooked up to a machine that simply passes
UnitTests.
To see about 510(k) submissions, Go to
This is just one aspect of FDA approval for medical devices in the US. Peruse the FDA site to get a glimpse of the nature of FDA testing requirements.]
FDA General Principles of Software Validation - go to
Avionics software
http://en.wikipedia.org/wiki/Avionics_software
It would be nice if my
LifeCriticalSystem had
BugFreeSoftware.
Bug free isn't nearly as important as predictive; thusly the above comment about finite state machines in medical applications.
If
ProofOfCorrectness can be more complex than the code it's trying to verify, and subject to errors themselves, surely you don't rely on proofs and no testing for
LifeCriticalSystems?
Actually, there are other mechanisms (besides testing) to insure correctness. I related a couple of stories about the FaganDefectFreeProcess on that page; we proved by inspection that code which had been tested still
contained bugs, and code which passed inspection absolutely did not. That's what you need for Class IIb and above medical systems, commercial aircraft avionics, mass transportation controls, etc. -- MartySchrader