JIPS : Vol. 1 (2010), Num. 1, Art. 3

Vérification et validation formelles de systèmes interactifs fondées sur la preuve : application aux systèmes multi-modaux
Yamine Ait-Ameur, Idir Ait-Sadoune, Mickael Baron & Jean-Marc Mota

Résumé : Cet article s'intéresse à la validation et à la vérification formelles d'IHM Multi-Modales (IHM3). Il décrit une partie des résultats obtenus dans le cadre du projet RNRT VERBATIM, dont l'objet est la VERification Biformelle et Automatisation du Test des Interfaces Multimodales. Ce projet s'intéresse, entre autres, à la mise en {\oe}uvre d'une technique formelle : la méthode B événementiel. Cette technique fondée sur la preuve ne souffre donc pas du problème d'explosion du nombre d'états rencontré généralement par les techniques de vérification sur modèles. Nous discutons les apports de cette technique pour la conception d'IHM3, en particulier, sa capacité à exprimer et à vérifier des propriétés de la famille CARE. Notre approche utilise des notations et techniques semi-formelles issues du domaine des IHM et propose de les formaliser. Enfin, nous appliquons notre approche sur une étude de cas appelé "Pages Jaunes CLIPS".

Mots clés : IHM multi-modales, technique formelle fondée sur la preuve, vérification, validation, propriétés CARE, modèle de tâches.

Abstract: This paper focuses on the formal validation and verification of multi-modal human computer interfaces. It describes part of the obtained results of the French RNRT VERBATIM project whose purpose is the Multimodal Interfaces BIformal Verification and Test Automation. This project focuses on the application of a formal technique, namely the event B method. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. We outline the capability of this technique to support the design of multi-modal human computer interfaces, in particular, the capability to support the expression and the verification of properties issued from the CARE family. The proposed approach uses notations and semi-formal techniques issued from the HCI design area. We apply our approach on a case study called "CLIPS Yellow Pages".

Key words: Multi-modal HCI, proof based technique, verification, validation, CARE properties, task model.

BibTeX:

@article{v1_n1_a3,
author = "Yamine Ait-Ameur and Idir Ait-Sadoune and Mickael Baron and Jean-Marc Mota",
title = "Vérification et validation formelles de systèmes interactifs fondées sur la preuve : application aux systèmes multi-modaux",
journal = "Journal d'Interaction Personne-Système", 
publisher = "AFIHM",
volume = 1, number = 1, note = "Article 3",
year = 2010, month = sep,
pages = "1-30",
url = "http://jips.gforge.inria.fr/articles/1/1/3-aitameur.html"
}

Les articles de JIPS sont publiés sous licence Creative Commons Paternité 2.0 Générique