Systèmes informatiques interactifs

Télécharger le fichier original (Mémoire de fin d’études)

Comment formaliser les éléments de la scène graphique des interfaces humain-machine ?

Au cours des dernières décennies, de nombreuses méthodes formelles ont été proposées pour le développement de systèmes informatiques interactifs sûrs et fonc-tionnellement corrects. Toutefois, lorsque des techniques de vérification formelle sont utilisées, elles permettent souvent de ne couvrir que partiellement les problèmes liés aux interfaces humain-machine [53, 79, 32]. D’une part, elles adressent large-ment les propriétés comportementales des systèmes. D’autre part, nous constatons que les propriétés liées à la spécificité des systèmes informatiques interactifs, par exemple celles spécifiques à la scène graphique, sont peu étudiées. Par exemple, il y a peu d’exemples avec les méthodes formelles actuelles permettant de garan-tir les exigences relatives aux éléments graphiques d’une interface humain-machine impliquant la forme, la couleur, la position dans l’interface, etc.
De plus, nous avons précisé que la conception de la scène graphique suit souvent une norme ou des règles de conception imposées [119, 123]. Or, l’expression formelle de ces propriétés est encore peu développée ce qui laisse la place à des erreurs d’interprétation.
Ainsi, formaliser les éléments de la scène graphique des interfaces humain-machine permettrait de:
• définir sans ambiguïté les éléments de la scène graphique et leurs propriétés,
• mécaniser la vérification des exigences graphiques des systèmes informatiques interactifs.

Comment mécaniser la vérification des exigences gra-phiques des systèmes informatiques interactifs ?

Il existe deux approches pour vérifier la conformité d’un système à une spécifi-cation technique :
• Appliquer la vérification sur un modèle de la spécification puis traduire le modèle en code du système (par exemple, « Un modèle B événementiel décrit un système réactif par un ensemble d’événements qui modifient un état. Le raﬃnement permet de bâtir ce modèle étape par étape en introduisant de nouveaux événements tout en préservant les propriétés établies. » [7]).
• Appliquer la vérification sur un modèle du système obtenu à partir de son code (par exemple, Frama-C [109] possède des outils d’analyse de code permettant de vérifier des propriétés de programmes écrits en C et son plugin WP utilise notamment la logique de Hoare pour vérifier des propriétés par annotation de code).
La première approche est contraignante du fait de la nécessité de produire une traduction du modèle en du code informatique pour implémenter le système. Cepen-dant, même si le modèle vérifie les exigences de la spécification, il faut assurer que la traduction est sûre et que le code résultant est équivalent au modèle de la spéci-fication. Nous verrons aussi que les quelques approches de vérification formelle des propriétés graphiques des systèmes informatiques interactifs suivent jusqu’à présent cette approche.
Nous privilégions la seconde approche. Celle-ci reste en eﬀet plus simple car elle prend en entrée le code final du système qui est eﬀectivement exécuté. De plus, cette approche restant extrêmement peu explorée pour les systèmes informatiques interactifs, son étude nous apparaît comme la plus pertinente.
Ainsi, analyser statiquement le code des systèmes informatiques interactifs per-mettrait de vérifier formellement et de manière plus sûre les exigences graphiques de ces systèmes le tout en assurant l’exhaustivité de la vérification grâce à l’exploration systémique de tous les scénarios possibles.

Plan du manuscrit

