Abstract FR:

Cette thèse étudie une approche pour la vérification des interfaces Homme Machine fondée sur le formalisme à flots de données Lustre. Elle consiste à construire des modèles formels de l’IHM décrits en Lustre et de les utiliser pour vérifier des propriétés des interfaces par les techniques de model-checking. L’approche présente deux difficultés : la première est que les modèles d’IHM en Lustre ne sont pas facilement compréhensibles pour l’utilisateur ; la deuxième est due au problème de l’explosion combinatoire inhérente au model checking. Le travail de cette thèse cherche à apporter des solutions à ces difficultés, en proposant d’abord d’étudier un lien entre le modèle d’IHM à flots de données décrit en Lustre et le modèle d’IHM d’York lui-même fondé sur un formalisme d’ordre partiel. La relation exhibée entre les deux modèles d’IHM aboutit à deux propositions. La première consiste à donner aux descriptions Lustre d’IHM une sémantique d’ordre partiel qui permet de rendre ces descriptions plus compréhensibles. La deuxième proposition consiste en une approche de vérification par abstraction destinée à optimiser les opérations de preuves des propriétés. L’approche est fondée sur la relation d’abstraction des modèles d’ordre partiel associés aux descriptions Lustre d’IHM. Les propriétés des interfaces sont vérifiées sur des modèles Lustre d’IHM abstraits, plus petits que les modèles concrets. La mise en œuvre proposée s’appuie sur des techniques d’analyse statistique fondées sur la sémantique d’ordre partiel de textes Lustre : le calcul par interprétation abstraite des modèles Lustre abstraits à partir des modèles Lustre concrets et l’identification des certaines abstractions sur la base de deux stratégies d’analyse statique proposées. La généralisation de cette approche a permis d’aboutir à la proposition d’une technique complémentaire de réduction des modèles Lustre d’IHM et de sa mise en œuvre par analyse statique des textes Lustre.