Thèmes de recherche

Modélisation et vérification des IHM multimodales.

L’étude des interactions entre l’homme et la machine est pluridisciplinaire. Elle recouvre des domaines différents tels que la psychologie, l’ergonomie et l’informatique. Les progrès réalisés par la technologie ont ouvert la voie à l’apparition de nouveaux types d’interfaces tels que les interfaces homme-machine (IHM) de type WIMP (Windows, Icônes, Menus, Pointing devices) ou les IHM multimodales. Cette diversité et ces progrès ont conduit à une complexité dans la conception et la mise en œuvre des IHM. Dans les applications actuelles, le code consacré à l’interface est de plus en plus important et a pour conséquence une augmentation du risque d’erreur lors de la conception. Le recours à des modèles de conception et à des notations de description des IHM devient indispensable pour maîtriser cette complexité. Dans le but d’améliorer la flexibilité et l’utilisabilité des IHM, de nombreux travaux se sont intéressés à ce domaine. Toutefois leur application aux IHM multimodales reste rare.

L’utilisabilité des IHM multimodales en entrée. L’étude de l’utilisabilité des IHM multimodales implique la prise en considération de nouvelles notions absentes dans les IHM classiques. Parmi les propriétés propres aux IHM multimodales on trouve les propriétés CARE (Concurrence, Assignation, Redondance et Equivalence) que le système doit assurer. Reste aussi que dans la plupart des travaux, les besoins de l’utilisateur sont négligés dans la phase de conception. Nos travaux visent à augmenter la part de l’utilisateur dans le processus de développement d’une IHM. La plupart des modèles de description de tâches utilisateurs existants sont informels ou semi-formels.  Dans ce contexte, nous avons proposé une approche de modélisation et de vérification des IHM multimodales basée sur la preuve pour l’établissement des propriétés et le raffinement pour la structuration du développement. La méthode B Evénementiel est utilisée. Une méthodologie de conception basée sur quatre scénarios de développement utilisant le raffinement a été définie. Notre approche assure l’utilisabilité de l’IHM à travers la prise en compte des propriétés CARE et des tâches utilisateur exprimées à l’aide du modèle de tâche CTT. Ce dernier reste un élément moteur dans notre approche.

Restitution de l’information et allocation des modalités et des médias dans les IHM multimodales en sortie. Les interfaces multimodales en sortie permettent au système de restituer l’information à l’utilisateur en utilisant plusieurs médias et modalités dans le but de véhiculer les informations élémentaires résultantes de la décomposition de l’information produite par le noyau fonctionnel.  Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel générique pour la conception des interfaces multimodales en sortie. Le modèle proposé se décompose en deux sous-modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des paires modalité-média pour chaque information élémentaire. Une mise en œuvre des deux sous-modèles est réalisée en utilisant la méthode B Événementiel.

Modélisation et vérification de la composition de services.

La description d’architectures de systèmes et de leurs fonctionnalités au travers des services qu’elles fournissent est devenue courante dans le cas des systèmes communicants en télécommunications, en avionique, sur le Web ou dans les applications interactives. Les architectures orientées services (SOA) constituent une réponse aux problématiques que rencontrent les développeurs en termes de description, de réutilisabilité, d’interopérabilité et de réduction de couplage entre les différents systèmes (services) qui implémentent des fonctionnalités en général issues d’applications complexes, en cachant les détails d’implantation. La description de systèmes basés sur les services utilise essentiellement des formalismes graphiques ou textuels basés sur des standards. Ces standards sont, dans la plupart des cas, des textes informels ou semi-formels et leur sémantique est souvent décrite en langue naturelle. Par conséquent, cette description souffre d’ambiguïté dans l’interprétation des constructions du langage et de leur composition du fait de l’absence de sémantique formelle non ambiguë.

Dans nos travaux, nous nous sommes intéressés au cas des architectures orientées services basées sur les services Web. Un des apports principaux de ces architectures est la possibilité de composer des services Web préexistants et indépendants pour construire de nouveaux services Web avec de nouvelles fonctionnalités. Divers formalismes et langages sont utilisés pour décrire une composition de services Web ou un Workflow de services Web. Bien que certains de ces langages soient considérés comme des standards, l’absence de sémantique formelle et la possibilité d’interprétations ambiguës des documents décrivant ces standards, constituent un frein à leur utilisation et à leur généralisation, et compromettent l’interopérabilité. De plus, ces langages n’offrent aucune possibilité pour décrire des exigences que le service doit assurer, et les outils associés ne permettent pas de garantir à priori que les services Web composés obtenus se comportent conformément à des exigences. Cette étape de validation est repoussée à la phase de déploiement du service. Enfin, ils n’offrent pas de méthodologie de conception de telles compositions et/ou décompositions. Notre travail est une contribution à la formalisation de la sémantique de ces langages en vue d’établir des propriétés des services décrits. Il préconise l’utilisation de méthodes formelles.