Chapitre 2. Concepts de base. Ce chapitre introduit les diﬀérents concepts qui permettent de préciser notre problématique sur la vérification formelle des pro-priétés graphiques des systèmes informatiques interactifs. Nous présentons les quatre paradigmes de programmation usuels (impératif, fonctionnel, objet, réactif) et leurs particularités spécifiquement dans le contexte de leur vérification. Nous présentons ensuite notre classification des propriétés relatives aux systèmes informatiques in-teractifs et liées à l’interaction. Nous présentons enfin notre nomenclature des for-malismes.
Chapitre 3. État de l’art. Ce chapitre constitue une revue de la littérature visant à extraire et classer les propriétés liées à l’interaction et formalismes utilisés pour la vérification de ces propriétés. Son objectif principal est de répondre à trois questions :
• Quelles sont les propriétés liées à l’interaction étudiées ?
• Quels sont les formalismes utilisés pour ce faire ?
• Quels sont les principaux cas d’étude utilisés pour démontrer l’approche ?
La deuxième partie de ce chapitre est une analyse de la revue précédente. Notre objectif ici est de répondre à deux questions :
• Quelles sont les propriétés liées à l’interaction les plus couvertes et celles qui sont les moins adressées ?
• Quels sont les formalismes les plus utilisés pour l’expression et la vérifica-tion des propriétés des systèmes informatiques interactifs, et y en a-t-il des nouveaux qui ont émergé spécifiquement pour ce type de propriétés ?
En répondant à ces questions, nous justifions nos questions de recherche. Chapitre 4. Cas d’étude : Smala et TCAS. Ce chapitre introduit dans un
premier temps le contexte de ces travaux de thèse.
Tout d’abord, nous présentons le secteur de l’aéronautique qui est au cœur des pro-blématiques de notre équipe de recherche. Ce secteur définit de nombreuses normes que les systèmes informatiques interactifs doivent absolument respecter. L’usage des méthodes formelles est conseillé pour vérifier que les systèmes respectent ces normes. Nous présentons ensuite le langage de programmation réactive Smala développé par notre équipe et qui sert de base à nos travaux.
Enfin, nous présentons le cas d’étude que nous utilisons : le TCAS ((Trafic alert and Collision Avoidance System)), un système de prévention des collisions aériennes dont l’aﬃchage peut être intégré dans diﬀérents équipements du cockpit des aéronefs.
Chapitre 5. Vérification des propriétés graphiques. Ce chapitre présente le processus de vérification des propriétés graphiques que nous avons développé au cours ces travaux de thèse. Nous présentons le formalisme que nous avons développé afin d’exprimer formellement les exigences graphiques des systèmes informatiques interactifs. Nous présentons ensuite l’algorithme qui analyse les diﬀérents opéra-teurs graphiques que nous avons définis. Enfin, nous présentons GPCheck, l’outil de vérification des propriétés graphiques que nous avons développé et qui implémente notre algorithme.
Chapitre 6. GPCheck : Application au TCAS. Dans ce chapitre, nous appliquons notre processus et utilisons notre outil sur notre cas d’étude : le TCAS intégré à l’IVSI (Instantaneous Vertical Speed Indicator). Nous appliquons le proces-sus de vérification aux exigences graphiques de ce système informatique interactif.
Chapitre 7. Conclusion et discussion. Dans ce chapitre, nous synthétisons les diﬀérents « findings » de cette thèse et rappelons les réponses que nous avons apportées à chacun d’entre eux à travers nos contributions. Nous discutons ensuite des résultats obtenus et envisageons les pistes futures permettant de prolonger ces travaux lorsque l’utilisateur interagit avec le système et de tous les sous-objectifs qui doivent être atteints en fonction de cette tâche. Cette définition du but de l’utilisateur est complétée par Rukš˙enas et al. [99]. Ils donnent les propriétés d’un but dont par exemple : la garde représentant l’activation du but ; le choix représentant la possibilité de choisir le but ; le prédicat atteint représente l’atteignabilité du but ; les sous-objectifs.
Un but d’utilisateur est donc une liste de sous-objectifs qu’un utilisateur doit réaliser pour atteindre un objectif plus important lié aux fonctionnalités du système utilisé.
Exemple. Prenons le but d’utilisateur « Retirer de l’argent à un distributeur au-tomatique de billets ». « Insérer la carte », « rentrer le code PIN » et « choisir le montant d’argent » sont des sous-objectifs de ce but d’utilisateur [82]. La garde pour atteindre le sous-objectif « choisir le montant d’argent » est ici « code PIN valide ».

Privilèges

Cerone et Elbegbayan [46] définissent les privilèges de l’utilisateur comme les interactions que l’utilisateur peut ou ne peut pas eﬀectuer avec le système en fonc-tion de son statut dans le système. À partir de cette définition, les auteurs pro-posent de contraindre le système en modifiant la conception en fonction du statut de l’utilisateur. Ces changements de conception permettent au système de limiter les interactions disponibles afin d’appliquer des privilèges d’utilisateurs au sein du système.
Les privilèges de l’utilisateur sont donc un moyen d’empêcher un utilisateur ayant un niveau d’accréditation non autorisé d’atteindre des objectifs que l’utilisa-teur ne devrait pas atteindre. Exemple. « Dans un système de gestion des articles de conférence, les utilisateurs ont des droits d’accès et d’action diﬀérents selon leur rôle (auteurs, réviseurs, orga-nisateurs). Dans ce contexte, en fonction de leur rôle dans le système, les auteurs peuvent uniquement être en mesure de soumettre et de télécharger leur propre ar-ticle, tandis que l’examinateur principal peut être en mesure de visualiser et de gérer plusieurs articles soumis par les auteurs. » [62]

