Aplicación de métodos formales de validación de modelos para IU

Hola Habr! Les presento la traducción del artículo "FORMALMENTE ESPECIFICANDO UIS" por Hillel Wayne.

Del autor

Hace relativamente poco, me encontré con un artículo sobre métodos de ingeniería en el desarrollo de software , donde vasil-sd habló sobre la validación formal de las especificaciones para los productos de software que se están creando. La aleación se usó como un juego de herramientas. Uno de los principales leitmotivs en los comentarios fue analizar el artículo en el contexto de algún proyecto web moderno, porque es costoso \ largo \ difícil de usar métodos formales donde todos lo hacen de manera rápida / económica. Como el autor se refirió al blog de Hillel Wayne, donde se encontraban tales ejemplos, decidí traducir algunos de sus artículos como una adición al texto principal de vasil-sd

Advertencia :

• Todo lo que el autor llama máquina de estado finito, lo llamaré máquina de estado o modelo de máquina de estado.
• Aprendí algo de la terminología de un artículo que mencioné anteriormente sobre un enfoque de ingeniería para el desarrollo. Sin embargo, el tema para mí es relativamente nuevo, porque ambos autores (tanto extranjeros como no) podrían entender que no, no lo juren.

Especificación formal de IU

Una buena interfaz de usuario es esencial para crear el software adecuado. Y si los usuarios tienen problemas para usar el programa, es probable que hagan algo mal. Prefiero no trabajar en la interfaz de usuario, no me considero por encima de esto, pero "no es mío". Los efectos visuales y las interfaces me preocupan, y las personas que son capaces de hacer frente a todo esto me causan un gran respeto.

Amo los métodos formales. Mi amigo Kevin Lynagh lanzó recientemente sketch.systems ¹ , una nueva herramienta de especificación formal para diseñadores de UI. Bueno, descubramos: ¿puede mi amor por los métodos formales superar mi miedo?

El problema

De vuelta en Edmodo, estaba trabajando en una interfaz de usuario para nuestra aplicación Snapshot. Este fue nuestro primer segundo intento de ganar dinero: comenzamos dándoles a todos los maestros un programa gratuito y luego pidiendo donaciones o algo así. Como puede ver, Edmodo no difería mucho de su visión para los negocios. ²

En Snapshot, los maestros pueden realizar "encuestas" o "instantáneas" entre los estudiantes. Además, el programa agrega los resultados de la encuesta y proporciona a los maestros varios informes en tiempo real en las siguientes secciones: informe "resumen", "por estudiantes" y "según los estándares". Además, decidimos que el programa debería tener un informe de "respuestas" que podría abrirse desde el informe de "estudiantes" y que proporcionara información sobre respuestas incorrectas.

Nos imaginamos que el usuario se mueve entre los informes presionando los botones necesarios, y que todos los informes deben ser accesibles desde otros informes, con la excepción de las respuestas. El significado de la palabra "disponible" en el contexto de las transiciones es bastante vago: puede significar "de alguna manera puede ir al informe", o puede significar "ir con un clic directamente al informe deseado". Todo lo descrito anteriormente es solo parte del usuario La interfaz de toda la aplicación, que, además de la navegación en los informes, tiene su propio sistema de navegación.

Cuando el sistema comienza a complicarse, debemos tener cuidado. Esto significa escribir una especificación. Entonces, ¿cómo podemos especificar esto? Veo que el profesor puede estar en una pantalla específica de la aplicación y puede tomar medidas para pasar a otra pantalla. Esto me lleva a la idea de que podemos considerar las acciones del maestro como una máquina de estados finitos.

Máquinas de estado

Las máquinas de estados finitos (FSM) son uno de los modelos matemáticos más simples de la teoría de los autómatas abstractos. Tiene un conjunto finito de estados, un conjunto de transiciones entre estados y un conjunto de eventos (desencadenantes) que desencadenan transiciones. Cada transición está vinculada a un evento, por lo que si el evento ocurre, el estado puede cambiar. ³ En nuestro modelo, los eventos serán "el maestro presiona los botones". El siguiente es un modelo de máquina de estado para nuestro sistema actual:


El modelo muestra dos problemas con nuestra interfaz de usuario. En primer lugar, todas las máquinas de estados finitos necesitan un estado inicial, pero no lo tenemos. Cuando un maestro visita la página de informes, ¿qué informe debería ver primero? En segundo lugar, no indicamos qué sucede cuando hace clic en el botón del informe que ya está viendo. Esto es ambiguo, ya que hay varios comportamientos:

