Formal Verification and Validation of Interactive Systems Specifications

: 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. Key words: B Method, EXPRESS, UAN, interaction properties, verification, validation, formal specification of interactive systems.

• Type: Conference
• Year: 2004
• Where: IFIP13
• Authors: Yamine Aït Ameur, Benoit Breholée, Patrick Girard, Laurent Guittet, Francis Jambon
• Keywords: Artificial Intelligence, IFIP13 2004, Interactive Systems, Specification, Specification Language Express