Pour répondre à la problématique de modélisation et de vérification formelles de compositions de services, une approche basée sur la méthode B Événementiel a été proposée. Le cas de compositions de services Web décrites par une orchestration de services (le standard BPEL) a été étudié. Les contributions de notre travail se résument aux points suivants.

• une modélisation B Evénementiel des opérateurs de composition d’une algèbre de processus en se basant sur le raffinement et l’utilisation d’un variant lexicographique explicite,
• une interprétation formelle basée sur la méthode B Evénementiel du standard BPEL permettant de formaliser les parties statique et dynamique de ce langage en gardant un lien un-à-un entre BPEL et B Evénementiel pour des besoins de traçabilité,
• une méthodologie de conception basée sur l’opérateur de décomposition de BPEL et l’opération du raffinement de la méthode B Evénementiel permettant de guider le concepteur dans son processus de modélisation et de vérification d’un processus BPEL,
• une formalisation et vérification de propriétés fonctionnelles et comportementales de services Web composés,
• une implémentation de l’approche proposée dans un outil nommé BPEL2B permettant de générer automatiquement des modèles B Evénementiel à partir d’une description BPEL d’un service composé,
• et une application de l’approche proposée sur la cas de la composition de services Web transactionnels en définissant un scénario d’utilisation permettant d’améliorer la qualité du service Web composé et de prendre en compte les propriétés transactionnelles de ce type de services en s’appuyant sur la méthode B Evénementiel.

Animation de modèles B et B-Evénementiel.

Les développements formels de programmes ou de systèmes fondés sur le raffinement et la preuve consistent à définir une succession de modèles M_i, où M_i+1 est un raffinement de M_i. Ces modèles introduisent de proche en proche les éléments décrivant le système à concevoir à partir des exigences exprimées dans le cahier des charges. Des propriétés correspondant à des exigences, exprimées par des pré-conditions, post-conditions, des invariants, etc. sont prouvées et maintenues durant ce processus de développement. Par ailleurs, la correction du raffinement est assurée par un invariant de collage qui préserve les propriétés établies dans le modèle abstrait. Pour garantir la correction de tels développements, un ensemble d’obligations de preuve sont associées à chaque opération (préservation de l’invariant, correction du raffinement, etc.). La preuve de ces obligations de preuve est réalisée de façon automatique ou bien semi-automatique en interaction avec l’utilisateur.

La méthode B, en particulier la méthode B événementiel que nous utilisons pour nos travaux, permet de supporter de tels développements fondés sur la preuve. Cependant, l’activité de développement par la preuve ne supporte pas toutes les activités de développement et en particulier pour la validation des exigences. Dans ce type de développement, les propriétés, exprimant ces exigences, sont prouvées. C’est le moyen offert pour la validation. Nous qualifions cette validation de validation par la preuve. Il n’y a pas de moyen d’animer ou de tester les modèles obtenus.  La possibilité d’animer et de tester des modèles, en particulier les modèles B événementiel compléterait le processus de validation par la preuve. L’intérêt d’une telle validation est multiple.

• Elle permet de contrôler si les exigences du cahier des charges sont prises en compte dans les différents modèles. L’utilisateur est en mesure de décrire un scénario d’utilisation et d’animer les modèles en fonction de ce scénario ;
• Elle permet de valider des propriétés liées au comportement et de contrôler si le modèle possède le même comportement que le système modélisé ;
• Elle guide le développeur dans le processus de preuve, par exemple, en permettant de contrôler si l’invariant de collage est bien satisfait dans le cas d’un raffinement ;
• Elle permet de définir un contrôleur de système qui surveille son fonctionnement par espionnage des événements déclenchés (monitoring).

Nous avons proposé d’animer les modèles B Evénementiel en utilisant une technique formelle de modélisation de données. Le principe est de suivre les traces des événements déclenchés. Nous avons pour cela traduit les modèles B dans le langage de modélisation de données EXPRESS. Les traces des exécutions sont rangées dans des instances d’objets EXPRESS. Nous avons développé, à base de cette technique, un animateur, nommé B2EXPRESS, permettant de suivre les exécutions de modèles B Evénementiels selon plusieurs modes d’animation, avec ou sans vérification de l’invariant, des assertions, avec contrôle des gardes uniquement etc.