Constructing formal specifications from informal requirements

The rigorous object-oriented analysis (ROOA) method provides a systematic development process which, starting from a set of informal requirements, produces an executable object-oriented analysis model. The model is expressed in LOTOS and provides a precise and unambiguous formal requirements specification of the static, dynamic and functional aspects of a problem. There is, however, a wide gap between informal requirements and a formal specification. To help bridge this gap, the authors propose that a formal and executable model which specifies behaviour in terms of what the environment expects from the system should be constructed initially. This user-centred model will give very early feedback to the requirements capture process and can be used as a step in the construction of the ROOA model. Both models are expressed in the same executable formal language and so they can be composed to verify that the ROOA model is compatible with the user-centred model and the composition executed to validate it with respect to the requirements.