1. Si está en un informe de resumen, el botón de resumen no aparece o no hace nada.
2. Si está en un informe de resumen, el botón de resumen restablece el informe.

Hemos elegido la segunda opción. Nuestro estado inicial era un informe "resumen". Modelo actualizado:


El modelo transmite con mucha precisión nuestra interfaz de usuario, también está abarrotada. Esta es una limitación significativa del modelo de máquina de estados finitos: cuantas más transiciones entre estados, más difícil es percibirlas. En nuestro caso, de casi todos los informes fue posible cambiar a otro informe.

El desarrollo posterior del sistema y su modelado se vuelve problemático. Porque, por ejemplo, si tenemos en cuenta que en cualquier momento el maestro podría desconectarse del sistema, entonces el siguiente modelo de la máquina de estado ya se verá así:


Para agregar la función de cierre de sesión, tuvimos que agregar cuatro bordes más. El desarrollo adicional de especificaciones con este enfoque deja de ser rápidamente rápido. Necesitamos alguna forma de representar las transiciones "generales". Para esto, podemos usar estados anidados, lo que complicará nuestro formalismo, pero simplificará nuestras especificaciones.

Tablas de estado de Harel

La mayoría de nuestros estados tienen una lógica común del llamado superestado: nuestros cuatro "informes" tienen la misma lógica para cerrar sesión en el sistema, y ​​los tres principales tienen las mismas transiciones. Si podemos agruparlos en un informe de "estado parental", todo lo que nos queda es determinar la transición a la "salida" y distribuir esta transición en los estados secundarios. La lógica es similar a la herencia: los estados secundarios heredan (o anulan) las transiciones de los estados primarios.

Las máquinas de estados finitos con estados anidados se denominan máquinas de estados jerárquicos , y hay varias formas diferentes de formalizarlas. La forma más adecuada de escribir modelos de máquinas de estado para una interfaz de usuario es el diagrama de estado de Harel. ^{4 Las} reglas para ella son las siguientes:

1. Todos los estados parentales son abstractos. Cada estado primario debe definir un estado secundario predeterminado.
2. Los estados secundarios heredan automáticamente todas las transiciones principales, pero también pueden anularlas.
3. Una transición puede indicar cualquier estado. Si cambia al estado primario, vaya a su estado secundario predeterminado. Si el estado secundario también es padre, entonces el estado se determina de forma recursiva.

Puede desarrollar gráficos de estado de Harel en Graphviz y horrorizarse ante los muchos vértices, bordes y delicias de los gráficos gráficos cada vez. Utilizaremos la interfaz de usuario mucho mejor 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 

_fuente

Recomendaría seguir el enlace al diagrama, como Ella es interactiva. Puede hacer clic en las transiciones y ver cómo cambian los estados. Esta es una gran ventaja del Diagrama del Estado de Harkel: no solo son formales y concisos, sino también cinéticos. Puedes investigarlos.

Mientras estudiaba la tabla, encontré un error: puede pasar directamente de las "respuestas" a las "normas". Esto se puede solucionar haciendo que las "respuestas" sean un descendiente directo de la "entrada" en lugar de los "informes":


_fuente

Idealmente, sería bueno ver claramente tales problemas en el diagrama, lo que implica cierta automatización de la verificación del modelo.

Cheque

Una especificación formal tiene dos ventajas. Uno de ellos está implícito: el trabajo sobre formalización conduce a una mejor comprensión del sistema. El otro es explícito: si tenemos una especificación formal, podemos verificar sus propiedades. ¿Nuestra interfaz de usuario tiene puntos muertos? ¿Hay transiciones implícitas o especificadas incorrectamente?

Sketch.systems puede verificar si el diagrama de estado de Harel tiene el formato correcto, pero no puede verificar el comportamiento del modelo. Existen otras herramientas para determinar el estado de una máquina de estados, en particular, los diagramas de estado UML, pero todas están orientadas a especificaciones de nivel de código y no a especificaciones de nivel de sistema. Su objetivo es, en última instancia, generar código C o Java a partir de un diagrama de estado. Pero tienen un nivel demasiado bajo para probar las propiedades abstractas, y nosotros tenemos un nivel demasiado alto para querer generar código. Si queremos una prueba formalizada, necesitaremos describir nuestro modelo en un lenguaje de especificación de propósito general.

