| 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 |
Paso a paso