Interprétation

Rukš˙enas et Curzon [100] présentent l’interprétation de l’utilisateur comme l’en-semble des hypothèses de l’utilisateur sur le système. Ces suppositions peuvent être dues à l’expérience de l’utilisateur avec le système ou un système suﬃsamment proche. L’interprétation d’un système peut amener les utilisateurs à adapter leur comportement en fonction de leurs hypothèses.
Exemple. Nous sommes habitués au raccourci Ctrl+C afin de copier du texte. Un utilisateur novice d’un terminal pourrait l’utiliser pour copier du texte et fermer l’application en cours d’exécution parce que la fonctionnalité n’est pas la même, il s’agit là d’une mauvaise interprétation de ce raccourci.

Attention

Su et al. [116] s’intéressent aux limites de l’attention temporelle des utilisateurs humains principalement dans un scénario de test de présentation visuelle en série rapide. Ils rappellent que l’attention est liée à la signification des éléments aﬃchés dans l’interface et à leur saillance. Ils précisent que le fait de s’occuper des surprises dans un schéma constant pourrait faire perdre l’attention de l’utilisateur.
Cerone [44] définit l’attention comme une activité de l’utilisateur qui doit se concentrer sur une caractéristique de l’environnement. L’utilisateur ignore les autres caractéristiques de l’environnement tout en se concentrant sur une caractéristique spécifique. L’utilisateur est plus susceptible de perdre son attention lors d’une ex-position à des stimuli soudains non liés à l’activité en cours. Plus tard, Cerone [45] ajoute les définitions de l’attention implicite et explicite. D’une part, l’attention implicite est associée à des stimuli inattendus liés à l’état mental de l’utilisateur. D’autre part, l’attention explicite se réfère à l’attention portée aux stimuli pertinents pour la tâche en cours de réalisation.
L’attention de l’utilisateur est donc la capacité de l’utilisateur à se concentrer sur une activité spécifique sans être perturbé par des informations non pertinentes.
Exemple. Au volant d’une voiture, l’utilisation d’un GPS uniquement audio (une modalité perturbatrice) permet au conducteur de porter davantage d’attention à sa vitesse que l’utilisation d’un GPS audiovidéo (deux modalités perturbatrices) [77].

Expérience

Cerone et Zhao [47] expliquent que, dans le processus de conduite, les expé-riences de l’utilisateur influencent son comportement. Si l’utilisateur est confronté à un événement particulier, tel qu’un risque inattendu, dans une situation courante, il adaptera son comportement la prochaine fois qu’il sera confronté à la situation au cours de laquelle l’événement s’est produit. Ce phénomène fait référence à ldu système prendre le dessus sur l’état réel du système dans son esprit. Cela pour-rait également conduire à ce que l’utilisateur ne voit pas du tout les informations aﬃchées, par exemple si elles sont supprimées trop tôt de l’écran. Ce problème d’aﬃchage peut résulter d’une erreur de conception ou d’un système trop lent, ce deuxième cas représentant la latence.
Leriche et al. [81] expliquent que les délais entre les interactions avec une ap-plication et le retour des informations de l’application avec des interactions tactiles peuvent rendre l’application inutilisable. Cette latence peut être gérée au niveau du matériel avec des outils conçus pour cette manipulation.
À l’origine, la latence est une problématique de réseau (temps de transmission d’un ordinateur à un autre) qui prend une autre forme dans le domaine des systèmes informatiques interactifs. « La latence d’un système interactif est le délai entre l’ac-tion d’un utilisateur et le moment où le retour d’information correspondant est présenté à l’utilisateur » [25].
Exemple. Si un ordinateur exécute plusieurs actions en même temps, il faudra quelques secondes pour lancer un navigateur web.

Cohérence

