Integrating SCR Requirements into Cleanroom Software Engineering

This paper describes the combination of two industrially proven methods, SCR Requirements and Cleanroom Soft ware Engineering, to form a seamless method for the for mal specification and design of real-time systems. SCR documents functional and non-functional requirements such as timing and precision using a tabular notation of mathematical functions. Cleanroom supports the develop ment of near-zero-defect software through formal methods and statistical quality control. The formalism primarily used in Cleanroom for specification and design is called Box Structure Method (BSM). We show how SCR can be integrated in BSM as a black-box-like description, and how the syntax and semantics of box structures can be extended to serve for real-time systems. Subsequently we describe how BSM's refinement and verification proce dures have to be modified according to our previous defini tions. The presentation is illustrated with a simplified example of a safety injection system for a reactor core.