Geekly articles weekly

Application des méthodes formelles de validation des modèles pour l'interface utilisateur

Bonjour, Habr! Je vous présente la traduction de l'article «FORMALEMENT SPÉCIFIANT UIS» par Hillel Wayne.


De l'auteur


Relativement récemment, je suis tombé sur un article sur les méthodes d'ingénierie dans le développement de logiciels , où vasil-sd a parlé de la validation formelle des spécifications des produits logiciels en cours de création. L'alliage a été utilisé comme boîte à outils. L'un des principaux leitmotivs dans les commentaires était d'analyser l'article dans le contexte d'un projet Web moderne, car il est coûteux \ long \ difficile d'utiliser des méthodes formelles où tout le monde le fait rapidement / à moindre coût. Étant donné que l'auteur a fait référence au blog Hillel Wayne, où de tels exemples se trouvaient, j'ai décidé de traduire certains de ses articles comme ajout au texte principal de vasil-sd

Attention :

  • Tout ce que l'auteur appelle une machine à états finis, j'appellerai une machine à états ou un modèle de machine à états.
  • J'ai appris une partie de la terminologie d'un article que j'ai mentionné plus tôt sur une approche d'ingénierie du développement. Néanmoins, le sujet pour moi est relativement nouveau, car les deux auteurs (étrangers ou non) pourraient ne pas comprendre - ne jurez pas.

Spécification de l'interface utilisateur formelle


Une bonne interface utilisateur est essentielle pour créer le bon logiciel. Et si les utilisateurs ont des problèmes à utiliser le programme, ils sont susceptibles de faire quelque chose de mal. Je préfère ne pas travailler sur l'interface utilisateur - je ne me considère pas au-dessus de cela, mais ce n'est pas le mien. Les effets visuels et les interfaces me préoccupent, et les gens qui sont capables de faire face à tout cela me font un respect fou.

J'adore les méthodes formelles. Mon ami Kevin Lynagh a récemment publié sketch.systems 1 , un nouvel outil de spécification formel pour les concepteurs d'interface utilisateur. Eh bien, découvrons - mon amour des méthodes formelles peut-il surmonter ma peur?

Le problème


De retour à Edmodo, je travaillais sur une interface utilisateur pour notre application Snapshot. C'était notre première deuxième tentative de gagner de l'argent: nous avons commencé par offrir à tous les enseignants un programme gratuit, puis demander des dons ou quelque chose comme ça. Comme vous pouvez le voir, Edmodo ne différait pas beaucoup de sens des affaires. 2

Chez Snapshot, les enseignants peuvent effectuer des «sondages» ou des «snaps» auprès des élèves. De plus, le programme regroupe les résultats de l'enquête et fournit aux enseignants plusieurs rapports en temps réel dans les sections suivantes: rapport «résumé», «par les élèves» et «selon les normes». De plus, nous avons décidé que le programme devrait avoir un rapport «réponses» qui pourrait être ouvert à partir du rapport «étudiants» et qui fournirait des informations sur les réponses incorrectes.

NOUS avons imaginé que l'utilisateur se déplace entre les rapports en appuyant sur les boutons nécessaires, et que tous les rapports devraient être accessibles à partir d'autres rapports, à l'exception des réponses. Le sens du mot «disponible» dans le contexte des transitions est assez vague: il peut signifier «vous pouvez en quelque sorte accéder au rapport», ou il peut signifier «en un clic aller directement au rapport souhaité». Tout ce qui est décrit ci-dessus n'est qu'une partie de la l'interface de l'ensemble de l'application qui, en plus de la navigation dans les rapports, possède son propre système de navigation.

Lorsque le système commence à devenir plus compliqué, nous devons être prudents. Cela signifie écrire une spécification. Alors, comment pouvons-nous spécifier cela? Je vois que l'enseignant peut être sur un écran spécifique de l'application et peut prendre des mesures pour passer à un autre écran. Cela m'amène à l'idée que nous pouvons considérer les actions de l'enseignant comme une machine à états finis.

