Formal Verification and Validation of Interactive Systems Specifications
Yamine Aït‐Ameur, Benoit Breholée, Patrick Girard, Laurent Guittet, Francis Jambon · Kluwer Academic Publishers eBooks · 2006
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 specifications.