VDM for Requirements Engineering

Requirements engineering is normally split into the following activities:

1. Elicitation
2. Analysis
3. Specification
4. Modelling
5. Validation
6. Management

VDM can be helpful in all of them:

Elicitation is not a well structured process itself, however VDM (or any other detailed) model can uncover very specific cases to clarify that otherwise may be unnoticed till late stages of testing.

Analysis is done in the course of creation of a precise mathematical model to the software to build.

Specification is what VDM was actually created for!

VDM-SL specification becomes an executable model in the Overture Tool. It can be further embedded into a prototype, e.g. a GUI based Jython application.

Validation of internal correctness is natural part of the modelling and specification. In addition, the executable model with an extended prototype as needed can serve as the basis for runnable and clickable validation with end users.

Surprisingly enough, being mathematically precise VDM method is an iterative one, or rather based on refinement. Thus in terms of requirements management, VDM accommodates for creation and maintenance of a series of more and more detailed (refined) models that suits well both linear and iterative software development lifecycles.