Pioneered at IBM, Cleanroom has grown up from a good academic idea to a successful practice. (The book highlights several military and business projects that have succeeded using Cleanroom.) By decomposing a problem into "black boxes" of mathematical functions and then statistically verifying that all possible inputs to these functions are processed correctly, Cleanroom can guarantee the correctness of software before it ships.
The book looks at the incremental approach to software design favored by Cleanroom, in which functions are verified independently. A case study for an embedded security alarm device is presented. Subsequent sections examine the statistical foundations of Cleanroom. (Though not all inputs can be tested, a piece of software can nevertheless be verified statistically.) A second case study explores a Java program that controls a communications satellite, which shows the whole Cleanroom approach--from initial design and coding to Cleanroom certification that proves its correctness (along with plenty of tables showing test data).
The Y2K problem proves once and for all that software doesn't always work correctly with every input. Cleanroom techniques, though not yet in the business mainstream, would seem to offer a new level of software reliability. Geared to the academic reader, Cleanroom Software Engineering shows the strengths of this technique for designing the mission-critical software of the future. --Richard Dragan