Aplicação de métodos formais de validação de modelo para UI

Olá Habr! Apresento a você a tradução do artigo “FORMALLY SPECIFYING UIS” de Hillel Wayne.

Do autor

Recentemente, deparei com um artigo sobre métodos de engenharia no desenvolvimento de software , onde vasil-sd falou sobre a validação formal de especificações para produtos de software que estavam sendo criados. Liga foi usada como um kit de ferramentas. Um dos principais temas nos comentários foi analisar o artigo no contexto de algum projeto moderno da Web, porque é caro / longo \ difícil usar métodos formais, onde todo mundo faz isso de forma rápida / barata. Como o autor se referiu ao blog Hillel Wayne, onde esses exemplos estavam, decidi traduzir alguns de seus artigos como um complemento ao texto principal de vasil-sd

Atenção :

• Tudo o que o autor chama de máquina de estado finito, chamarei de máquina de estado ou modelo de máquina de estado.
• Aprendi algumas das terminologias de um artigo mencionado anteriormente sobre uma abordagem de engenharia para o desenvolvimento. No entanto, o tópico para mim é relativamente novo, porque ambos os autores (estrangeiros e não tão) poderiam entender isso - não juro.

Especificação formal da interface do usuário

Uma boa interface do usuário é essencial para criar o software certo. E se os usuários tiverem problemas ao usar o programa, eles provavelmente farão algo errado. Prefiro não trabalhar na interface do usuário - não me considero acima disso, mas "não é minha". Os efeitos visuais e as interfaces me preocupam e as pessoas que conseguem lidar com tudo isso me causam um respeito louco.

Eu amo métodos formais. Meu amigo Kevin Lynagh lançou recentemente o sketch.systems ¹ , uma nova ferramenta de especificação formal para designers de interface do usuário. Bem, vamos descobrir - meu amor por métodos formais pode superar meu medo?

O problema

De volta ao Edmodo, eu estava trabalhando em uma interface de usuário para nosso aplicativo Snapshot. Esta foi a nossa primeira segunda tentativa de ganhar dinheiro: começamos dando a todos os professores um programa gratuito e depois pedindo doações ou algo assim. Como você pode ver, o Edmodo não difere muito da visão de negócios. ²

No Snapshot, os professores podem realizar "pesquisas" ou "snapshots" entre os alunos. Além disso, o programa agrega os resultados da pesquisa e fornece aos professores vários relatórios em tempo real nas seções a seguir: relatório "resumo", "pelos alunos" e "pelos padrões". Além disso, decidimos que o programa deveria ter um relatório de "respostas" que pudesse ser aberto a partir do relatório de "alunos" e que fornecesse informações sobre respostas incorretas.

Imaginamos que o usuário se movesse entre os relatórios pressionando os botões necessários e que todos os relatórios deveriam ser acessíveis a partir de outros relatórios, com exceção das respostas. O significado da palavra "disponível" no contexto de transições é bastante vago: pode significar "você pode ir de alguma forma ao relatório" ou "ir com um clique diretamente ao relatório desejado". Tudo o que foi descrito acima é apenas parte do conteúdo do usuário. a interface de todo o aplicativo que, além da navegação nos relatórios, possui seu próprio sistema de navegação.

Quando o sistema começa a ficar mais complicado, precisamos ter cuidado. Isso significa escrever uma especificação. Então, como podemos especificar isso? Vejo que o professor pode estar em uma tela específica do aplicativo e pode executar ações para mudar para outra tela. Isso me leva à ideia de que podemos considerar as ações do professor como uma máquina de estados finitos.

Máquinas de estado

Máquinas de estados finitos (FSMs) são um dos modelos matemáticos mais simples da teoria dos autômatos abstratos. Você tem um conjunto finito de estados, um conjunto de transições entre estados e um conjunto de eventos (gatilhos) que acionam transições. Cada transição está vinculada a um evento, portanto, se o evento ocorrer, o estado poderá mudar. ³ Em nosso modelo, os eventos serão “o professor pressiona os botões”. A seguir, é apresentado um modelo de máquina de estado para o nosso sistema atual:


O modelo mostra dois problemas com nossa interface do usuário. Em primeiro lugar, todas as máquinas de estados finitos precisam de um estado inicial, mas não o temos. Quando um professor visita a página de relatórios, qual relatório ele deve ver primeiro? Em segundo lugar, não indicamos o que acontece quando você clica no botão do relatório que já está visualizando. Isso é ambíguo, pois existem vários comportamentos:

