A validation check between a design and its implementation is usually done in order to validate the correctness of the requirements for any system. It is crucial to check that the requirements are correct when the system is developed. Formal techniques are usually used for checking the correctness of the system’s requirements.

Mashkoor and Jacquot present an approach to check the correctness of a system’s requirements using formal specifications through transformation and animation. They propose a framework, called verify-transform-animate (VTA), for their approach.

The authors’ approach starts by formalizing the specification requirements of any system by grouping them into observation levels. Then, the formal specification is verified through model checking. Finally, once the formal specification is verified, the specification is transformed into a model using animation. Animation is used to demonstrate the behavior of the specification to stakeholders after its correctness is verified.

The authors demonstrate the proposed approach using case studies and successfully proving the case studies in terms of the validation of formal requirements specifications. The evaluation shows the correctness of the animated specifications. The VTA framework can be used by readers to transform the requirements of any system into animated specifications, for easy demonstrations for stakeholders.