Afortunadamente, para este caso es bastante fácil de hacer. Para esto, utilizaremos Alloy, ya que puede reflejar con mayor precisión la estructura del Diagrama del Estado de Harel. ⁵ Podemos usar extensiones de firma para representar estados anidados: “Estándares” extienden “Informes” significa que cada pieza de “Estándares” también es un “Informe”, que es equivalente a la afirmación de que este es un estado secundario en el Diagrama de Harel correspondiente. Esto simplifica la definición de transiciones. Cada uno de ellos está representado por un predicado único que requiere tiempo (t), estado inicial (inicio) y estado final (final), y declara que el estado en el tiempo t va de principio a fin para t.siguiente. A pesar de que los estados primarios son abstractos, aún podemos usarlos como un comienzo y aprovechar las transiciones primarias.

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

Ahora podemos verificar las propiedades de nuestro modelo. Por ejemplo, ¿es posible obtener el informe de "respuestas" sin pasar por el informe de "estudiantes"?

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

También podemos simular un ejemplo cuando alguien cierra sesión y vuelve a iniciar sesión:

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

La aleación proporciona una gama bastante amplia de especificaciones. Con la verificación de ciertas propiedades, por ejemplo, tupiokov, pueden surgir dificultades. Sin embargo, no soy la primera persona en ver qué tan bien funciona Alloy con los diagramas de estado. La profesora Nancy Day anunció recientemente una variante de Alloy llamada DASH, que agrega la semántica de primera clase de Harel Diagrams a Alloy. Puedes leer sobre esto aquí .

Valor

¿Todo esto tiene valor? ¿Qué hace que un diagrama de estado interactivo sea mejor que solo notas en inglés? Definitivamente, un digram se vuelve más valioso cuando escalas. Recuerdo que en el proyecto Instantánea había aproximadamente dos docenas de pantallas de maestros anidadas en varias jerarquías grandes. Sin una especificación formal, no podríamos probar nuestro trabajo. Hasta donde recuerdo, algunos de los errores que cometimos:

• Olvidamos considerar el "cierre del informe de respuesta" como un evento, y las "respuestas" se convirtieron en un callejón sin salida
• La creación de una nueva encuesta tenía un montón de rutas del condado que realmente no necesitamos.
• No determinamos el comportamiento de la interfaz de usuario después de crear la encuesta, por lo que devolvimos al profesor a la pantalla de creación de la encuesta, pensó que durante el error la encuesta no se creó y la recreó
• Fue difícil acceder a varias pantallas, por lo que nadie fue a ellas.

Creo que tener una especificación formal ayudaría mucho. Escribir el ejemplo que hice anteriormente tardó unos cinco minutos en escribirse, y la especificación para la aplicación completa tardaría menos de dos horas. Si, incluso en la etapa de diseño, esto nos ayudara a encontrar al menos uno de los errores enumerados, ahorraríamos mucho tiempo más adelante.

Conclusión

Discutimos la especificación formal de la interacción del usuario con la interfaz de usuario. ¿Puede mi amor por los métodos formales superar mi miedo a la IU? Gosh no. Si siguió los enlaces a Sketch.systems, probablemente vio que puede adjuntar un prototipo en Javascript a su diagrama de estado. Esto es magico!

A pesar de mi miedo, creo que hay algún potencial en los métodos formales. La gente suele pensar en ellos como cosas puramente académicas utilizadas exclusivamente por la NASA. El tema principal de este blog es que los métodos formales son herramientas poderosas para el trabajo diario. Principalmente considero su aplicación al backend y sistemas paralelos, porque lo disfruto. Pero su uso no se limita solo a mis preferencias. Los métodos formales son especialmente importantes para la interfaz de usuario. No creo que los diagramas de estado de Harel sean, de lejos, la mejor notación posible, pero este es un buen primer paso.

Por cierto, oye, aconsejo sobre métodos formales . ¡Dile a tu jefe!

---

1. Advertencia, yo era uno de los alfa testrovers. La mayoría de mis comentarios fueron como "¡deberías hacerlo más complicado!". Sí, soy un probador alfa más o menos. ^[volver]
2. En 2017, ganaron 1 millón y perdieron 20 millones. ^[volver]
3. Una máquina de estados finitos tiene mucho en común con una máquina de estados finitos determinista, que es un componente importante de la informática. La principal diferencia en el campo de aplicación: el uso de una máquina de estados finitos determinista se justifica por el "conjunto de lenguajes regulares que reconoce", el uso de la máquina de estados finitos por "consistencia de especificación" ^[volver]
4. El principal competidor es el Diagrama de estado de UML, que básicamente representa el Diagrama de estado de Harer, que se complementa con las especificaciones de su código. Es más expresivo, pero difícil de analizar. ^[volver]
5. Si no está familiarizado con Alloy, escribí varios artículos aquí y aquí .