Les applications interactives sont aujourd'hui présentes dans plusieurs domaines et leur utilisation au sein de systèmes critiques est de plus en plus fréquente. Leur puissance ne cesse d'augmenter ainsi que leur complexité ce qui accroît le risque que des fautes soient introduites pendant les différentes étapes de leur développement. Leur correction devient ainsi un enjeu important et leur développement requiert une validation rigoureuse. Outre le besoin de correction fonctionnelle, les exigences attendues d'une application interactive s'expriment en termes d'utilisabilité, définie au moyen de propriétés ergonomiques. La vérification de ces dernières n'est pas une tâche facile, leur définition étant souvent trop informelle ou bien difficilement exprimable en des termes exploitables par des ingénieurs de développement ou de validation. Dans cet article, nous présentons la formalisation de certaines propriétés ergonomiques qui pourront ultérieurement être validées automatiquement. Pour cela, nous nous basons sur une notation courante dans le domaine de l'interaction homme-machine, les arbres des tâches, déjà utilisée dans le cadre de nos travaux antérieurs pour la génération automatique de tests. Nous identifions les insuffisances du modèle sousjacent à cette génération en vue de la prise en compte de propriétés ergonomiques et nous exhibons une extension de ce dernier permettant d'envisager le test de certaines d'entre elles.