Mickael BARON - These

École Nationale Supérieure de Mécanique et d’Aérotechnique /Université de PoitiersLaboratoire d’Informatique Scientifique et Industrielle (www.lisi.ensma.fr)ENSMA - Téléport 2-1 Avenue Clément Ader - BP 40109 - 86961 FUTUROSCOPE CHASSENEUIL Cedex - FranceVers une approche sûre du développement des Interfaces Homme-MachineEnjeuxEnjeuxDéveloppement, validation et Les interfaces homme-machine (IHM) constituent une vérification de systèmes interactifspart indispensable dans la quasi-totalité des systèmes Approches fondées sur le Approches fondées sur informatiques. Le recours à des modèles de développement formel la définition d’outilsspécification, de développement, de vérification et de validation devient indispensable. Aujourd’hui les Model Based SystemsConstructeurs UIApproches existantes Systèmes de preuvesapproches fondées sur le développement formel et les • Spécification de • Outils d’aide à la approches fondér la définition d ’outils peuvent • CNUCE (Lotos) • Model Checkingmodèlesêtre mises en parallèle pour la vérification de propriétés. conceptionCNUCE, CERT, ICO• York (Z)• Génération UIMalgré des avancées intéressantes, aucune d’elles • Absence de prise en • Theorem Proving• ICO (Réseaux de Petri)n’est encore parvenue à s’imposer. compte de l’utilisateur • MASTERMIND, York et LISI• LISI (Méthode B) MOBI-D, Petshop• JBuilder, Visual .NETL’objectif général de nos travaux consiste à améliorer • CERT (Lustre)l’utilisation de méthodes formelles dans ...