LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: 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, 000, Verification, User interface, Human computer interaction, HCI, Usability, Formal methods, Event B method, Static Analysis, Dialog model, Task model
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. 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).
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article