Anwendung formaler Modellvalidierungsmethoden für die Benutzeroberfläche

Hallo Habr! Ich präsentiere Ihnen die Übersetzung des Artikels „FORMAL SPECIFYING UIS“ von Hillel Wayne.

Vom Autor

Vor relativ kurzer Zeit stieß ich auf einen Artikel über technische Methoden in der Softwareentwicklung , in dem vasil-sd über die formale Validierung von Spezifikationen für Softwareprodukte sprach, die erstellt werden. Legierung wurde als Toolkit verwendet. Eines der wichtigsten Leitmotive in den Kommentaren war das Parsen des Artikels im Kontext eines modernen Webprojekts, da es teuer und schwierig ist, formale Methoden zu verwenden, bei denen jeder dies schnell / billig tut. Da der Autor auf den Hillel Wayne-Blog verwies, in dem sich solche Beispiele befanden, beschloss ich, einige seiner Artikel als Ergänzung zum Haupttext von vasil-sd zu übersetzen

Warnung :

• Alles, was der Autor eine endliche Zustandsmaschine nennt, werde ich eine Zustandsmaschine oder ein Modell einer Zustandsmaschine nennen.
• Ich habe einen Teil der Terminologie aus einem Artikel gelernt, den ich zuvor über einen technischen Entwicklungsansatz erwähnt habe. Trotzdem ist das Thema für mich relativ neu, weil beide Autoren (sowohl ausländische als auch nicht so) dies nicht verstehen konnten - schwören Sie nicht.

Formale UI-Spezifikation

Eine gute Benutzeroberfläche ist für die Erstellung der richtigen Software unerlässlich. Und wenn Benutzer Probleme mit der Verwendung des Programms haben, machen sie wahrscheinlich etwas falsch. Ich ziehe es vor, nicht an der Benutzeroberfläche zu arbeiten - ich betrachte mich nicht darüber, aber es ist "nicht meins". Die visuellen Effekte und Schnittstellen machen mir Sorgen, und Leute, die mit all dem fertig werden, machen mir verrückten Respekt.

Ich liebe formale Methoden. Mein Freund Kevin Lynagh hat kürzlich scale.systems veröffentlicht ¹ , ein neues formales Spezifikationstool für UI-Designer. Nun, lassen Sie uns herausfinden - kann meine Liebe zu formalen Methoden meine Angst überwinden?

Das Problem

Zurück in Edmodo arbeitete ich an einer Benutzeroberfläche für unsere Snapshot-Anwendung. Dies war unser erster zweiter Versuch, Geld zu verdienen: Wir gaben zunächst allen Lehrern ein kostenloses Programm und baten dann um Spenden oder ähnliches. Wie Sie sehen können, unterschied sich Edmodo nicht wesentlich vom Geschäftssinn. ²

Bei Snapshot können Lehrer „Umfragen“ oder „Schnappschüsse“ unter Schülern durchführen. Darüber hinaus fasst das Programm die Umfrageergebnisse zusammen und bietet Lehrern in den folgenden Abschnitten mehrere Echtzeitberichte: Bericht „Zusammenfassung“, „nach Schülern“ und „nach Standards“. Darüber hinaus haben wir beschlossen, dass das Programm einen Bericht mit „Antworten“ enthält, der aus dem Bericht „Schüler“ geöffnet werden kann und Informationen zu falschen Antworten enthält.

Wir stellten uns vor, dass der Benutzer durch Drücken der erforderlichen Schaltflächen zwischen Berichten wechselt und dass alle Berichte mit Ausnahme der Antworten von anderen Berichten aus zugänglich sein sollten. Die Bedeutung des Wortes "verfügbar" im Zusammenhang mit Übergängen ist eher vage: Es kann bedeuten, dass Sie irgendwie zum Bericht gehen können, oder es kann bedeuten, dass Sie mit einem Klick direkt zum gewünschten Bericht gehen. Alles, was oben beschrieben wurde, ist nur ein Teil des Benutzers Die Schnittstelle der gesamten Anwendung, die neben der Navigation in Berichten über ein eigenes Navigationssystem verfügt.

Wenn das System komplizierter wird, müssen wir vorsichtig sein. Dies bedeutet, eine Spezifikation zu schreiben. Wie können wir das spezifizieren? Ich sehe, dass sich der Lehrer auf einem bestimmten Bildschirm der Anwendung befinden und Maßnahmen ergreifen kann, um zu einem anderen Bildschirm zu wechseln. Dies führt mich zu der Idee, dass wir die Handlungen des Lehrers als eine endliche Zustandsmaschine betrachten können.