1. Se você estiver em um relatório de resumo, o botão Resumo não aparecerá ou não fará nada.
2. Se você estiver em um relatório de resumo, o botão Resumo redefine o relatório.

Nós escolhemos a segunda opção. Nosso estado inicial era um relatório "resumo". Modelo atualizado:


O modelo transmite com muita precisão nossa interface de usuário - também é confusa. Essa é uma limitação significativa do modelo de máquina de estados finitos: quanto mais transições entre estados, mais difícil é percebê-los. No nosso caso, em quase todos os relatórios, foi possível mudar para outro relatório.

O desenvolvimento do sistema e sua modelagem se tornam problemáticos. Porque, por exemplo, se levarmos em conta que a qualquer momento o professor pode sair do sistema, o próximo modelo da máquina de estado já terá algo parecido com isto:


Para adicionar a função de logout, tivemos que adicionar mais quatro arestas. O desenvolvimento de especificações adicionais com essa abordagem rapidamente deixa de ser sólido. Precisamos de alguma maneira de representar as transições "gerais". Para isso, podemos usar estados aninhados, o que complicará nosso formalismo, mas simplificará nossas especificações.

Harel Status Charts

A maioria dos nossos estados possui uma lógica comum do chamado superestado: todos os nossos quatro "relatórios" têm a mesma lógica para fazer logoff do sistema, e os três principais têm as mesmas transições. Se pudermos agrupá-los em um relatório de "estado parental", tudo o que resta para nós é determinar a transição para "sair" e distribuir essa transição em estados filhos. A lógica é semelhante à herança: os estados filhos herdam (ou substituem) as transições dos estados pai.

Máquinas de estados finitos com estados aninhados são chamadas de máquinas de estados hierárquicas e existem várias maneiras diferentes de formalizá-las. A maneira mais adequada de escrever modelos de máquina de estado para uma interface do usuário é o Harel Statechart. ^{4 As} regras para ela são as seguintes:

1. Todos os estados parentais são abstratos. Cada estado pai deve definir um estado filho padrão.
2. Os estados filhos herdam automaticamente todas as transições pai, mas também podem substituí-las.
3. Uma transição pode indicar qualquer estado. Se você alternar para o estado pai, vá para o estado filho padrão. Se o estado filho também for pai, então o estado é determinado recursivamente.

Você pode desenvolver gráficos do estado de Harel no Graphviz e ficar horrorizado com os vários vértices, arestas e delícias dos gráficos gráficos sempre. Usaremos a interface de usuário muito melhor do 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 

_fonte

Eu recomendaria seguir o link para o diagrama, como ela é interativa. Você pode clicar nas transições e ver como os estados mudam. Essa é uma grande vantagem do diagrama do estado de Harkel: eles não são apenas formais e concisos, mas também cinéticos. Você pode pesquisá-los.

Ao estudar o gráfico, encontrei um erro: você pode ir diretamente das “respostas” para os “padrões”. Isso pode ser corrigido tornando as "respostas" um descendente direto da "entrada" e não dos "relatórios":


_fonte

Idealmente, seria bom ver claramente esses problemas no diagrama, o que implica alguma automação da verificação do modelo.

Verifique

Uma especificação formal tem duas vantagens. Um deles está implícito: o trabalho de formalização leva a uma melhor compreensão do sistema. O outro é explícito: se temos uma especificação formal, podemos verificar suas propriedades. Nossa interface do usuário tem algum conflito? Existem transições implícitas ou especificadas incorretamente?

O Sketch.systems pode verificar se o Harel State Diagram possui o formato correto, mas não pode verificar o comportamento do modelo. Existem outras ferramentas para determinar o estado de uma máquina de estado, em particular os diagramas de estado UML, mas todas elas são orientadas para especificações de nível de código e não para especificações de nível de sistema. Seu objetivo é finalmente gerar código C ou Java a partir de um diagrama de estado. Mas eles são de nível muito baixo para testar propriedades abstratas e nós somos de alto nível para querer gerar código. Se queremos um teste formalizado, precisaremos descrever nosso modelo em uma linguagem de especificação de uso geral.

