| Titre : |
Conception et vérification formelles des interfaces homme-machine multimodales : application à la multimodalité en sortie |
| Type de document : |
thèse |
| Auteurs : |
Linda MOHAND-OUSSAÏD, Auteur ; Yamine AIT AMEUR, Directeur de thèse ; Idir AIT SADOUNE, Directeur de thèse ; LIAS UR 20299 UP-ENSIP / ISAE-ENSMA, Commanditaire ; Christophe KOLSKI, Rapporteur ; Hassan MOUNTASSIR, Rapporteur ; Patrick GIRARD, Examinateur ; Christian ATTIOGBE, Examinateur |
| Importance : |
184 p. |
| Note générale : |
NNT 2014ESMA0022
Remerciements
Table des matières
Table des figures
Liste des tableaux
Introduction générale
Bibliographie
Résumé
Mots clés |
| Catégories : |
Interaction homme-ordinateur
Interfaces utilisateur (informatique)
Méthode B (informatique)
Systèmes, Analyse de
Systèmes, Conception de
|
| Résumé : |
LES INTERFACES HOMME-MACHINE MULTIMODALES
Introduction
Interaction homme-machine
Systèmes interactifs
Concepts de base
Interfaces homme-machine multimodales
Développement des interfaces homme-machine
Les modèles de description du dialogue
Propriétés des interfaces homme-machine
Conception des IHM multimodales
Les systèmes multimodaux
Conclusion
DEVELOPPEMENTS FORMELS DES SYSTEMES INTERACTIFS
Introduction
Les modèles formels
La conception formelle
Les méthodes de spécification formelles
Vérification formelle
Utilisation des méthodes formelles pour le développement des IHM
Synthèse et proposition
UN MODELE FORMEL GENERIQUE POUR LES INTERFACES HOMME-MACHINE MULTIMODALES EN SORTIE
Introduction
Démarche générale de modélisation
Modèle formel de conception des interfaces homme-machine multimodales en sortie
Conclusion
MODELISATION DES INTERFACES HOMME-MACHINE MULTIMODALES EN SORTIE DANS B EVENEMENTIEL
Introduction
La méthode B événementiel
Démarche de modélisation avec B événementiel
Les modèles génériques de développement B événementiel
Conclusion
MODELISATION DE LA FISSION SEMANTIQUE AVEC B EVENEMENTIEL : GENERALISATION
Introduction
Démarche de modélisation avec B événementiel
Le modèle de fission sémantique
Bilan des obligations de preuve
Intanciation du modèle B événementiel de fission sémantique
Application à l'étude de cas
Conclusion
MODELISATION DE L'ALLOCATION AVEC B EVENEMENTIEL : GENERALISATION
Introduction
Démarche de modélisation avec B événementiel
Le modèle de combinaison des présentations
Le modèle de décomposition des présentations
Le modèle d'affectation
Bilan des obligations de preuve
Instanciation du modèle B événementiel d'allocation
Application à l'étude de cas
Vérification des propriétés
Conclusion
CONCLUSION GENERALE ET PERSPECTIVES |
| En ligne : |
https://tel.archives-ouvertes.fr/tel-01127547 |
Faire une suggestion Affiner la rechercheApproche dirigée par les modèles pour la conception et la validation des applications interactives : une démarche basée sur la modélisation des tâches
Théorie et synthèse des machines numérales
