Actuellement, les applications interactives sont utilisées dans de nombreux domaines (guichets automatiques, tours de contrôle...), par des publics très différents (enfants, experts, handicapés...) et par un nombre important d'utilisateurs (interfaces de téléphones portables...) ou au contraire très spécifiques (logiciels conçus spécifiquement pour une entreprise). Elles sont de ce fait très diverses. De par la multiplicité des paramètres à prendre en compte, la conception et le développement des applications interactives sont devenus très coûteux. Afin de réduire ces coûts, des recherches sont actuellement menées sur le processus de conception. Cette thèse s'inscrit dans ces travaux. L'un des axes étudiés pour réduire le coût de production des applications interactives est la détection des erreurs le plus en amont possible pendant le processus de conception. Nous proposons de faciliter la vérification et la validation de la dynamique des applications (plus spécifiquement dénommée dialogue) tout au long de la conception, en fonction des spécifications recueillies auprès des futurs utilisateurs, exprimés sous forme de modèles de tâches. Les modèles de dialogue et les modèles de tâches représentent deux points de vue différents et complémentaires pour une même application. Nous proposons une approche de vérification de cohérence entre ces deux modèles tout au long du cycle de vie de l'application. Pour cela, nous avons défini des règles de cohérence entre les modèles que nous vérifions formellement en utilisant une méta-modélisation des formalismes que nous avons choisis après évaluation de leur utilisation pour une conception centrée-utilisateur.