Machines d'état


Les machines à états finis (FSM) sont l'un des modèles mathématiques les plus simples de la théorie des automates abstraits. Vous disposez d'un ensemble fini d'états, d'un ensemble de transitions entre états et d'un ensemble d'événements (déclencheurs) qui déclenchent des transitions. Chaque transition est liée à un événement, donc si l'événement se produit, l'état peut changer. 3 Dans notre modèle, les événements seront «l'enseignant appuie sur les boutons». Voici un modèle de machine d'état pour notre système actuel:


Le modèle présente deux problèmes avec notre interface utilisateur. Tout d'abord, toutes les machines à états finis ont besoin d'un état initial, mais nous ne l'avons pas. Lorsqu'un enseignant visite la page des rapports, quel rapport doit-il voir en premier? Deuxièmement, nous n'indiquons pas ce qui se passe lorsque vous cliquez sur le bouton du rapport que vous consultez déjà. Ceci est ambigu, car il existe plusieurs comportements:

  1. Si vous êtes dans un rapport de synthèse, le bouton de synthèse n'apparaît pas ou ne fait rien.
  2. Si vous êtes dans un rapport de synthèse, le bouton de résumé réinitialise le rapport.

Nous avons choisi la deuxième option. Notre état initial était un rapport «résumé». Modèle mis à jour:


Le modèle transmet très précisément notre interface utilisateur - il est également encombré. Il s'agit là d'une limitation importante du modèle de machine à états finis: plus il y a de transitions entre états, plus il est difficile de les percevoir. Dans notre cas, à partir de presque tous les rapports, il était possible de passer à un autre rapport.

La poursuite du développement du système et de sa modélisation devient problématique. Parce que, par exemple, si nous prenons en compte qu'à tout moment, l'enseignant peut se déconnecter du système, le prochain modèle de la machine d'état ressemblera déjà à ceci:


Pour ajouter la fonction de déconnexion, nous avons dû ajouter quatre bords supplémentaires. La poursuite du développement des spécifications avec cette approche cesse rapidement d'être valable. Nous avons besoin d'un moyen de représenter les transitions «générales». Pour cela, nous pouvons utiliser des états imbriqués, ce qui compliquera notre formalisme, mais simplifiera nos spécifications.

Tableaux de statut Harel


La plupart de nos États ont une logique commune du soi-disant super-État: nos quatre «rapports» ont tous la même logique pour se déconnecter du système, et les trois principaux ont les mêmes transitions. Si nous pouvons les regrouper dans un rapport «état parental», il ne nous reste plus qu'à déterminer la transition vers la «sortie» et à répartir cette transition dans les états enfants. La logique est similaire à l'héritage: les états enfants héritent (ou remplacent) les transitions des états parents.

Les machines à états finis avec des états imbriqués sont appelées machines à états hiérarchiques et il existe plusieurs façons de les formaliser. La manière la plus appropriée d'écrire des modèles de machines d'état pour une interface utilisateur est le Harel Statechart. 4 Les règles pour elle sont les suivantes:

  1. Tous les états parentaux sont abstraits. Chaque état parent doit définir un état enfant par défaut.
  2. Les états enfants héritent automatiquement de toutes les transitions parentales, mais peuvent également les remplacer.
  3. Une transition peut indiquer n'importe quel état. Si vous passez à l'état parent, passez plutôt à son état enfant par défaut. Si l'état enfant est également parent, l'état est déterminé de manière récursive.

Vous pouvez développer des graphiques d'état Harel dans Graphviz et vous horrifier à chaque fois des nombreux sommets, bords et délices des graphiques graphiques. Nous utiliserons l'interface utilisateur beaucoup plus agréable de Sketch.systems:

Snapshot logout -> Login Page Reports summary -> Summary students -> Students standards -> Standards Summary* Students answer -> Answers Standards Answers close -> Students Login Page login -> Snapshot


source

