Titre :	Utilisation des méthodes formelles pour la vérification des systèmes interactifs
Type de document :	texte imprimé
Auteurs :	MOUFFOK, Reguia ; KAMEL, N, Directeur de thèse
Editeur :	Setif:UFA
Année de publication :	2012
Importance :	1 vol (54f.)
Format :	29 cm
Langues :	Français (fre)
Catégories :	Thèses & Mémoires:Informatique
Mots-clés :	Système interactif, IHM, méthode formelle, Model checking, logique temporelle, modèle de tâche.
Index. décimale :	004 Informatique
Résumé :	Résumé Prévoir l’échec dans des systèmes interactifs est difficile puisqu’ils peuvent fonctionner dans des conditions opérationnelles imprévisibles ils sont soumis à beaucoup de facteurs incluant le noyau fonctionnel du système, le comportement de l’opérateur humain, les dispositifs d’interaction, des interfaces des dispositifs et l’environnement opérationnel. L’utilisation des méthodes formelles dans le développement de ce type de systèmes peut aider à minimiser le taux d’échec.
Note de contenu :	Table des matières 1 Les systèmes interactifs et les IHMs 7 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Les systèmes interactifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.1 Définition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.2 La décomposition des systèmes interactifs . . . . . . . . . . . . . . 8 1.2.3 Développement des systèmes interactifs . . . . . . . . . . . . . . . . 8 1.2.4 L’évaluation des systèmes interactifs . . . . . . . . . . . . . . . . . 8 1.2.5 Les propriétés des systèmes interactifs . . . . . . . . . . . . . . . . 9 1.3 Les interfaces Homme-Machine . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.1 Notations pour la description d’IHM . . . . . . . . . . . . . . . . . 11 1.4 Les modèles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.4.1 Modèles d’architecture et de conception . . . . . . . . . . . . . . . . 13 1.4.2 Le modèle de tâche . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2 Les techniques de vérification formelles 16 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Définition de la vérification formelle . . . . . . . . . . . . . . . . . . . . . . 16 2.3 Introduction aux méthodes formelles . . . . . . . . . . . . . . . . . . . . . 17 2.4 Définition des méthodes formelles . . . . . . . . . . . . . . . . . . . . . . . 18 2.4.1 Pourquoi les méthodes formelles . . . . . . . . . . . . . . . . . . . . 18 2.4.2 Apports des méthodes formelles . . . . . . . . . . . . . . . . . . . . 19 2.4.3 Limites des méthodes formelles . . . . . . . . . . . . . . . . . . . . 20 2.5 Classification des méthodes formelles . . . . . . . . . . . . . . . . . . . . . 21 2.5.1 Les Méthodes déductives . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5.2 Les méthodes automatiques . . . . . . . . . . . . . . . . . . . . . . 23 2.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 La vérification formelle des systèmes interactifs 29 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2 Des exemples utilisant les méthodes automatiques . . . . . . . . . . . . . . 29 3.2.1 Développement d’un distributeur de billets en utilisant les RDPs . . 29 3.2.2 La pompe PCA (Patient Controlled Analgesia) . . . . . . . . . . . 32 3.2.3 Le système du guichet automatique . . . . . . . . . . . . . . . . . . 40 3.3 Un exemple utilisant une méthode déductive . . . . . . . . . . . . . . . . . 46 3.3.1 L’étude du cas Post-It Notes en méthode B . . . . . . . . . . . . . 46 3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
Côte titre :	MAI/0026
En ligne :	https://drive.google.com/file/d/10X_gaxuexpLOwfvMkWcqBiWI2OBBOFJH/view?usp=shari [...]
Format de la ressource électronique :	pdf

Utilisation des méthodes formelles pour la vérification des systèmes interactifs [texte imprimé] / MOUFFOK, Reguia ; KAMEL, N, Directeur de thèse . - [S.l.] : Setif:UFA, 2012 . - 1 vol (54f.) ; 29 cm.
Langues : Français (fre)

Catégories :	Thèses & Mémoires:Informatique
Mots-clés :	Système interactif, IHM, méthode formelle, Model checking, logique temporelle, modèle de tâche.
Index. décimale :	004 Informatique
Résumé :	Résumé Prévoir l’échec dans des systèmes interactifs est difficile puisqu’ils peuvent fonctionner dans des conditions opérationnelles imprévisibles ils sont soumis à beaucoup de facteurs incluant le noyau fonctionnel du système, le comportement de l’opérateur humain, les dispositifs d’interaction, des interfaces des dispositifs et l’environnement opérationnel. L’utilisation des méthodes formelles dans le développement de ce type de systèmes peut aider à minimiser le taux d’échec.
Note de contenu :	Table des matières 1 Les systèmes interactifs et les IHMs 7 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Les systèmes interactifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.1 Définition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.2 La décomposition des systèmes interactifs . . . . . . . . . . . . . . 8 1.2.3 Développement des systèmes interactifs . . . . . . . . . . . . . . . . 8 1.2.4 L’évaluation des systèmes interactifs . . . . . . . . . . . . . . . . . 8 1.2.5 Les propriétés des systèmes interactifs . . . . . . . . . . . . . . . . 9 1.3 Les interfaces Homme-Machine . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.1 Notations pour la description d’IHM . . . . . . . . . . . . . . . . . 11 1.4 Les modèles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.4.1 Modèles d’architecture et de conception . . . . . . . . . . . . . . . . 13 1.4.2 Le modèle de tâche . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2 Les techniques de vérification formelles 16 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Définition de la vérification formelle . . . . . . . . . . . . . . . . . . . . . . 16 2.3 Introduction aux méthodes formelles . . . . . . . . . . . . . . . . . . . . . 17 2.4 Définition des méthodes formelles . . . . . . . . . . . . . . . . . . . . . . . 18 2.4.1 Pourquoi les méthodes formelles . . . . . . . . . . . . . . . . . . . . 18 2.4.2 Apports des méthodes formelles . . . . . . . . . . . . . . . . . . . . 19 2.4.3 Limites des méthodes formelles . . . . . . . . . . . . . . . . . . . . 20 2.5 Classification des méthodes formelles . . . . . . . . . . . . . . . . . . . . . 21 2.5.1 Les Méthodes déductives . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5.2 Les méthodes automatiques . . . . . . . . . . . . . . . . . . . . . . 23 2.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 La vérification formelle des systèmes interactifs 29 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2 Des exemples utilisant les méthodes automatiques . . . . . . . . . . . . . . 29 3.2.1 Développement d’un distributeur de billets en utilisant les RDPs . . 29 3.2.2 La pompe PCA (Patient Controlled Analgesia) . . . . . . . . . . . 32 3.2.3 Le système du guichet automatique . . . . . . . . . . . . . . . . . . 40 3.3 Un exemple utilisant une méthode déductive . . . . . . . . . . . . . . . . . 46 3.3.1 L’étude du cas Post-It Notes en méthode B . . . . . . . . . . . . . 46 3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
Côte titre :	MAI/0026
En ligne :	https://drive.google.com/file/d/10X_gaxuexpLOwfvMkWcqBiWI2OBBOFJH/view?usp=shari [...]
Format de la ressource électronique :	pdf