Application of formal model validation methods for UI
Hello, Habr! I present to you the translation of the article “FORMALLY SPECIFYING UIS” by Hillel Wayne.
Relatively recently, I came across an article about Engineering methods in software development , where vasil-sd talked about the formal validation of specifications for software products being created. Alloy was used as a toolkit. One of the main leitmotifs in the comments was to parse the article in the context of some modern web project, because it’s expensive \ long \ difficult to use formal methods where everyone does it quickly / cheaply. Since the author referred to the Hillel Wayne blog, where such examples were, I decided to translate some of his articles as an addition to the main text of vasil-sd
Warning :
A good user interface is essential for creating the right software. And if users have problems using the program, they are likely to do something wrong. I prefer not to work on the user interface - I do not consider myself superior to this, but it is “not mine”. The visual effects and interfaces cause me concern, and people who are able to cope with all this, cause me crazy respect.
I love formal methods. My friend Kevin Lynagh recently released sketch.systems 1 , a new formal specification tool for UI designers. Well, let's find out - can my love of formal methods overcome my fear?
Back in Edmodo, I was working on a user interface for our Snapshot application. This was ourfirst second attempt to make money: we started by giving all teachers a free program, and then asking for donations or something like that. As you can see, then Edmodo did not differ much business acumen. 2
In Snapshot, teachers can conduct “polls” or “snaps” among students. Further, the program aggregates survey results and provides teachers with several real-time reports in the following sections: “summary” report, “by students” and “by standards”. In addition, we decided that the program should have a “answers” report that could be opened from the “students” report and which provided information about incorrect answers.
WE imagined that the user moves between reports by pressing the necessary buttons, and that all reports should be accessible from other reports, with the exception of answers. The meaning of the word “available” in the context of transitions is rather vague: it may mean “you can somehow go to the report”, or it can mean “one-click go directly to the desired report.” Everything described above is only part of the user’s the interface of the entire application, which, in addition to navigation in reports, has its own navigation system.
When the system starts to get more complicated, we need to be careful. This means writing a specification. So how can we specify this? I see that the teacher can be on a certain screen of the application and can take actions to move to another screen. This leads me to the idea that we can consider the actions of the teacher as a finite state machine.
Finite state machines (FSM) is one of the simplest mathematical models of the theory of abstract automata. You have a finite set of states, a set of transitions between states, and a set of events (triggers) that trigger transitions. Each transition is tied to an event, so if the event occurs, the state may change. 3 In our model, the events are “the teacher presses the buttons.” The following is a state machine model for our current system:
The model shows two problems with our user interface. First, all state machines need an initial state, but we don’t have it. When a teacher visits the reports page, which report should he see first? Secondly, we do not indicate what happens when you click the button of the report that you are already viewing. This is ambiguous, as there are several behaviors:
We chose the second option. Our initial state was a “summary" report. Updated model:
The model very accurately conveys our user interface - it is also cluttered. This is a significant limitation of the finite state machine model: the more transitions between states, the more difficult it is to perceive them. In our case, from almost every report it was possible to switch to another report.
Further development of the system and its modeling becomes problematic. Because, for example, if we take into account that at any moment the teacher could exit the system, then the next model of the state machine will already look something like this:
To add the logout function, we had to add four more ribs. Further development of the specification with this approach quickly ceases to be sound. We need some way to represent the “general” transitions. For this, we can use nested states, which will complicate our formalism, but simplify our specifications.
Most of our states have a common logic of the so-called super-state: all four of our “reports” have the same logic for logging out of the system, and the main three have the same transitions. If we can group them into a “parental state” report, all that remains for us is to determine the transition to “exit” and distribute this transition in child states. The logic is similar to inheritance: child states inherit (or redefine) transitions of parent states.
Finite state machines with nested states are called hierarchical state machines, and there are several different ways to formalize them. The most suitable way to write state machine models for a UI is the Harel Statechart. 4 The rules for her are as follows:
You can design Harel State Charts in Graphviz and get horrified at the many vertices, edges, and delights of graphing graphs each time. We will use the much nicer user interface from Sketch.systems:
source
I would recommend following the link to the diagram, as she is interactive. You can click on the transitions and see how the states change. This is a great advantage of the Harkel State Diagram: they are not only formal and concise, but also kinetic. You can research them.
While studying the chart, I found a mistake: you can go directly from the “answers” to the “standards”. This can be fixed by making the “answers” a direct descendant of the “input” rather than the “reports”:
source
Ideally, it would be nice to clearly see such problems on the diagram, which implies some automation of the model verification.
A formal specification has two advantages. One of them is implicit: work on formalization leads to a better understanding of the system. The other is explicit: if we have a formal specification, we can check its properties. Does our user interface have any deadlocks? Are there implicit or incorrectly specified transitions?
Sketch.systems can check if the Harel State Diagram has the correct format, but cannot check the behavior of the model. There are other tools for determining state of a state machine, in particular, UML state diagrams, but all of them are focused on code level specifications, and not on system level specifications. Their goal is to ultimately generate C or Java code from a state diagram. But they are too low-level to test abstract properties, and we are too high-level to want to generate code. If we want a formalized test, we will need to describe our model in a general-purpose specification language.
Fortunately, for this case it is quite easy to do. To do this, we will use Alloy, since it can most accurately reflect the structure of the Harel State Diagram. 5 We can use signature extensions to represent nested states: “Standards” expand “Reports” means that each piece of “Standards” is also a “Report”, which is equivalent to the statement that this is a child state in the corresponding Harel Diagram. This simplifies the definition of transitions. Each of them is represented by one predicate that takes time (t), initial state (start) and final state (end), and declares that the state at time t goes from start to end for t.next. Despite the fact that parent states are abstract, we can still use them as a start and take advantage of parent transitions.
Now we can check the properties of our model. For example, is it possible to get a “answers” report without going through a “students” report?
We can also simulate an example when someone logs out and logs in again:
Alloy provides a fairly wide range of specifications. With the verification of certain properties, for example, tupiokov, difficulties may arise. However, I'm not the first person to see how well Alloy works with state diagrams. Professor Nancy Day recently announced an Alloy variant called DASH, which adds the first-class semantics of Harel Diagrams to Alloy. You can read about it here .
Does all this have value? What makes an interactive state diagram better than just notes in English? Definitely, a digram becomes more valuable when you scale. I remember that in the Snapshot project there were about two dozen teacher screens nested in several large hierarchies. Without a formal specification, we could not test our work. As far as I remember, some of the mistakes we made:
I think having a formal specification would help a lot. Writing the example I made above took about five minutes to write, and the specification for the full application would take less than two hours. If at the design stage it helped us find at least one of the errors listed, we would save a lot of time later.
We discussed the formal specification of user interaction with the UI. Can my love of formal methods overcome my fear of UI? Gosh no. If you followed the links to Sketch.systems, you probably saw that you can attach a prototype in Javascript to your state diagram. It `s Magic!
Despite my fear, I think there is some potential in formal methods. People usually think of them as purely academic things used exclusively by NASA. The main theme of this blog is that formal methods are powerful tools for everyday work. I mainly consider their application to the backend and parallel systems, because I enjoy it. But their use is not limited only to my preferences. Formal methods are especially important for the user interface. I don’t think Harel’s State Diagrams are by far the best possible notation, but this is a good first step.
By the way, hey, I am advising on formal methods . Tell your boss!
From the author
Relatively recently, I came across an article about Engineering methods in software development , where vasil-sd talked about the formal validation of specifications for software products being created. Alloy was used as a toolkit. One of the main leitmotifs in the comments was to parse the article in the context of some modern web project, because it’s expensive \ long \ difficult to use formal methods where everyone does it quickly / cheaply. Since the author referred to the Hillel Wayne blog, where such examples were, I decided to translate some of his articles as an addition to the main text of vasil-sd
Warning :
- Everything that the author calls a finite-state machine, I will call a state machine or a model of a state machine.
- I learned some of the terminology from an article I mentioned earlier about an engineering approach to development. Nevertheless, the topic for me is relatively new, because both authors (both foreign and not so) could understand not so - do not swear.
Formal UI Specification
A good user interface is essential for creating the right software. And if users have problems using the program, they are likely to do something wrong. I prefer not to work on the user interface - I do not consider myself superior to this, but it is “not mine”. The visual effects and interfaces cause me concern, and people who are able to cope with all this, cause me crazy respect.
I love formal methods. My friend Kevin Lynagh recently released sketch.systems 1 , a new formal specification tool for UI designers. Well, let's find out - can my love of formal methods overcome my fear?
Problem
Back in Edmodo, I was working on a user interface for our Snapshot application. This was our
In Snapshot, teachers can conduct “polls” or “snaps” among students. Further, the program aggregates survey results and provides teachers with several real-time reports in the following sections: “summary” report, “by students” and “by standards”. In addition, we decided that the program should have a “answers” report that could be opened from the “students” report and which provided information about incorrect answers.
WE imagined that the user moves between reports by pressing the necessary buttons, and that all reports should be accessible from other reports, with the exception of answers. The meaning of the word “available” in the context of transitions is rather vague: it may mean “you can somehow go to the report”, or it can mean “one-click go directly to the desired report.” Everything described above is only part of the user’s the interface of the entire application, which, in addition to navigation in reports, has its own navigation system.
When the system starts to get more complicated, we need to be careful. This means writing a specification. So how can we specify this? I see that the teacher can be on a certain screen of the application and can take actions to move to another screen. This leads me to the idea that we can consider the actions of the teacher as a finite state machine.
State machines
Finite state machines (FSM) is one of the simplest mathematical models of the theory of abstract automata. You have a finite set of states, a set of transitions between states, and a set of events (triggers) that trigger transitions. Each transition is tied to an event, so if the event occurs, the state may change. 3 In our model, the events are “the teacher presses the buttons.” The following is a state machine model for our current system:
The model shows two problems with our user interface. First, all state machines need an initial state, but we don’t have it. When a teacher visits the reports page, which report should he see first? Secondly, we do not indicate what happens when you click the button of the report that you are already viewing. This is ambiguous, as there are several behaviors:
- If you are in a summary report, the summary button does not appear or does nothing.
- If you are in a summary report, the summary button resets the report.
We chose the second option. Our initial state was a “summary" report. Updated model:
The model very accurately conveys our user interface - it is also cluttered. This is a significant limitation of the finite state machine model: the more transitions between states, the more difficult it is to perceive them. In our case, from almost every report it was possible to switch to another report.
Further development of the system and its modeling becomes problematic. Because, for example, if we take into account that at any moment the teacher could exit the system, then the next model of the state machine will already look something like this:
To add the logout function, we had to add four more ribs. Further development of the specification with this approach quickly ceases to be sound. We need some way to represent the “general” transitions. For this, we can use nested states, which will complicate our formalism, but simplify our specifications.
Harel Status Charts
Most of our states have a common logic of the so-called super-state: all four of our “reports” have the same logic for logging out of the system, and the main three have the same transitions. If we can group them into a “parental state” report, all that remains for us is to determine the transition to “exit” and distribute this transition in child states. The logic is similar to inheritance: child states inherit (or redefine) transitions of parent states.
Finite state machines with nested states are called hierarchical state machines, and there are several different ways to formalize them. The most suitable way to write state machine models for a UI is the Harel Statechart. 4 The rules for her are as follows:
- All parental states are abstract. Each parent state must define a default child state.
- Child states automatically inherit all parent transitions, but can also override them.
- A transition may indicate any state. If you switch to the parent state, instead go to its default child state. If the child state is also a parent, then the state is determined recursively.
You can design Harel State Charts in Graphviz and get horrified at the many vertices, edges, and delights of graphing graphs each time. We will use the much nicer user interface from 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
I would recommend following the link to the diagram, as she is interactive. You can click on the transitions and see how the states change. This is a great advantage of the Harkel State Diagram: they are not only formal and concise, but also kinetic. You can research them.
While studying the chart, I found a mistake: you can go directly from the “answers” to the “standards”. This can be fixed by making the “answers” a direct descendant of the “input” rather than the “reports”:
source
Ideally, it would be nice to clearly see such problems on the diagram, which implies some automation of the model verification.
Check
A formal specification has two advantages. One of them is implicit: work on formalization leads to a better understanding of the system. The other is explicit: if we have a formal specification, we can check its properties. Does our user interface have any deadlocks? Are there implicit or incorrectly specified transitions?
Sketch.systems can check if the Harel State Diagram has the correct format, but cannot check the behavior of the model. There are other tools for determining state of a state machine, in particular, UML state diagrams, but all of them are focused on code level specifications, and not on system level specifications. Their goal is to ultimately generate C or Java code from a state diagram. But they are too low-level to test abstract properties, and we are too high-level to want to generate code. If we want a formalized test, we will need to describe our model in a general-purpose specification language.
Fortunately, for this case it is quite easy to do. To do this, we will use Alloy, since it can most accurately reflect the structure of the Harel State Diagram. 5 We can use signature extensions to represent nested states: “Standards” expand “Reports” means that each piece of “Standards” is also a “Report”, which is equivalent to the statement that this is a child state in the corresponding Harel Diagram. This simplifies the definition of transitions. Each of them is represented by one predicate that takes time (t), initial state (start) and final state (end), and declares that the state at time t goes from start to end for t.next. Despite the fact that parent states are abstract, we can still use them as a start and take advantage of parent transitions.
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] }
Now we can check the properties of our model. For example, is it possible to get a “answers” report without going through a “students” report?
check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7 // valid
We can also simulate an example when someone logs out and logs in again:
run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7
Alloy provides a fairly wide range of specifications. With the verification of certain properties, for example, tupiokov, difficulties may arise. However, I'm not the first person to see how well Alloy works with state diagrams. Professor Nancy Day recently announced an Alloy variant called DASH, which adds the first-class semantics of Harel Diagrams to Alloy. You can read about it here .
Value
Does all this have value? What makes an interactive state diagram better than just notes in English? Definitely, a digram becomes more valuable when you scale. I remember that in the Snapshot project there were about two dozen teacher screens nested in several large hierarchies. Without a formal specification, we could not test our work. As far as I remember, some of the mistakes we made:
- We forgot to consider the “closing of the response report” as an event, and the “responses” became a dead end
- Creating a new survey had a bunch of county routes that we really don't need.
- We did not determine the user interface behavior after creating the survey, so we returned the teacher to the survey creation screen, he thought that during the error the survey was not created and recreated it
- It was hard to get to multiple screens, so no one ever went to them.
I think having a formal specification would help a lot. Writing the example I made above took about five minutes to write, and the specification for the full application would take less than two hours. If at the design stage it helped us find at least one of the errors listed, we would save a lot of time later.
Output
We discussed the formal specification of user interaction with the UI. Can my love of formal methods overcome my fear of UI? Gosh no. If you followed the links to Sketch.systems, you probably saw that you can attach a prototype in Javascript to your state diagram. It `s Magic!
Despite my fear, I think there is some potential in formal methods. People usually think of them as purely academic things used exclusively by NASA. The main theme of this blog is that formal methods are powerful tools for everyday work. I mainly consider their application to the backend and parallel systems, because I enjoy it. But their use is not limited only to my preferences. Formal methods are especially important for the user interface. I don’t think Harel’s State Diagrams are by far the best possible notation, but this is a good first step.
By the way, hey, I am advising on formal methods . Tell your boss!
- Warning, I was one of the alpha testrovers. Most of my feedback was like “you should make it more complicated!”. Yes, I'm so-so alpha tester. [return]
- In 2017, they gained 1 million and lost 20 million. [return]
- A finite state machine has much in common with a deterministic finite state machine, which is an important component of computer science. The main difference in the field of application: the use of a deterministic finite state machine is justified by the “set of regular languages that it recognizes”, the use of the finite state machine by “specification consistency” [return]
- The main competitor is the UML State Diagram, which basically represents the Harer State Diagram, supplementing with its code specifications. It is more expressive, but difficult to analyze. [return]
- If you are not familiar with Alloy, I wrote several articles on it here and here .
All Articles