Je recommanderais de suivre le lien vers le diagramme, car elle est interactive. Vous pouvez cliquer sur les transitions et voir comment les états changent. C'est un grand avantage du diagramme d'état de Harkel: ils sont non seulement formels et concis, mais aussi cinétiques. Vous pouvez les rechercher.

En étudiant le tableau, j'ai trouvé une erreur: vous pouvez passer directement des «réponses» aux «normes». Cela peut être résolu en faisant des «réponses» un descendant direct de l '«entrée» plutôt que des «rapports»:


source

Idéalement, il serait bien de voir clairement ces problèmes sur le diagramme, ce qui implique une certaine automatisation de la vérification du modèle.

Vérifier


Une spécification formelle présente deux avantages. L'une d'elles est implicite: les travaux de formalisation conduisent à une meilleure compréhension du système. L'autre est explicite: si nous avons une spécification formelle, nous pouvons vérifier ses propriétés. Notre interface utilisateur a-t-elle des blocages? Existe-t-il des transitions implicites ou incorrectement spécifiées?

Sketch.systems peut vérifier si le diagramme d'état Harel a le format correct, mais ne peut pas vérifier le comportement du modèle. Il existe d'autres outils pour déterminer l'état d'une machine à états, en particulier les diagrammes d'état UML, mais tous sont orientés vers les spécifications au niveau du code et non vers les spécifications au niveau du système. Leur objectif est de générer à terme un code C ou Java à partir d'un diagramme d'état. Mais ils sont trop bas pour tester les propriétés abstraites, et nous sommes trop haut pour vouloir générer du code. Si nous voulons un test formalisé, nous devrons décrire notre modèle dans un langage de spécification à usage général.

Heureusement, pour ce cas, c'est assez facile à faire. Pour cela, nous utiliserons l'alliage, car il peut refléter le plus fidèlement la structure du diagramme d'état Harel. 5 Nous pouvons utiliser des extensions de signature pour représenter des états imbriqués: «Standards» étendre «Reports» signifie que chaque élément de «Standards» est également un «Report», ce qui équivaut à la déclaration selon laquelle il s'agit d'un état enfant dans le diagramme de Harel correspondant. Cela simplifie la définition des transitions. Chacun d'eux est représenté par un seul prédicat qui prend le temps (t), l'état initial (début) et l'état final (fin), et déclare que l'état au temps t va du début à la fin pour t.next. Malgré le fait que les états parents sont abstraits, nous pouvons toujours les utiliser comme point de départ et profiter des transitions parentales.

 open util/ordering[Time] sig Time { state: one State } abstract sig State {} abstract sig Login extends State {} abstract sig Reports extends Login {} one sig Logout extends State {} one sig Students, Summary, Standards extends Reports {} one sig Answers extends Login {} pred transition[t: Time, start: State, end: State] { t.state in start t.next.state in end } pred logout[t: Time] { transition[t, Login, Logout] } pred login[t: Time] { transition[t, Logout, Summary] } pred students[t: Time] { transition[t, Reports, Students] } pred summary[t: Time] { transition[t, Reports, Summary] } pred standards[t: Time] { transition[t, Reports, Standards] } pred answers[t: Time] { transition[t, Students, Answers] } pred close_answers[t: Time] { transition[t, Answers, Students] } fact Trace { first.state = Summary all t: Time - last | logout[t] or login[t] or students[t] or summary[t] or standards[t] or answers[t] or close_answers[t] }

Nous pouvons maintenant vérifier les propriétés de notre modèle. Par exemple, est-il possible d'obtenir le rapport «réponses» sans passer par le rapport «étudiants»?

 check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7 // valid

Nous pouvons également simuler un exemple lorsque quelqu'un se déconnecte et se reconnecte:

 run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7

