| 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 |
Libro de texto
Lee [Lee&Seshia] capítulo 14. Gran parte de esta página es traducción directa de ese capítulo.
Transparencias
Transparencias de E. Lee usadas en clase.
A abstrae B si A es más sencillo, más pequeño, o más fácil de entender.
Una abstracción es sólida (con respecto a algún sistema formal de propiedades) si las propiedades que son verdaderas de la abstracción también lo son del refinamiento. El sistema formal de propiedades puede ser, por ejemplo, un sistema de tipos, la lógica temporal lineal o los lenguajes de máquinas de estado.
Las abstracciones útiles suelen ser sólidas pero no completas, porque es difícil hacer una abstracción completa que sea significativamente más simple o más pequeña.
Puertos y Señales de la Máquina de Estados: Cada puerto de una máquina de estados está asociado con un tipo, y puede recibir o producir una secuencia de valores (o estar ausente) en cada reacción. Esta secuencia se representa como una función que mapea de números naturales al conjunto de posibles valores más un marcador de 'ausente'.
Lenguaje de una Máquina de Estados: El conjunto de todos los comportamientos posibles (asignaciones de señales a puertos) de una máquina de estados define su lenguaje. La equivalencia de lenguaje entre dos máquinas significa que tienen el mismo conjunto de comportamientos.
Máquinas No Deterministas: Para las máquinas no deterministas, múltiples comportamientos (secuencias de salida) pueden corresponder a la misma señal de entrada, abarcando todos los comportamientos posibles en el lenguaje de la máquina. La equivalencia de lenguaje en este contexto aún se mantiene cuando dos máquinas pueden producir los mismos conjuntos de comportamientos para las mismas secuencias de entrada. La equivalencia de lenguaje también se denomina equivalencia de traza.
Contención y Refinamiento de Lenguaje: Cuando el lenguaje de la máquina A es un subconjunto del lenguaje de la máquina B (L(A) ⊂ L(B)), A se considera un refinamiento de B. Esto significa que A puede sustituir a B en cualquier entorno que encuentre aceptables los comportamientos de B. La contención de lenguaje es significativa para verificar fórmulas de Lógica Temporal Lineal (LTL) sobre secuencias de entrada y salida, pero no para aquellas que se refieren a estados de la máquina.
Simulación: Este concepto va más allá de la equivalencia de lenguaje al requerir que una máquina (M1) pueda coincidir con las reacciones de otra (M2) en todas las secuencias de entrada posibles, a pesar de las elecciones no deterministas. Si M1 siempre puede producir salidas coincidentes a las de M2, simula a M2. La relación de simulación captura todos los posibles pares de estados a través de estas máquinas para los cuales M1 puede simular a M2.
Definición Formal de Simulación: La simulación se define formalmente utilizando los estados, entradas, salidas y posibles actualizaciones de dos máquinas. Una relación de simulación es un conjunto de pares de estados (de M2 a M1) que satisface condiciones específicas asegurando que M1 puede coincidir con la salida de M2 para cada entrada.
Transitividad y No Unicidad: La simulación es transitiva; si M1 simula a M2 y M2 simula a M3, entonces M1 simula a M3. Además, puede haber más de una relación de simulación entre dos máquinas.
Simulación vs. Contención de Lenguaje: La simulación implica contención de lenguaje (L(M2) ⊆ L(M1)), pero lo contrario no es necesariamente cierto. La simulación proporciona una garantía más fuerte que la contención de lenguaje, particularmente para FSM no deterministas.
Bisimulación: Una equivalencia más fuerte que la simulación, la bisimulación requiere que dos máquinas puedan simularse mutuamente, asegurando que son observacionalmente idénticas en todos los entornos. Una relación de bisimulación se establece si para cada par de estados en la relación, cada máquina puede coincidir con la salida de la otra para cada entrada.