Felizmente, para este caso, é bastante fácil de fazer. Para isso, usaremos o Alloy, pois ele pode refletir com mais precisão a estrutura do Diagrama do Estado de Harel. ⁵ Podemos usar extensões de assinatura para representar estados aninhados: “Padrões” estendem “Relatórios” significa que cada parte dos “Padrões” também é um “Relatório”, que é equivalente à afirmação de que este é um estado filho no Diagrama de Harel correspondente. Isso simplifica a definição de transições. Cada um deles é representado por um único predicado que leva o tempo (t), o estado inicial (início) e o estado final (final), e declara que o estado no momento t vai do início ao fim para t.next. Apesar do fato de os estados pais serem abstratos, ainda podemos usá-los como um começo e tirar proveito das transições pai.

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

Agora podemos verificar as propriedades do nosso modelo. Por exemplo, é possível obter o relatório de "respostas" sem passar pelo relatório de "alunos"?

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

Também podemos simular um exemplo quando alguém se desconecta e se conecta novamente:

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

Liga fornece uma gama bastante ampla de especificações. Com a verificação de certas propriedades, por exemplo, tupiokov, podem surgir dificuldades. No entanto, não sou a primeira pessoa a ver como o Alloy funciona com diagramas de estados. A professora Nancy Day anunciou recentemente uma variante Alloy chamada DASH, que adiciona a semântica de primeira classe dos diagramas Harel ao Alloy. Você pode ler sobre isso aqui .

Valor

Tudo isso tem valor? O que torna um diagrama de estados interativo melhor do que apenas anotações em inglês? Definitivamente, um digram se torna mais valioso quando você escala. Lembro que no projeto Snapshot havia cerca de duas dúzias de telas de professores aninhadas em várias hierarquias grandes. Sem uma especificação formal, não poderíamos testar nosso trabalho. Tanto quanto me lembro, alguns dos erros que cometemos:

• Esquecemos de considerar o “fechamento do relatório de respostas” como um evento, e as “respostas” se tornaram um beco sem saída
• A criação de uma nova pesquisa teve várias rotas de condado que realmente não precisamos.
• Como não determinamos o comportamento da interface do usuário após a criação da pesquisa, retornamos o professor à tela de criação da pesquisa, ele pensou que durante o erro a pesquisa não foi criada e a recriou.
• Era difícil acessar várias telas, então ninguém nunca foi a elas.

Eu acho que ter uma especificação formal ajudaria muito. Escrever o exemplo que fiz acima levou cerca de cinco minutos para ser escrito, e a especificação para o aplicativo completo levaria menos de duas horas. Se, mesmo no estágio de design, isso nos ajudou a encontrar pelo menos um dos erros listados, economizaríamos muito tempo mais tarde.

Conclusão

Discutimos a especificação formal da interação do usuário com a interface do usuário. Meu amor por métodos formais pode superar meu medo de interface do usuário? Puxa, não. Se você seguiu os links para o Sketch.systems, provavelmente viu que pode anexar um protótipo em Javascript ao seu diagrama de estado. Isso é mágico!

Apesar do meu medo, acho que há algum potencial nos métodos formais. As pessoas geralmente pensam nelas como coisas puramente acadêmicas usadas exclusivamente pela NASA. O tema principal deste blog é que os métodos formais são ferramentas poderosas para o trabalho diário. Considero principalmente a sua aplicação nos sistemas back-end e paralelo, porque gosto disso. Mas o uso deles não se limita apenas às minhas preferências. Métodos formais são especialmente importantes para a interface do usuário. Não acho que os diagramas de estado de Harel sejam de longe a melhor notação possível, mas esse é um bom primeiro passo.

A propósito, ei, eu aconselho sobre métodos formais . Diga ao seu chefe!

---

1. Aviso, eu fui um dos alfa testrovers. A maior parte do meu feedback foi do tipo "você deveria torná-lo mais complicado!". Sim, sou um testador alfa mais ou menos. ^[voltar]
2. Em 2017, eles ganharam 1 milhão e perderam 20 milhões. ^[voltar]
3. Uma máquina de estados finitos tem muito em comum com uma máquina determinística de estados finitos, que é um componente importante da ciência da computação. A principal diferença no campo de aplicação: o uso de uma máquina determinista de estados finitos é justificado pelo "conjunto de linguagens regulares que ele reconhece", o uso da máquina de estados finitos por "consistência de especificação" ^[retornar]
4. O principal concorrente é o diagrama de estados UML, que basicamente representa o diagrama de estados Harer, complementando suas especificações de código. É mais expressivo, mas difícil de analisar. ^[voltar]
5. Se você não conhece o Alloy, escrevi vários artigos aqui e aqui .