Quality, cleanroom and formal methods

We have proposed a new approach to software quality combining cleanroom methodologies and formal methods. Cleanroom emphasizes defect prevention rather than defect removal. Formal methods use mathematical and logical formalizations to find defects early in the software development lifecycle. These two methods have been used separately to improve software quality since the 1980’s. The combination of the two methods may provide further quality improvements through reduced software defects. This result, in turn, may reduce development costs, improve time to market, and increase overall product excellence. Defects in computer software are costly. Their detection is usually postponed to the test phase, and their removal is also a very time consuming and expensive task. Cleanroom software engineering is a methodology which relies on preventing the defects, rather than removing them. It is based on incremental development and it emphasizes the development phase. An enhancement to this methodology is presented in this paper, which combines formal methods and cleanroom. The efficiency of the new model rests on an appropriate logical representation, to write the specification of the intended system. In the new model, design plans are formally verified before any implementation is done. The advantages of finding defects in the early stages are decreased cost and increased quality. Results show that, by using formal methods, a higher quality will be achieved and the software project can also benefit from the existing mechanized tools of these two techniques