Stage - Vérification de systèmes interactifs
Une particularité du domaine des applications interactives est l'hétérogénéité des cultures et des notations entre l'usager ou ses représentants (centrés sur l'interaction) et les réalisateurs des systèmes. Ceci rend difficile de vérifier que les besoins exprimés par les premiers ont bien été pris en compte par les seconds. L’utilisation de notations formelles et des méthodes de vérification associées apporte de la rigueur dans la validation mais est loin des habitudes des concepteurs d’interfaces homme-machine. Certaines notations utilisées par ces derniers ne sont pas assez précises pour servir de support à une vérification formelle. C’est le cas, en particulier, des arbres de tâches, modèle clé en interaction homme-machine : un arbre de tâches est une spécification semi-formelle de l’enchaînement des services offerts par le système et censée refléter les objectifs de l’utilisateur.
Dans ce travail, le parti pris est de considérer comme point de départ les modèles de représentation de l’interaction pour générer des modèles formels adéquats à la vérification. L'objectif de la vérification est de s'assurer du respect de propriétés d’utilisabilité, essentielles pour le domaine d’application visé. Par exemple, on veut vérifier qu’un achat sur un site marchand s’effectue bien en moins de trois clicks.
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. On s’intéresse plus particulièrement (mais non-exclusivement) aux langages suivants :
– Le langage LOTOS NT permet de décrire formellement, dans une syntaxe qui se rapproche des langages de programmation usuels, le comportement du système à vérifier sous la forme de processus s’exécutant en parallèle, communiquant et se synchronisant.
– Le langage MCL permet de décrire des propriétés concernant le système modélisé formellement. MCL possède la puissance expressive de la logique temporelle, étendue avec des variables typées et des expressions permettant d’exprimer des prédicats sur les données contenues dans le modèle.
Le travail de recherche consistera à :
1) Faire un état de l’art sur les travaux existants pour la validation et la vérification d’IHM.
2) Proposer des règles de transformations des modèles IHM vers le langage LOTOS NT, qui permet de mettre en œuvre les activités de vérifications.
3) Identifier les types de propriétés d’IHM qui peuvent être vérifiées à l’aide des outils CADP, notamment celles qui peuvent être codées dans le langage MCL.
4) Formaliser quelques propriétés d’utilisabilité et les vérifier à l’aide des outils CADP.
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.