University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur MOUFFOK, Reguia |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la rechercheUtilisation des méthodes formelles pour la vérification des systèmes interactifs / MOUFFOK, Reguia
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 : 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 : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0026 MAI/0026 Mémoire Bibliothéque des sciences Français Disponible
Disponible
