Composición concurrente de máquinas de estados
| 1 | 2 | 3 | 4 | 5 | 6 |
|---|---|---|---|---|---|
| Especificación | Modelado | Verificación | Implementación | Verificación | Análisis |
| PARA QUÉ | QUÉ | CÓMO | |||
| ¿Cuál es el problema? | ¿Qué tiene que hacer el sistema? | ¿El modelo cumple la especificación? | ¿Cómo hace lo que tiene que hacer? (modelo refinado) | ¿La implementación cumple la especificación? | ¿Se cumplen los plazos en el caso peor? |
| LTL, CTL | FSM / xFSM | nuXmv | fsm.h / fsm.c | nuXmv | Análisis del tiempo |
| (model checking) | Ejecutivo cíclico / FreeRTOS / Reactor | (model checking) | de respuesta |
Implementación alternativa de HFSM
Consulta una implementación alternativa de estados jerárquicos en esta página.
Modelo de actor para FSM
Expone entradas y salidas para permitir la composición de FSM.
Figura: Modelo de FSM como actor en Ptolemy II
Composición paralela
Figura: Composición paralela
Las máquinas reaccionan simultáneamente e instantáneamente.
1MODULE cell(input) 2VAR 3 val : {red, green, blue}; 4ASSIGN 5 next(val) := {val, input}; 6 7MODULE main 8VAR 9 c1 : cell(c3.val); 10 c2 : cell(c1.val); 11 c3 : cell(c2.val);
La composición asíncrona no vamos a utilizarla. En el caso del ejemplo de arriba ambas descripciones pueden servir para describir el mismo sistema, sin necesidad de utilizar process. Veamos ahora un ejemplo de composición en paralelo y su equivalente en C utilizando la biblioteca fsm proporcionada en el tema anterior.
side_by_side.smv1MODULE cell 2VAR 3 out: 0..9; 4ASSIGN 5 init(out) := 0; 6 next(out) := (out + 1) mod 10; 7 8MODULE main 9VAR 10 m1 : cell; 11 m2 : cell; 12 sum: 0..18; 13ASSIGN 14 sum := m1.out + m2.out;
En el ejemplo de arriba obviamente habrá que reemplazar los printf por las operaciones de entrada/salida necesarias (gpio_get_level, gpio_set_level, etc.) que se requieran en una aplicación concreta.
Composición en cascada
Figura: Composición en cascada
cascade.smv1MODULE cell(input) 2VAR 3 out: 0..9; 4ASSIGN 5 init(out) := 0; 6 next(out) := case 7 input: (out + 1) mod 10; 8 !input: out; 9 esac; 10DEFINE 11 carry := out = 9; 12 13MODULE main 14VAR 15 m1 : cell(TRUE); 16 m2 : cell(m1.carry); 17 out: 0..99; 18ASSIGN 19 out := m1.out + 10 * m2.out;
Composición con realimentación
Figura: Composición con realimentación
La realimentación es muy delicada. Los modelos de computación definen la semántica concreta. Un modelo con muy razonables propiedades formales es el síncrono-reactivo, pero requiere del cálculo de puntos fijos, que implica iterar el cálculo de las salidas hasta que se estabilicen. Para el caso normal esto sería muy ineficiente.
En nuXmv la verificación de propiedades ocurre sobre el modelo completamente aplanado, por lo que la semántica concreta de la realimentación es poco importante, siempre que se mantenga la consistencia entre el modelo SMV y la implementación. Veamos un ejemplo.
feedback.smv1MODULE counter(input) 2VAR 3 out: 0..9; 4ASSIGN 5 init(out) := 0; 6 next(out) := case 7 !input: (out + 1) mod 10; 8 input: 0; 9 esac; 10 11MODULE detector(input, value) 12VAR 13 out: boolean; 14ASSIGN 15 init(out) := FALSE; 16 next(out) := case 17 input = value: TRUE; 18 input != value: FALSE; 19 esac; 20 21MODULE main 22VAR 23 m1 : counter(m2.out); 24 m2 : detector(m1.out, 3); 25DEFINE 26 out := m1.out;
Máquinas de estado jerárquicas
El concepto de jerarquía de nuXmv se refiere a la composición concurrente, no al refinamiento de estados de Lee&Seshia. Por tanto las máquinas de estados jerárquicas (con estados refinados por otra máquina de estados) debe implementarse de forma manual.
hierarchical_fsm.smv1MODULE main 2IVAR 3 g1: boolean; 4 g2: boolean; 5VAR 6 s: { sA, sB }; 7 a1: boolean; 8 a2: boolean; 9 fsmB: nested(s = sB); 10ASSIGN 11 init(s) := sA; 12 next(s) := case 13 s = sA & g2: sB; 14 s = sB & g1: sA; 15 TRUE: s; 16 esac; 17 next(a1) := (s = sB & g1); 18 next(a2) := (s = sA & g2); 19 20 21MODULE nested(active) 22IVAR 23 g3: boolean; 24 g4: boolean; 25VAR 26 s: { sC, sD }; 27 a3: boolean; 28 a4: boolean; 29ASSIGN 30 init(s) := sC; 31 next(s) := case 32 active & s = sC & g4: sD; 33 active & s = sD & g3: sC; 34 TRUE: s; 35 esac; 36 next(a3) := (active & s = sD & g3); 37 next(a4) := (active & s = sC & g4);
Obviamente es necesario rellenar el código de las funciones de guarda y de acción con el código correspondiente a la aplicaciópn concreta (típicamente gpio_get_level y gpio_set_level).