Chapter 29

Chapter 29

Cleanroom Software Engineering

CHAPTER OVERVIEW AND COMMENTS

The late Harlan Mills (one of the true giants of the first half century of computing) suggested that software could be constructed in a way that eliminated all (or at least most) errors before delivery to a customer. He argued that proper specification, correctness proofs, and formal review mechanisms could replace haphazard testing, and as a consequence, very high quality computer software could be built. His approach, called cleanroom software engineering, is the focus of this chapter.

The cleanroom software engineering strategy introduces a radically different paradigm for software work. It emphasizes a special specification approach, formal design, correctness verification,  “statistical” testing, and certification as the set of salient activities for software engineering. The intent of this chapter is to introduce the student to each of these activities.

The chapter begins by introducing box structure specification and a more rigorous approach for representing the analysis model.  Next define refinement of the box structure specification is presented, followed by the correctness proofs that can be applied to the specification to verify that it is correct. The cleanroom approach to testing is radically different that more conventional software engineering paradigms. The culmination of this chapter is to emphasize the cleanroom testing approach.

The key concepts for students to understand are boxes, formal verification, probability distributions, and usage based testing. The mathematics and statistical background needed to read the chapter is not overwhelming. However, if you want to have your students do some cleanroom software development, you may need to do some additional teaching on program verification and statistical sampling.

Note:  Cleanroom software engineering has not been widely adopted in the industry, and for that reason, a number of reviewers for SEPA 6/e suggested that the chapter could be deleted. I disagree. Although the complete cleanroom paradigm may not be widely used, the individual elements of the approach have significant merit and provide students with insight that they may not otherwise obtain. Even if they don’t use cleanroom, your students can certainly adopt and use things like statistical use testing or proofs of correctness.

29.1  The Cleanroom Approach

This section introduces the key concepts of cleanroom software engineering and discusses its strengths and weaknesses. An outline of the basic cleanroom strategy is presented. Students will need some additional information on the use of box specifications and probability distributions before they can apply this strategy for their own projects.

29.2  Functional Specification

Functional specification using boxes is the focus of this section. It is important for students to understand the differences between black boxes (specifications), state boxes (architectural designs), and clear boxes (component designs). Even if students have weak understanding of program verification techniques, they should be able to write box specifications for their own projects using the notations shown in this section.

29.3  Cleanroom Design

If you plan to have your students verify their box specifications formally, you may need to show them some examples of the techniques used (if you did not already do so when covering Chapter 28). The key to making verification accessible to students at this level is to have them write procedural designs using only structured programming constructs in their designs. This will reduce considerably the complexity of the logic required to complete the proof. It is important for students to have a chance to consider the advantages offered by formal verification over exhaustive unit testing to try to identify defects after the fact.

29.4  Cleanroom Testing

This section provides and overview of statistical use testing and increment certification. It is important for students to understand that some type of empirical data needs to be collected to determine the probability distribution for the software usage pattern. The set of test cases created should reflect this probability distribution and then random samples of these test cases may be used as part of the testing process. Some additional review of probability and sampling may be required. Students would benefit from seeing the process of developing usage test cases for a real software product. Developing usage test cases for their own projects will be difficult, unless they have some means of acquiring projected usage pattern data. Certification is an important concept. Students should understand the differences among the certification models presented in this section as well.