Cleanroom Software Engineering for Real-Time Systems. A Combination of the Box Structure Method and Statecharts
Cleanroom is a managerial and technical process for the development of software with ultra- high quality and certified reliability. The specification and design method of Cleanroom is the Box Structure Method (BSM), based on the usage hierarchy of data abstractions, in which each abstraction is defined in three distinct forms: black box, state box and clear box. The efficiency of a specification method depends on the tool support which is given, but until now no sufficient tool support for BSM exists. The purpose of this thesis is to define a tech nique that improves the BSM in a manner that a graphical notation can be used and tool sup port for automated consistency checks, simulation and code generation is given. This thesis defines a technique to integrate statecharts into the Box Structure Method. The technique is called Box Structure Method using Statecharts (BoSMuS). Using BoSMuS a clearer and more efficient specification of software systems is possible. Instructions are given to specify the state box (chart box) with STATEMATE`s hierarchical and concurrent statecharts. A simulation of the chart boxes at every level of specification is possible and automated consist ency checks can be performed. Further, it is defined how to derive a clear box from a BoSMuS chart box. It is described how BSM`s refinement and verification process has to be modified according to previous definitions and the modified BSM algorithm is presented. The presenta tion is illustrated with a simplified example of a bicycle computer. Finally, an evaluation of the BoSMuS technique is made by performing a case study.
Kaiserslautern, Univ., Dipl.-Arb., 1998