Formal Verification and Validation of Interactive Systems Specifications - From Informal Specifications to Formal Validation.
Yamine Aït Ameur, Benoit Breholée, Patrick Girard, Laurent Guittet, Francis Jambon · 2004
This paper proposes a development process for interactive systems based both on verification and validation methods. Our approach is formal and use at first the B Method. We show in this paper how formal B specifications can be derived from informal requirements in the informal notation UAN. Then, these B specifications are validated using the data oriented specification language EXPRESS. Several scenarios can be tested against these EXPRESS