Un modèle pour une satisfaction implicite des propriétés d’utilisabilité care pour les IHM multimodales

Nous proposons un modèle formel d’interaction multimodale intégrant les spécifications des propriétés d’utilisabilité CARE (Complémentarité, Assignation, Redondance et Équivalence). Le modèle permet la conception d’interfaces multimodales vérifiant de manière implicite les propriétés CARE désirées. Ceci permet d’éviter l’étape de vérification de ces propriétés après la conception de l’interface. Ainsi, le temps et le coût de développement de ces systèmes sont réduits. Le modèle a été validé en utilisant la technique de vérification sur modèle (model-checking) SMV (Symbolic Model Verifier) sur une étude de cas.