Zustandsautomaten

Finite-State-Maschinen (FSMs) sind eines der einfachsten mathematischen Modelle der Theorie abstrakter Automaten. Sie haben eine endliche Menge von Zuständen, eine Reihe von Übergängen zwischen Zuständen und eine Reihe von Ereignissen (Triggern), die Übergänge auslösen. Jeder Übergang ist an ein Ereignis gebunden. Wenn das Ereignis eintritt, kann sich der Status ändern. ³ In unserem Modell sind die Ereignisse "Der Lehrer drückt die Tasten". Das Folgende ist ein Zustandsmaschinenmodell für unser aktuelles System:


Das Modell zeigt zwei Probleme mit unserer Benutzeroberfläche. Erstens benötigen alle endlichen Zustandsmaschinen einen Anfangszustand, den wir jedoch nicht haben. Welchen Bericht sollte ein Lehrer zuerst sehen, wenn er die Berichtsseite besucht? Zweitens geben wir nicht an, was passiert, wenn Sie auf die Schaltfläche des Berichts klicken, den Sie bereits anzeigen. Dies ist nicht eindeutig, da es verschiedene Verhaltensweisen gibt:

1. Wenn Sie sich in einem Zusammenfassungsbericht befinden, wird die Schaltfläche "Zusammenfassung" nicht angezeigt oder führt nichts aus.
2. Wenn Sie sich in einem Zusammenfassungsbericht befinden, wird der Bericht über die Schaltfläche "Zusammenfassung" zurückgesetzt.

Wir haben die zweite Option gewählt. Unser Ausgangszustand war ein "zusammenfassender" Bericht. Aktualisiertes Modell:


Das Modell vermittelt sehr genau unsere Benutzeroberfläche - es ist auch überladen. Dies ist eine wesentliche Einschränkung des Modells der endlichen Zustandsmaschine: Je mehr Übergänge zwischen Zuständen auftreten, desto schwieriger ist es, sie wahrzunehmen. In unserem Fall war es von fast jedem Bericht möglich, zu einem anderen Bericht zu wechseln.

Die Weiterentwicklung des Systems und seine Modellierung wird problematisch. Wenn wir zum Beispiel berücksichtigen, dass sich der Lehrer jederzeit vom System abmelden kann, sieht das nächste Modell der Zustandsmaschine bereits ungefähr so ​​aus:


Um die Abmeldefunktion hinzuzufügen, mussten wir vier weitere Kanten hinzufügen. Die weitere Entwicklung von Spezifikationen mit diesem Ansatz hört schnell auf, solide zu sein. Wir brauchen eine Möglichkeit, die „allgemeinen“ Übergänge darzustellen. Hierfür können wir verschachtelte Zustände verwenden, was unseren Formalismus kompliziert, aber unsere Spezifikationen vereinfacht.

Harel Status Charts

Die meisten unserer Zustände haben eine gemeinsame Logik des sogenannten Superzustands: Alle unsere vier „Berichte“ haben dieselbe Logik zum Abmelden vom System, und die drei Hauptzustände haben dieselben Übergänge. Wenn wir sie in einem Bericht über den „elterlichen Zustand“ zusammenfassen können, müssen wir nur noch den Übergang zum „Ausstieg“ bestimmen und diesen Übergang in untergeordneten Zuständen verteilen. Die Logik ähnelt der Vererbung: Untergeordnete Zustände erben (oder überschreiben) Übergänge von übergeordneten Zuständen.

Endliche Zustandsmaschinen mit verschachtelten Zuständen werden als hierarchische Zustandsmaschinen bezeichnet, und es gibt verschiedene Möglichkeiten, sie zu formalisieren. Die am besten geeignete Methode zum Schreiben von Zustandsmaschinenmodellen für eine Benutzeroberfläche ist das Harel Statechart. ^{4 Die} Regeln für sie lauten wie folgt:

1. Alle elterlichen Zustände sind abstrakt. Jeder übergeordnete Status muss einen untergeordneten Standardstatus definieren.
2. Untergeordnete Zustände erben automatisch alle übergeordneten Übergänge, können sie aber auch überschreiben.
3. Ein Übergang kann einen beliebigen Zustand anzeigen. Wenn Sie in den übergeordneten Status wechseln, wechseln Sie stattdessen in den untergeordneten Standardstatus. Wenn der untergeordnete Status auch ein übergeordneter Status ist, wird der Status rekursiv bestimmt.

