Contribution à la formalisation des propriétés graphiques des systèmes interactifs pour la validation automatique

Résumé : Dans la plupart des secteurs, les systèmes d'aujourd'hui sont interactifs et disposent d'in-terfaces graphiques sophistiquées. A notre connaissance, il existe peu d'études sur la vérifi-cation des propriétés spécifiques de la scène graphique des interfaces homme-machine et en particulier sur celles liées à la visibilité des composants graphiques par l'utilisateur humain. Dans ce papier, nous introduisons notre formalisme permettant de spécifier certaines proprié-tés des composants graphiques, dans l'objectif de réaliser à terme un outillage de validation automatique de ces propriétés. Nous illustrons l'usage de ce formalisme pour des propriétés extraites d'une norme décrivant un instrument critique présent dans les cockpits d'avions com-merciaux. Nous avons développé une version complètement fonctionnelle de cet instrument au moyen de Smala, un langage interactif de haut niveau produit par notre équipe. Cela nous permet de montrer la manière dont nous envisageons les opérations de validation formelle automatique de propriétés graphiques de tels systèmes.