Bowen et Reeves [35] définissent la cohérence comme l’utilisation de la même terminologie pour les fonctions, les menus ou les écrans d’aide d’une application multiécrans, l’utilisation de commandes ou de séquences de commandes équivalentes afin d’atteindre des objectifs spécifiques tels que la fermeture d’une fenêtre dans l’interface.
Campos et Harrison [41] donnent trois propriétés liées à la cohérence des inter-faces : le rôle et la visibilité des modes, la cohérence de la dénomination et de la finalité des fonctions telles que décrites précédemment, la cohérence du comporte-ment des entrées de données. La première concerne la nécessité d’informer l’utilisa-teur du mode dans lequel se trouve le système, ce qui est surtout important pour les systèmes où l’utilisateur n’interagit qu’avec un dispositif physique. La troisième concerne les fonctions des touches et plus particulièrement le fait qu’elles ont un eﬀet similaire quel que soit le mode.
Harrison et al. [67] définissent deux types de cohérence dans l’utilisation des touches programmables : le premier détaille quand une même touche est associée à une même fonction, le second explique qu’un aﬃchage programmable apparaît lors de l’activation d’une touche particulière.
Harrison et al. [68] définissent la cohérence comme une propriété pour les actions. Une action telle qu’appuyer sur un bouton doit avoir le même eﬀet quel que soit le mode du système et ne doit pas avoir d’autres eﬀets que ceux prévus à l’origine par le comportement.
La cohérence représente donc un comportement constant du système, que ce soit pour un aﬃchage ou une fonctionnalité, quel que soit le mode actuel du système.
Exemple. Il peut s’agir de l’utilisation de la même terminologie pour les fonctions (« Exit » ou « Quit » afin de définir une fonction « fermer une fenêtre »).

Prédictibilité

Masci et al. [86] donnent une définition de la prédictibilité dans le cas d’utili-sateurs expérimentés et compétents avec des systèmes interactifs. Ces utilisateurs sont censés avoir des modèles mentaux corrects du système. En d’autres termes, les utilisateurs connaissent les diﬀérentes caractéristiques des systèmes et leur fonction-nement. Dans ce cas précis, les auteurs définissent la prédictibilité comme la capacité de l’utilisateur à prévoir, à partir d’un état spécifique du système, le comportement futur du système et donc son état futur lorsqu’il interagit avec lui.
La prédictibilité est donc la capacité de l’utilisateur à prédire le comportement futur du système à partir de son état actuel et de la façon dont l’utilisateur interagira avec lui.
Exemple. Lorsqu’un utilisateur s’apprête à fermer un éditeur de texte contenant un document non sauvegardé, il sait qu’une fenêtre contextuelle s’aﬃchera pour lui proposer un choix parmi : sauvegarder le document, annuler la fermeture ou fermer sans sauvegarder.

Utilisabilité

Rukš˙enas et al. [98, 99] donnent des propriétés d’utilisabilité liées aux objectifs de l’utilisateur. En matière d’objectifs de l’utilisateur, les auteurs définissent l’utilisa-bilité comme l’assurance de l’atteignabilité du principal objectif de l’interaction, ou du moins celui que l’utilisateur perçoit comme principal. Rukš˙enas et al. [98] précise également cette propriété avec l’assurance que tous les sous-objectifs de l’objectif principal seront également atteints à terme.
Coutaz et al. [51] présentent les propriétés CARE comme un moyen pour éva-luer l’utilisabilité des interactions multimodales. Elles reposent sur des notions d’état (propriété qui peut être mesurée), d’objectif (état que l’utilisateur veut atteindre), modalité (type d’interaction) et temporalité (temps passé sur une modalité). L’acro-nyme CARE correspond à :
• complementarity : les modalités doivent être utilisées de manière complémen-taire (choix oral puis choix écrit par exemple),
• assignment : une seule modalité permet d’atteindre l’état suivant (absence de choix)
• redundancy : les modalités sont utilisées de manière redondante pour atteindre l’état suivant (peut représenter la confirmation d’un choix dans une modalité par une autre modalité)
• equivalence : les modalités sont équivalentes pour atteindre l’état suivant (choix écrit ou oral de la même phrase par exemple)
La norme ISO 9241-11 [115] définit l’utilisabilité comme « la mesure dans la-quelle un produit peut être utilisé par des utilisateurs spécifiés pour atteindre des objectifs spécifiés avec eﬃcacité, performance et satisfaction dans un contexte d’uti-lisation spécifié ».
Exemple. Il est possible d’améliorer l’utilisabilité d’une fenêtre « accepter/refuser » en ajoutant des symboles liés aux deux notions, tels que pour accepter et × pour refuser.

