Behavioral Refinement

Behavioral refinement gives a mathematical foundation to two essential system development activities, namely, stepwise requirements engineering and incremental system development. In the first case, the requirements specification is developed by adding requirements step by step in the order they are identified and formalized. In the second case, the requirements are captured, formalized, and implemented in a stepwise incremental manner. In both cases, each step typically strengthens the constraints on the system to be developed. This strengthening reduces underspecification and imposes more and more requirements. As a special case we may also refine the way the specification is formulated without changing its external behavior, for example, by introducing a glass-box view.