L'alliage fournit une gamme assez large de spécifications. Avec la vérification de certaines propriétés, par exemple tupiokov, des difficultés peuvent survenir. Cependant, je ne suis pas la première personne à voir à quel point Alloy fonctionne avec les diagrammes d'état. Le professeur Nancy Day a récemment annoncé une variante en alliage appelée DASH, qui ajoute la sémantique de première classe des diagrammes Harel à Alloy. Vous pouvez en lire plus ici .

Valeur


Est-ce que tout cela a de la valeur? Qu'est-ce qui rend un diagramme d'état interactif meilleur que de simples notes en anglais? Certainement, un digramme devient plus précieux lorsque vous évoluez. Je me souviens que dans le projet Snapshot, il y avait environ deux douzaines d'écrans d'enseignants imbriqués dans plusieurs grandes hiérarchies. Sans spécification formelle, nous n'avons pas pu tester notre travail. Pour autant que je m'en souvienne, certaines des erreurs que nous avons commises:

  • Nous avons oublié de considérer la «clôture du rapport de réponse» comme un événement et les «réponses» sont devenues une impasse
  • La création d'une nouvelle enquête avait un tas de routes de comté dont nous n'avons vraiment pas besoin.
  • Nous n'avons pas déterminé le comportement de l'interface utilisateur après la création de l'enquête, nous avons donc renvoyé l'enseignant à l'écran de création de l'enquête, il a pensé que lors de l'erreur l'enquête n'a pas été créée et l'a recréée
  • Il était difficile d'accéder à plusieurs écrans, donc personne n'y est jamais allé.

Je pense qu'avoir une spécification formelle aiderait beaucoup. L'écriture de l'exemple que j'ai fait ci-dessus a pris environ cinq minutes à écrire, et la spécification de l'application complète prendrait moins de deux heures. Si, même au stade de la conception, cela nous aidait à trouver au moins une des erreurs répertoriées, nous gagnerions beaucoup de temps plus tard.

Conclusion


Nous avons discuté de la spécification formelle de l'interaction de l'utilisateur avec l'interface utilisateur. Mon amour des méthodes formelles peut-il surmonter ma peur de l'assurance-chômage? Mon Dieu non. Si vous avez suivi les liens vers Sketch.systems, vous avez probablement vu que vous pouvez attacher un prototype en Javascript à votre diagramme d'état. C'est magique!

Malgré ma peur, je pense qu'il y a un certain potentiel dans les méthodes formelles. Les gens les considèrent généralement comme des choses purement académiques utilisées exclusivement par la NASA. Le thème principal de ce blog est que les méthodes formelles sont de puissants outils pour le travail quotidien. Je considère principalement leur application au backend et aux systèmes parallèles, car je l'apprécie. Mais leur utilisation ne se limite pas à mes préférences. Les méthodes formelles sont particulièrement importantes pour l'interface utilisateur. Je ne pense pas que les diagrammes d'état de Harel soient de loin la meilleure notation possible, mais c'est une bonne première étape.

Au fait, hé, je donne des conseils sur les méthodes formelles . Dites à votre patron!


  1. Attention, j'étais l'un des testrovers alpha. La plupart de mes commentaires étaient du genre «tu devrais rendre les choses plus compliquées!». Oui, je suis un testeur alpha. [retour]
  2. En 2017, ils ont gagné 1 million et perdu 20 millions. [retour]
  3. Une machine à états finis a beaucoup en commun avec une machine à états finis déterministe, qui est une composante importante de l'informatique. La principale différence dans le domaine d'application: l'utilisation d'une machine à états finis déterministe est justifiée par «l'ensemble des langages réguliers qu'il reconnaît», l'utilisation de la machine à états finis par «cohérence des spécifications» [retour]
  4. Le principal concurrent est le diagramme d'état UML, qui représente essentiellement le diagramme d'état Harer, en complément de ses spécifications de code. Il est plus expressif, mais difficile à analyser. [retour]
  5. Si vous n'êtes pas familier avec Alloy, j'ai écrit plusieurs articles dessus ici et ici .

Source: https://habr.com/ru/post/fr469379/

More articles:


All Articles