Propriétés liées à la scène graphique

Au niveau de la représentation graphique des données ou de l’état du système, Hjelmslev [70] donne deux plans permettant de définir un élément graphique et l’information qu’il contient. Cette information appartient au plan du contenu, aussi appelé plan des signifiés. L’élément graphique appartient au plan de l’expression ou plan des signifiants. Le signifiant peut être caractérisé par des paramètres associés à des éléments graphiques.
Bertin et Barbut [26] ont présenté des variables visuelles pour définir les éléments graphiques et les informations qu’ils représentent. Pour eux, un élément graphique peut être défini avec ses coordonnées, sa taille, sa valeur, son grain, sa couleur, son orientation et sa forme. Wilkinson [125] a ajouté la notion d’opacité à ces variables. Jacques Bertin, qui était cartographe, portait son intérêt principalement sur les éléments graphiques placés sur une feuille de papier. De ce fait, les coordonnées étudiées se limitaient au plan (x, y). Dans le cas des systèmes informatiques où les interfaces humain-machine ont un aﬃchage dynamique, il faut également ajouter la Beckert et Beuster [19] donnent deux définitions de l’intégrité. La première est générique aux systèmes qui peuvent être exposés à des menaces et explique que les hypothèses de l’utilisateur sur l’application sont correctes et que l’inverse est égale-ment vrai. La seconde est spécifique aux interfaces utilisateur et explique qu’il existe une correspondance entre les hypothèses de l’utilisateur concernant l’état et les don-nées de l’application et sa configuration. Ils précisent cette deuxième propriété en expliquant la nécessité pour l’utilisateur, lorsqu’il eﬀectue une tâche critique, d’avoir des hypothèses sur les propriétés critiques du système identiques à ses propriétés réelles.
La propriété d’intégrité indique donc que les hypothèses de l’utilisateur concer-nant l’application sont correctes et l’inverse est également vrai.
Exemple. Lorsque nous nous connectons à des interfaces avec deux champs de texte, l’inversion du champ nom d’utilisateur et du champ mot de passe est un défaut d’intégrité.

Table des matières

