Ce mémoire présente un cadre pour l'aide à la spécification d'interfaces homme-machine de haut niveau qui comprote un formalisme et un environnement de développement spécifique. Le formalisme est fondé sur un modèle conceptuel de spécification qui prend en compte l'aspect utilisateur (modèles cognitifs) et les aspects fonctionnels (modèles d'architecture). Les outils initialement disponibles dans l'environnement consistaient en un éditeur syntaxique et un générateur de prototypes exécutables. l'ambition de ce travail consiste à augmenter la panoplie d'outils disponibles. Tout d'abord, un outil de validation statique a été implanté. Ce travail, qui a permis de polir la définition du formalisme, a également permis d'en analyser plus finement la structure. Il est ainsi apparu une forte redondance structurelle entre les trois parties qui composent une spécification. Ces observations ont conduit à la définition et à l'implantation d'opérateurs d'aide à la construction de spécifications. Ces opérateurs permettent de générer du texte vérifiant formellement des propriétés sémantiques et d'interface, à partir d'informations saisies par le spécifieur. Une autre ambition de ce travail est des donner une sémantique rigroureuse au formalisme et aux outils associés. Pour cela, nous utilison le langage de description sémantique TYPOL, associé au générateur d'environnements CENTAUR, pour décrire et programmer nos outils.