Stage - Auto-explication de systèmes interactifs
Un problème de qualité dans une IHM nuit à l’utilisabilité d’un logiciel. Si les choix des concepteurs ne sont pas toujours adaptés aux utilisations finales du logiciel, il a aussi été noté un défaut de qualité pour les interfaces générées automatiquement à partir de modèles. Un palliatif à ce problème est de permettre aux utilisateurs de disposer d’explications sur l’IHM pour qu’ils la comprennent mieux et qu’ils la manipulent mieux.
Nous appelons auto-explication d’une IHM sa capacité à fournir à l’utilisateur final des informations sur la justification de l’IHM (quel est son but ?), les choix de conception (pourquoi est-elle structurée dans ces espaces de travail ? quelle est l’utilité de ce bouton ? ...), son état courant (pourquoi ce menu est-il grisé ?) ainsi que l’évolution de son état (comment puis-je activer cette fonctionnalité ?). L’auto-explication propose de fournir des réponses aux questions que peut se poser l’utilisateur face à une interface.
Dans ce travail, le parti pris est de considérer comme point de départ de l’auto-explication des modèles de représentation formelle qui permettent des raisonnements de haut niveau, tels que la simulation ou la vérification de propriétés temporelles. L'objectif est de montrer la faisabilité et l’intérêt d’utiliser un modèle formel pour l’auto-explication.
Les modèles formels et les outils considérés sont ceux disponibles dans la boîte à outils CADP développée par l’équipe VASY pour la vérification de systèmes concurrents asynchrones. En particulier, on considèrera le langage LOTOS NT, dont la syntaxe se rapproche des langages de programmation usuels, permettant de décrire formellement le comportement du système à vérifier sous la forme de processus s’exécutant en parallèle, communiquant et se synchronisant. CADP fournit également des langages et des outils de génération de code, de simulation, de génération de cas de test et de vérification, qui s’appliquent aux modèles décrits en LOTOS NT.
Le travail de recherche consistera à
1) Faire un état de l’art sur les travaux existants sur l’auto-explication des IHM et sur l’utilisation des méthodes formelles en IHM.
2) Proposer des pistes concernant l’apport des modèles formels dans une démarche d’auto-explication, en s’attachant dans un premier temps aux fonctionnalités disponibles dans la boîte à outils CADP.
3) Développer un exemple illustrant cet apport.
4) Identifier les fonctionnalités inexistantes dans les outils CADP, qui pourraient être utiles, voire nécessaires, dans une démarche d’auto-explication.
Les connaissances et compétences suivantes seraient un plus :
• Modèles pour l’interaction homme-machine
• Méthodes formelles
• Algèbres de processus
• Logique temporelle
Ce travail s'effectuera en collaboration avec l'équipe VASY du LIG, en particulier avec Frédéric Lang qui en assurera le co-encadrement.