1 Introduction
1.1 Systèmes informatiques interactifs
1.1.1 Définition
1.1.2 Les systèmes informatiques interactifs critiques
1.2 Vérification formelle
1.3 Questions de recherche
1.3.1 Comment formaliser les éléments de la scène graphique des interfaces humain-machine ?
1.3.2 Comment mécaniser la vérification des exigences graphiques des systèmes informatiques interactifs ?
1.4 Plan du manuscrit
2 Concepts de base 1
2.1 Paradigmes de programmation
2.1.1 Paradigme impératif
2.1.2 Paradigme fonctionnel
2.1.3 Paradigme objet
2.1.4 Paradigme réactif
2.1.5 Synthèse
2.2 Propriétés liées à l’interaction
2.2.1 Comportement de l’utilisateur
2.2.2 Principes cognitifs
2.2.3 Interfaces humain-machine
2.2.4 Sécurité
2.2.5 Modélisation des systèmes interactifs
2.2.6 Synthèse
2.3 Nomenclature des formalismes
2.3.1 Algèbre de processus
2.3.2 Langage de spécification
2.3.3 Processus de raffinement
2.3.4 Système de transition d’états
2.3.5 Logique temporelle
2.3.6 Synthèse
2.4 Synthèse
3 État de l’art
3.1 Objectif de ce chapitre
3.2 Revue de la littérature
3.2.1 Méthodologie
3.2.2 Propriétés liées au comportement de l’utilisateur
3.2.3 Propriétés liées aux principes cognitifs
3.2.4 Propriétés liées aux interfaces humain-machine
3.2.5 Propriétés liées à la sécurité
3.2.6 Modélisation des systèmes interactifs
3.2.7 Synthèse
3.3 Analyse de la littérature
3.3.1 Grande proportion de travaux sur la modélisation des systèmes
3.3.2 Utilisation privilégiée de certains formalismes
3.3.3 Émergence de nouveaux formalismes « ad hoc »
3.3.4 Maturité des cas d’étude
3.3.5 Propriétés de la scène graphique peu étudiées
3.4 Problématique abordée par cette thèse
3.4.1 Comment formaliser les éléments de la scène graphique des interfaces humain-machine ?
3.4.2 Comment mécaniser la vérification des exigences graphiques des systèmes informatiques interactifs ?
4 Cas d’étude : Smala et TCAS
4.1 Contexte des travaux de thèse
4.2 Smala
4.2.1 Gestion du contrôle
4.2.2 Composants graphiques
4.2.3 Graphe d’activation
4.2.4 Lien entre composants graphiques et graphe d’activation
4.3 TCAS
4.3.1 Données d’entrée de l’interface
4.3.2 Exemple de scénario : Approche frontale
4.3.3 Exigences graphiques du TCAS
4.4 Synthèse
5 Vérification des propriétés graphiques
5.1 Processus de vérification
5.1.1 Processus de vérification complet
5.1.2 Présentation des actions du processus de vérification
5.2 Formalisme
5.2.1 Définitions préalables
5.2.2 Opérateurs graphiques
5.3 Algorithme de vérification
5.3.1 Définitions préalables
5.3.2 Algorithme
5.4 GPCheck : Implémentation de l’algorithme
5.4.1 Définition de la structure des noeuds du graphe de scène enrichi
5.4.2 smax_to_node : Génération des données d’entrée de Smala
5.4.3 fgp_to_node : Génération des données d’entrée des propriétés graphiques
5.4.4 node_to_java : Génération des données d’entrée finales
5.4.5 find_proof : implémentation de l’algorithme
5.5 Synthèse
6 GPCheck : Application au TCAS
6.1 Rappels sur le TCAS
6.1.1 Données d’entrée de l’interface
6.1.2 Exigences graphiques du TCAS
6.2 GPCheck : Application au TCAS
6.3 Exigence E1 : Propre position relative
6.3.1 Formalisation de l’exigence graphique
6.3.2 Vérification de l’exigence
6.3.3 Visualisation du résultat de la vérification
6.4 Exigence E2 : Portée de 2 NM autour de own aircraft
6.4.1 Formalisation de l’exigence graphique
6.4.2 Vérification de l’exigence
6.5 Exigence E3 : TA – Trafic de type threat aircraft
6.5.1 Formalisation de l’exigence graphique
6.5.2 Vérification de l’exigence
6.5.3 Visualisation du résultat de la vérification
6.6 Exigence E4 : TA – Trafic de type intruder aircraft
6.6.1 Formalisation de l’exigence graphique
6.6.2 Vérification de l’exigence
6.6.3 Visualisation du résultat de la vérification
6.7 Exigence E5 : TA – Trafic de type proximate aircraft
6.7.1 Formalisation de l’exigence graphique
6.7.2 Vérification de l’exigence
6.7.3 Visualisation du résultat de la vérification
6.8 Exigence E6 : TA – Trafic de type other aircraft
6.8.1 Formalisation de l’exigence graphique
6.8.2 Vérification de l’exigence
6.8.3 Visualisation du résultat de la vérification
6.9 Exigence E7 : TA – Altitude relative
6.9.1 Formalisation de l’exigence graphique
6.9.2 Vérification de l’exigence
6.9.3 Visualisation du résultat de la vérification
6.10 Exigence E8 : TA – Sens vertical
6.10.1 Formalisation de l’exigence graphique
6.10.2 Vérification de l’exigence
6.10.3 Visualisation du résultat de la vérification
6.11 Synthèse
7 Conclusion et discussion
7.1 Bilan des contributions de la thèse
7.1.1 Classification des propriétés liées à l’interaction
7.1.2 Vérification formelle des propriétés liées à l’interaction
7.1.3 Développement d’un formalisme dédié à la scène graphique
7.1.4 Développement d’un algorithme de vérification des propriétés graphiques
7.1.5 Développement de GPCheck, implémentation de l’algorithme de vérification
7.1.6 Vérification des exigences graphiques du TCAS
7.2 Discussion
7.2.1 Formalisme de Randell et al. [96]
7.2.2 Couverture de l’analyse
7.2.3 Adressage de la perception utilisateur
7.2.4 Dépendance à Smala
7.2.5 Utilisabilité de GPCheck
7.3 Perspectives
7.3.1 Formalisme de Randell et al. [96]
7.3.2 Couverture de l’analyse
7.3.3 Adressage de la perception utilisateur
7.3.4 Dépendance à Smala
7.3.5 Utilisabilité de GPCheck