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.

Publications par années

2012

Verification and validation of BPEL processes. A proof and animation based approach. Idir Ait-Sadoune, Yamine Ait-Ameur and Mickaël Baron. Rodin User and Developer Workshop : Deploy Federated Event. Fontainebleau, France. February, 2012.

2011

A formal framework for design and validation of multimodal interactive systems in transport domain. Linda Mohand-Oussaïd, Nadjet Kamel, Idir Ait-Sadoune, Yamine Ait-Ameur and Mohamed Ahmed-Nacer. Human–computer interaction in transport, pp. 93-128. Christophe Kolski Editor, ISTE Ltd and John Wiley & Sons, Inc. 2011.

Modeling information fission in output multi-modal interactive systems using Event B. Linda Mohand-Oussaïd, Idir Ait-Sadoune and Yamine Ait-Ameur. 1st International Conference on Model & Data Engineering (MEDI). Lecture Notes in Computer Science (LNCS), vol. 6918/2011, pp 200-213. Edited by Springer Berlin/Heidelberg. Óbidos, Portugal. September, 2011.

2010

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, Mickaël Baron and Jean-Marc Mota. Journal d'Interaction Personne-Système (JIPS), vol. 1, pp. 1-30. AFIHM. 2010.

Un cadre formel pour la conception et la validation de systèmes interactifs multimodaux dans le secteur du transport. Linda Mohand-Oussaïd, Nadjet Kamel, Idir Ait-Sadoune, Yamine Ait-Ameur and Mohamed Ahmed-Nacer. Interaction homme-machine dans les transports - Personnalisation, Assistance et Information du voyageur, pp. 113-149. Christophe Kolski Editor, Hermes Science Publications. 2010.

BPEL2B : Un outil d’aide à la vérification de la composition de services Web basé sur la preuve et le raffinement. Idir Ait-Sadoune. Actes des 10es Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), pp. 65-74. Poitiers, France. Juin, 2010.

Stepwise Design of BPEL Web Services Compositions, An Event B Refinement Based Approach. Idir Ait-Sadoune and Yamine Ait-Ameur. 8^thACIS conference on Software Engineering Research, Management and Applications (SERA). Studies in Computational Intelligence (SCI), vol. 296/2010, pp. 51-68. Edited by Springer Berlin/Heidelberg. Montreal, Canada. May, 2010.

A Proof Based Approach for Formal Verification of Transactional BPEL Web Services. Idir Ait-Sadoune and Yamine Ait-Ameur. 2^nd International Conference on Abstract State Machines, Alloy, B and Z (ABZ). Lecture Notes in Computer Science (LNCS), vol. 5977/2010, pp. 405-406. Edited by Springer Berlin/Heidelberg. Orford, Quebec, Canada. February, 2010.

2009

A Proof Based Approach for Modelling and Verifying Web Services Compositions. Idir Ait-Sadoune and Yamine Ait-Ameur. Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 1-10. Edited by IEEE Computer Society. Potsdam, Germany. June, 2009.

From BPEL to Event-B. Idir Ait-Sadoune and Yamine Ait-Ameur. International Workshop on Integration of Model-based Formal Methods and Tools (IM FMT) at 7th International Conference on Integrated Formal Methods (IFM). Düsseldorf Germany, February, 2009.

2008

Développements formels d'interfaces multimodales fondés sur la preuve et le raffinement. Scénarios de développement. Yamine Ait-Ameur, Idir Ait-Sadoune, Mickaël Baron and Jean-Marc Mota. Revue des Sciences et Technologies de l'Information (RSTI), série Ingénierie des Systèmes d'Information (ISI), Modélisation multiple, Formalisme et Modèles, vol. 13 N° 2, pp. 127-154. Edité par Lavoisier. 2008.

Animating Event B Models by Formal Data Models. Idir Ait-Sadoune and Yamine Ait-Ameur. 3^rd International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA). Communications in Computer and Information Science (CCIS), vol. 17, part 3, pp. 37-55. Edited by Springer Berlin/Heidelberg. Kassandra, Greece. October, 2008.

Verification and Validation of  Web Service Composition Using Event B Method. Idir Ait-Sadoune and Yamine Ait-Ameur. 1^st International Conference on Abstract State Machines, B and Z (ABZ).  Lecture Notes in Computer Science (LNCS), vol. 5238/2008, pp. 339-340. Edited by Springer Berlin/Heidelberg. London, UK. September, 2008.

Semantic Hubs for Geological Projects. Yamine Ait-Ameur, Idir Ait-Sadoune, Nabil Belaid, Mohammed Bennis, Olivier Corby, Rose Dieng-Kuntz, Jérémie Doucy, Priscille Durville, Chimène Fankam, Fabien L. Gandon, Alain Giboin, Patrick Giroux, Sandrine Grataloup, Bruno Grilheres, Florian Husson, Stéphane Jean, Joel Langlois, Phuc-Hiep Luong, Laura Silveira Mastella, Olivier Morel, Michel Perrin, Guy Pierra, Jean-François Rainaud, Eric Sardet, Francois Tertre and João Francisco Valiati. 1^st International Workshop on Semantic Metadata Management and Applications (SeMMA) at the 5^th European Semantic Web Conference (ESWC).  CEUR Workshop Proceedings,  vol 346, pp. 3-17. Teneriffe, Spain. June, 2008.

Une architecture orientée services pour la gestion sémantique des données géologiques pour le stockage de CO2. Nabil Belaid, Idir Ait-Sadoune, Yamine Ait-Ameur, Jean-François Rainaud and Stéphane Jean. Actes de l’atelier Systèmes d’Information et de Décision pour l’Environnement (ASIDE) du XXVI^ème Congrès INFORSID, pp. 67-76. Fontainebleau (Seine-et-Marne), France. Mai, 2008.

2007

B2EXPRESS : Un animateur de modèles B événementiel. Idir Ait-Sadoune. Actes des 8es Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), pp. 295-296. Namur, Belgique. Juin, 2007.

2006

Validation et Vérification Formelles de Systèmes Interactifs Multi-Modaux Fondées sur la Preuve. Yamine Ait-Ameur, Idir Ait-Sadoune, Mickael Baron and Jean-Marc Mota. Actes de la 18e Conférence Francophone sur l'Interaction Homme-Machine (IHM), pp. 123-130. Edited by ACM International Conference Proceeding Series. Montréal, Canada. Avril, 2006.

Etude et comparaison de scénarios de développements formels d'interfaces multi-modales fondés sur la preuve et le raffinement. Yamine Ait-Ameur, Idir Ait-Sadoune and Mickael Baron. Actes de la 6ème Conférence Francophone de Modélisation, Optimisation et Simulation des Systèmes (MOSIM) : Défis et Opportunités, pp. 578-588. Edited by Lavoisier. Rabat, Maroc. Avril, 2006.