Sie können Harel-Zustandsdiagramme in Graphviz entwickeln und sich jedes Mal über die vielen Eckpunkte, Kanten und Freuden grafischer Diagramme entsetzen. Wir werden die viel schönere Benutzeroberfläche von Sketch.systems verwenden:

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

_Quelle

Ich würde empfehlen, dem Link zum Diagramm zu folgen, als Sie ist interaktiv. Sie können auf die Übergänge klicken und sehen, wie sich die Zustände ändern. Dies ist ein großer Vorteil des Harkel-Zustandsdiagramms: Sie sind nicht nur formal und prägnant, sondern auch kinetisch. Sie können sie recherchieren.

Beim Studium der Tabelle habe ich einen Fehler festgestellt: Sie können direkt von den „Antworten“ zu den „Standards“ wechseln. Dies kann behoben werden, indem die "Antworten" direkt von den "Eingaben" und nicht von den "Berichten" abgeleitet werden:


_Quelle

Im Idealfall wäre es schön, solche Probleme im Diagramm deutlich zu sehen, was eine gewisse Automatisierung der Modellüberprüfung impliziert.

Überprüfen Sie

Eine formale Spezifikation hat zwei Vorteile. Eine davon ist implizit: Die Arbeit an der Formalisierung führt zu einem besseren Verständnis des Systems. Das andere ist explizit: Wenn wir eine formale Spezifikation haben, können wir deren Eigenschaften überprüfen. Hat unsere Benutzeroberfläche Deadlocks? Gibt es implizite oder falsch spezifizierte Übergänge?

Sketch.systems kann überprüfen, ob das Harel-Zustandsdiagramm das richtige Format hat, kann jedoch das Verhalten des Modells nicht überprüfen. Es gibt andere Werkzeuge zum Bestimmen des Zustands einer Zustandsmaschine, insbesondere UML-Zustandsdiagramme, aber alle konzentrieren sich auf Spezifikationen auf Codeebene und nicht auf Spezifikationen auf Systemebene. Ihr Ziel ist es, letztendlich C- oder Java-Code aus einem Zustandsdiagramm zu generieren. Sie sind jedoch zu niedrig, um abstrakte Eigenschaften zu testen, und wir sind zu hoch, um Code generieren zu wollen. Wenn wir einen formalisierten Test wünschen, müssen wir unser Modell in einer allgemeinen Spezifikationssprache beschreiben.

Glücklicherweise ist dies in diesem Fall recht einfach. Hierfür verwenden wir Alloy, da es die Struktur des Harel-Zustandsdiagramms am genauesten widerspiegeln kann. ⁵ Wir können Signaturerweiterungen verwenden, um verschachtelte Zustände darzustellen: "Standards" erweitern "Berichte" bedeutet, dass jedes Bit von "Standards" auch ein "Bericht" ist, was der Aussage entspricht, dass dies ein untergeordneter Zustand im entsprechenden Harel-Diagramm ist. Dies vereinfacht die Definition von Übergängen. Jedes von ihnen wird durch ein einzelnes Prädikat dargestellt, das Zeit (t), den Anfangszustand (Start) und den Endzustand (Ende) benötigt und erklärt, dass der Zustand zum Zeitpunkt t für t.next von Anfang bis Ende geht. Trotz der Tatsache, dass übergeordnete Zustände abstrakt sind, können wir sie dennoch als Start verwenden und übergeordnete Übergänge nutzen.

 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] } 

Jetzt können wir die Eigenschaften unseres Modells überprüfen. Ist es beispielsweise möglich, den Bericht „Antworten“ abzurufen, ohne den Bericht „Schüler“ durchzugehen?

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

Wir können auch ein Beispiel simulieren, wenn sich jemand abmeldet und erneut anmeldet:

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

Legierung bietet eine ziemlich breite Palette von Spezifikationen. Bei der Überprüfung bestimmter Eigenschaften, beispielsweise Tupiokov, können Schwierigkeiten auftreten. Ich bin jedoch nicht der erste, der sieht, wie gut Alloy mit Zustandsdiagrammen arbeitet. Professor Nancy Day kündigte kürzlich eine Legierungsvariante namens DASH an, die Alloy die erstklassige Semantik von Harel-Diagrammen hinzufügt. Sie können hier darüber lesen.

