Formalizing informal specifications requires traceability. System descriptions are rarely fully formalized right from the start. Assumptions on the environment and requirements of the system are often specified semi-formally or as a mix of formal and informal specifications.

The authors start with a categorization of assumptions and requirements proposed for the WRSPM model and extend it to handle a mix of formal and informal parts. They propose a process to elaborate and validate formal requirements from an informal specification. The key feature of the process is traceability, showing how formal and informal parts relate. Traceability enables validation and change management. This approach is illustrated by a toy example using Event-B as the underlying formal method. A tool chain based on Rodin, ProB, and ProR is proposed for bigger projects.

The paper is accessible to a general audience and does a good job explaining the formal parts. However, a practitioner likely would have preferred the example to be more detailed and worked out, showing how the approach could actually be applied in practice.