CleanroomSoftwareEngineering:  IBM developed technology for writing bug-free software.

The methodology (as I understand it) relies on extensive reviewing and checking of code. To the extent that code will compile correctly, and is only compiled at the end of the development process. It's then extensively tested, using some formal coverage techniques.

The space shuttle flight software was created using a variant: contains ~500Klocs and has had something of the order of 17 bugs reported. It's also amongst the most expensive software mankind's ever written... the team has an annual budget of $35 million. I suspect, but don't know, that CleanRoom is an offshoot of having developed the shuttle software.

Any other examples?

-- KatieLucas

----

As I understand it, CleanRoom is effectively the AntiProcess of techniques like ExtremeProgramming as it relies on BigDesignUpFront backed up by FormalMethods for verifying the design/implementation, in favour of UnitTest''''''s or TestDrivenDevelopment by change-driven processes.

The emphasis in CleanRoom is IIRC to focus on developing design based on the use of functions and StructuredProgramming principles that at least ensure tractability in formulating a proof for that design. The design is sufficiently detailed and straightforward to be directly proved correct (ideally via FormalMethods or failing that by extensive and rigorous peer review) that the mapping onto code is not prone to subjective translation error by the programmer. Hence the theory goes: the design is proved correct, the implementation is therefore correct and no faults are present in the software.

Advantages of this process are the obvious extreme low tolerance for errors and the scalability of the process itself which make it very useful for large, complex yet safety-critical or real-time systems like (as pointed out above) astronautics or aeronautics.

Disadvantages are the large costs involved, rigour (and effort) required and the fact that the process is oriented around "one shot" programming projects, i.e. building a system end-to-end - the process is not naturally iterative but can be adapted to be so.

Please feel free to edit the above if I've got anything wrong, I'm a little rusty on this. 

''The thing that is innovative about this technique is that the FormalSpecification is not a separate artifact as in, for example, Z. The formal proofs are embedded in the implementation as comments. As far as I know it is still the choice method for developing medical and embedded applications.''

See CleanRoomSoftwareEngineeringIsNotDead
----
CategoryMethodology