Wert

Hat das alles Wert? Was macht ein interaktives Zustandsdiagramm besser als nur Notizen auf Englisch? Auf jeden Fall wird ein Digramm beim Skalieren wertvoller. Ich erinnere mich, dass es im Snapshot-Projekt ungefähr zwei Dutzend Lehrerbildschirme gab, die in mehreren großen Hierarchien verschachtelt waren. Ohne eine formale Spezifikation könnten wir unsere Arbeit nicht testen. Soweit ich mich erinnere, einige der Fehler, die wir gemacht haben:

• Wir haben vergessen, das „Schließen des Antwortberichts“ als Ereignis zu betrachten, und die „Antworten“ wurden zu einer Sackgasse
• Beim Erstellen einer neuen Umfrage gab es eine Reihe von County-Routen, die wir wirklich nicht benötigen.
• Wir haben das Verhalten der Benutzeroberfläche nach dem Erstellen der Umfrage nicht ermittelt. Daher haben wir den Lehrer zum Bildschirm zum Erstellen der Umfrage zurückgeführt. Er war der Ansicht, dass die Umfrage während des Fehlers nicht erstellt und neu erstellt wurde
• Es war schwierig, an mehrere Bildschirme zu gelangen, daher ging nie jemand zu ihnen.

Ich denke, eine formale Spezifikation würde viel helfen. Das Schreiben des oben erstellten Beispiels dauerte ungefähr fünf Minuten, und die Spezifikation für die vollständige Anwendung würde weniger als zwei Stunden dauern. Wenn uns dies bereits in der Entwurfsphase dabei helfen würde, mindestens einen der aufgeführten Fehler zu finden, würden wir später viel Zeit sparen.

Fazit

Wir haben die formale Spezifikation der Benutzerinteraktion mit der Benutzeroberfläche diskutiert. Kann meine Liebe zu formalen Methoden meine Angst vor der Benutzeroberfläche überwinden? Meine Güte, nein. Wenn Sie den Links zu Sketch.systems gefolgt sind, haben Sie wahrscheinlich gesehen, dass Sie Ihrem Statusdiagramm einen Prototyp in Javascript hinzufügen können. Das ist Magie!

Trotz meiner Angst denke ich, dass formale Methoden ein gewisses Potenzial haben. Die Leute betrachten sie normalerweise als rein akademische Dinge, die ausschließlich von der NASA verwendet werden. Das Hauptthema dieses Blogs ist, dass formale Methoden leistungsstarke Werkzeuge für die tägliche Arbeit sind. Ich betrachte ihre Anwendung hauptsächlich auf das Backend und parallele Systeme, weil es mir Spaß macht. Ihre Verwendung ist jedoch nicht nur auf meine Vorlieben beschränkt. Formale Methoden sind besonders wichtig für die Benutzeroberfläche. Ich denke nicht, dass Harels Zustandsdiagramme bei weitem die bestmögliche Notation sind, aber dies ist ein guter erster Schritt.

Übrigens, hey, ich rate zu formalen Methoden . Sag es deinem Chef!

---

1. Achtung, ich war einer der Alpha-Testrover. Die meisten meiner Rückmeldungen lauteten: "Sie sollten es komplizierter machen!". Ja, ich bin ein mittelmäßiger Alpha-Tester. ^[zurück]
2. Im Jahr 2017 haben sie 1 Million gewonnen und 20 Millionen verloren. ^[zurück]
3. Eine endliche Zustandsmaschine hat viel mit einer deterministischen endlichen Zustandsmaschine gemeinsam, die ein wichtiger Bestandteil der Informatik ist. Der Hauptunterschied im Anwendungsbereich: Die Verwendung einer deterministischen endlichen Zustandsmaschine wird durch die "Menge der von ihr erkannten regulären Sprachen" gerechtfertigt, die Verwendung der endlichen Zustandsmaschine durch "Spezifikationskonsistenz" ^[return]
4. Der Hauptkonkurrent ist das UML-Zustandsdiagramm, das im Wesentlichen das Harer-Zustandsdiagramm darstellt und durch seine Codespezifikationen ergänzt wird. Es ist aussagekräftiger, aber schwer zu analysieren. ^[zurück]
5. Wenn Sie mit Alloy nicht vertraut sind, habe ich hier und hier mehrere Artikel darüber geschrieben.