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