Bienvenue sur ArTeMIS, la plate-forme d’archivage et de diffusion des thèses et mémoires de l’ISAE-SUPAERO.
Vous y trouverez les thèses soutenues à Supaero depuis 1979 et à l’ISAE-SUPAERO depuis 2007 ayant fait l´objet d´une numérisation ou d´un dépôt électronique et pour lesquelles nous avons obtenu l’autorisation de diffusion.
???menu.label.??? > ???menu.label..??? fr| en
Artemis
  • A propos
  • Contact
  • Recherche
  • simple
  • Tous les mots:
  • avancée
  • Consulter par
  • auteur
  • année
  • thématique
  • laboratoire
  • équipe de recherche
  • école doctorale
Version imprimable
Contribution à la validation formelle d’applications interactives Java

Cortier, Alexandre
2008-06-06

Institut Supérieur de l'Aéronautique et de l'Espace
Directeur(s) de thèse:  D'Ausbourg, Bruno; Aït-Ameur, Yamine
Laboratoire :  Département Traitement de l’Information et Modélisation -DTIM (depuis 1997)
Ecole doctorale :  Mathématiques, Informatique et Télécommunications de Toulouse -MITT

Classification : Informatique
Accès : Texte intégral

Mots-clés : Validation, Vérification, Méthodes Formelles, Interaction Homme-Machine, IHM, Utilisabilité, Méthode B événementiel, NuSMV, Theorem Proving, Model-Checking, Analyse Statique, Abstraction, Modèle de dialogue, Java, Swing, Java-Swing, CTT, Modèle de Tâches

Résumé : Les travaux présentés dans ce manuscrit proposent une approche formelle pour la validation d'applications interactives Java-Swing vis-à-vis d'une spécification décrite par un modèle de tâches CTT. L'objectif de cette approche est de valider une partie de l'utilisabilité du système en s'appuyant sur l'extraction d'un modèle formel décrivant le comportement dynamique de l'application (modèle de dialogue). Cette extraction est obtenue par analyse statique du code source Java-Swing de l'application. La validation du système consiste alors à démontrer formellement que les structures d'interaction encodées dans le programme s'inscrivent bien dans les scénarii d'usage représentés en compréhension par le modèle de tâches CTT. Cette étape de validation exploite d'une part le modèle formel extrait par analyse statique et d'autre part une formalisation du modèle de tâches. La démarche d'extraction et de validation est abordée suivant deux techniques formelles distinctes : la méthode B événementielle basée sur la démonstration de théorèmes (theorem-proving), et la méthode NuSMV basée sur la vérification exhaustive de modèles (model-checking). Une étude de cas permet d'illustrer tout au long du mémoire la démarche de validation proposée suivant ces deux techniques formelles.

Résumé (anglais) : User Interface (UI) systems are increasingly complex and nowadays assist critical activities. The development of UIs needs empowered validation methodologies in order to ensure the correctness of the developed UI-based applications. This thesis investigates the applicability of reverse engineering, static analysis and formal approaches to the validation and the verification of UIs correctness. The approach is the following. User interface’s abstract models (NuSMV and B Event models) are derived starting from its Java/Swing source code. These formal execution models (dialog models) are then used to prove that the developed interactive system is in accordance with usability requirements expressed in CTT tasks models. A case study illustrates the proposed validation and verification process following these two formal techniques (Model-Checking with NuSMV and Theorem-Proving with Event B).


Langue : Français
Exporter au format XML
© 2006-2010 ORI-OAI
thèses ISAE,theses ISAE,thèse ISAE,these ISAE, thèses Institut Supérieur de l'Aéronautique et de l'Espace,thèse Institut Supérieur de l'Aéronautique et de l'Espace,,theses Institut Supérieur de l'Aéronautique et de l'Espace,,these Institut Supérieur de l'Aéronautique et de l'Espace, thèses aéronautique,thèse aéronautique,these aéronautique,,theses aéronautique, Artemis,Arthemis, thèses DAEP,thèses DMIA,thèses DMSM, thèses DEOS,thèses CAS,thèses LACS, thèse DAEP,thèse DMIA,thèse DMSM, thèse DEOS,thèse CAS,thèse LACS, these DAEP,these DMIA,these DMSM, these DEOS,these CAS,these LACS, theses DAEP,theses DMIA,theses DMSM, theses DEOS,theses CAS,theses LACS, thèses toulouse,thèse toulouse,theses toulouse,these toulouse, thèses supaero,thèse supaero,theses supaero,these supaero, thèses école nationale supérieure d'aéronautique,thèse école nationale supérieure d'aéronautique,theses école nationale supérieure d'aéronautique,these école nationale supérieure d'aéronautique, thèses ingénieur,thèse ingénieur,theses ingénieur,these ingénieur, phd thesis ISAE, phd thesis Institut Supérieur de l'Aéronautique et de l'Espace, phd thesis aéronautics, phd thesis DAEP,phd thesis DMIA,phd thesis DMSM,phd thesis DEOS,phd thesis CAS,phd thesis LACS, phd thesis toulouse,phd thesis supaero,phd thesis école nationale supérieure d'aéronautique,