Cleanroom Software Engineering

Our pervasive dependence on software in every sphere of modern life amplifies the consequences of errors and security flaws. Software systems that control critical infrastructure assets, from transportation and energy to finance and government, absolutely must function reliably in all circumstances. Nowhere is rigorous software engineering more important than in the development and evolution of these systems.

testing1

The objective of Cleanroom Software Engineering (CSE) is to develop and certify high reliability, high-security software. The Cleanroom process creates software that approaches zero defects prior to first execution, a level of quality that permits testing to be repurposed from bug finding to scientific certification of software fitness for use. These properties of near-zero defects and scientific certification are hallmarks of Cleanroom. This mathematics-based engineering process stands in sharp contrast to the informal and ad hoc methods employed in much of software development.

CSE is organized around six integrated activities:

Precise Specification: Rigorous methods such as box structures and sequenced-based specification are employed to permit hierarchical definition and validation of required system behavior prior to design.

Stepwise Design: Specifications are transformed into designs and implementations in a stepwise process guided by the structure theorem that localizes functionality for verification at every step.

Computational Verification: The R&K Hyperion System for software behavior computation can be employed to validate the programmed functionality of compiled binaries.

Human Verification: Computed verification is augmented by special team reviews that apply the correctness theorem to every structure in designs and implementations.

Statistical Testing: A testing process based on a statistical sampling of usage models permits scientifically valid projections of software quality in actual field use.

Incremental Development: Stepwise management based on the functional equivalence of specifications and their implementations permits increments to accumulate into the final system and shows earned value.

testing2
testing2

CSE is organized around six integrated activities:

Precise Specification: Rigorous methods such as box structures and sequenced-based specification are employed to permit hierarchical definition and validation of required system behavior prior to design.

Stepwise Design: Specifications are transformed into designs and implementations in a stepwise process guided by the structure theorem that localizes functionality for verification at every step.

Computational Verification: The R&K Hyperion System for software behavior computation can be employed to validate the programmed functionality of compiled binaries.

Human Verification: Computed verification is augmented by special team reviews that apply the correctness theorem to every structure in designs and implementations.

Statistical Testing: A testing process based on a statistical sampling of usage models permits scientifically valid projections of software quality in actual field use.

Incremental Development: Stepwise management based on the functional equivalence of specifications and their implementations permits increments to accumulate into the final system and shows earned value.