Resumen Técnico: Un Marco Unificado para la Verificación en Tiempo de Ejecución y el Diagnóstico Basado en Modelos en Lola

Planteamiento del Problema

Los sistemas críticos para la seguridad requieren no solo la detección de fallos, sino también la localización de sus causas raíz para permitir una mitigación efectiva. Mientras que la Verificación en Tiempo de Ejecución (RV) es eficaz para detectar desviaciones del comportamiento especificado durante la ejecución, y el Diagnóstico Basado en Modelos (MBD) es un marco basado en principios para identificar componentes defectuosos, estas dos técnicas han operado históricamente de forma aislada. Los monitores de RV tradicionales analizan el comportamiento del sistema sobre secuencias de estados potencialmente ilimitadas para detectar violaciones, mientras que el MBD suele operar en un único punto temporal no especificado tras la detección de un fallo. Además, las integraciones existentes a menudo no logran mapear las acciones de fallo detectadas directamente con componentes anormales en el sentido del MBD o carecen de la capacidad de manejar entradas inciertas y la dinámica temporal de los fallos dentro de un marco de razonamiento unificado basado en flujos (streams).

Metodología

El artículo propone un marco unificado que integra la RV basada en flujos y el MBD dentro de Lola, un lenguaje de especificación sincrónico basado en flujos. La metodología central consiste en codificar tanto la verificación como la información diagnóstica como flujos especializados, lo que permite la observación continua y el razonamiento simbólico bajo incertidumbre.

1. Codificación Unificada en Lola

Los autores mapean un sistema diagnosticado $S = (sd, comps)$ a un Sistema Lola $(\phi, comps)$:

• Descripción del Sistema ($sd$): Codificada en el flujo de suposiciones ($\alpha$), que es verdadero por definición. Este flujo contiene el conocimiento conductual (por ejemplo, $\neg ab(c) \to beh_c$) y el conocimiento general del sistema.
• Componentes ($comps$): Cada componente $c$ está representado por un flujo booleano interno donde true indica que el componente es anormal ($ab(c)$).
• Observaciones: Las variables observables del sistema (entradas/salidas) se modelan como flujos de entrada, que pueden ser ciertos (deterministas) o inciertos (intervalos o conjuntos no deterministas).
• Variables No Observables: Los valores internos del sistema no medidos directamente se modelan como flujos internos.
• Instancia del Problema de Diagnóstico (DPI): Una tupla $(\phi, comps, \Psi)$, donde $\Psi$ representa el historial de restricciones de entrada hasta el tiempo actual.

2. Razonamiento Simbólico y Computación del Diagnóstico

El marco utiliza un monitor simbólico que mantiene un conjunto de restricciones $[\phi]_{\Psi}^{\leq t}$ que representa todos los comportamientos posibles del sistema consistentes con las observaciones hasta el tiempo $t$.

• Resolución de Restricciones: Se utiliza un solver SMT (por ejemplo, Z3) para verificar la consistencia y derivar implicaciones.
• Derivación del Diagnóstico: Un diagnóstico es una suposición sobre el estado (normal/anormal) de los componentes que hace que la descripción del sistema sea consistente con las observaciones. El marco computa diagnósticos mínimos identificando conflictos mínimos (conjuntos de componentes que no pueden ser todos normales) y calculando sus conjuntos de golpeo mínimos (minimal hitting sets).
• Poda (Pruning): Para garantizar un monitoreo de tiempo y espacio constantes, las estrategias de poda reescriben las restricciones para acotar el tamaño del conjunto de restricciones, reteniendo solo la información histórica necesaria.

3. Escenarios Diagnósticos

El marco soporta tres modos diagnósticos distintos basados en la naturaleza temporal de los fallos de los componentes:

• Diagnóstico Multi-Instante: Asume que los estados de los componentes son estáticos durante una ventana de $k$ instantes pasados ($t-k$ a $t$). Un diagnóstico de $k$-instantes explica todas las observaciones dentro de esta ventana. El artículo demuestra que para especificaciones atemporales, los diagnósticos de $k$-instantes son equivalentes a agregar diagnósticos de un solo instante, pero para especificaciones temporales (con desfases distintos de cero), proporcionan resultados más enfocados.
• Diagnóstico Temporal: Permite que los estados de los componentes cambien a lo largo del tiempo. Un diagnóstico $k$-temporal es un conjunto de pares $(c, t')$ que indica que el componente $c$ es anormal específicamente en el tiempo $t'$. Esto es crítico para identificar fallos transitorios (por ejemplo, sobrecalentamiento) o fallos que se manifiestan más tarde debido a la propagación.
• Configuraciones Extendidas: El marco incorpora naturalmente el conocimiento de fondo (forzando a los componentes a ser normales), modelos de fallo fuertes (especificando comportamientos defectuosos específicos) y el modelado abstracto.

Principales Contribuciones

1. Codificación Unificada: Un método para expresar descripciones de sistemas y suposiciones diagnósticas como flujos especializados en Lola, representando implícitamente todos los diagnósticos válidos para el comportamiento observado.
2. Teoría del Diagnóstico Multi-Instante: Una teoría generalizada para diagnosticar fallos invariantes en el tiempo sobre una ventana deslizante de observaciones, que subsume el diagnóstico estándar de múltiples observaciones como un caso especial.
3. Diagnóstico Temporal: Soporte para la anormalidad variable en el tiempo, permitiendo la identificación de cuándo ocurre un fallo, no solo qué componente está defectuoso.
4. Escenarios Diagnósticos Flexibles: La capacidad de manejar elegantemente el conocimiento de fondo, el modelado abstracto y diversos tipos de fallos (persistentes vs. transitorios) dentro de un único marco basado en flujos.
5. Implementación y Evaluación: Una implementación prototipo que integra el algoritmo HS-Tree, QuickXplain y Z3, validada con los benchmarks ISCAS85 e ISCAS89.

Resultados

Los autores evaluaron el marco en dos circuitos booleanos:

• c17 (ISCAS85): Un circuito puramente combinacional con 6 componentes.
• s27 (ISCAS89): Un circuito secuencial con 14 componentes.

Hallazgos:

• Viabilidad: El marco identificó con éxito los fallos reales inyectados (stuck-at-false) en ambos circuitos.
• Precisión Temporal: Para el circuito secuencial (s27), el marco localizó correctamente los fallos solo cuando la ventana de observación ($k$) fue lo suficientemente grande como para cubrir el origen del fallo y el tiempo de propagación.
• Rendimiento:
  • El tiempo de ejecución aumentó con valores de $k$ más grandes. Para c17, el diagnóstico de $k$-instantes tomó hasta 246 ms ($k=0$) y 775 ms ($k=31$) por instante.
  • El diagnóstico temporal fue significativamente más costoso debido a la explosión combinatoria de tratar $(c, t')$ como componentes distintos. Para c17, el diagnóstico temporal tomó hasta 8.7 segundos por instante para $k=5$ y 136 segundos para $k=12$.
  • A pesar del costo computacional, los autores señalan que con una $k$ constante, los tiempos de ejecución permanecieron independientes de la longitud total de la traza, confirmando la viabilidad de las estrategias de poda.

Significación y Reivindicaciones

El artículo afirma proporcionar una integración compacta y bien fundamentada de la Verificación en Tiempo de Ejecución y el Diagnóstico Basado en Modelos. Su significación radica en cerrar la brecha entre la detección automática de fallos (RV) y la localización sistemática de la causa raíz (MBD) dentro de un único marco basado en flujos.

Los autores enfatizan que este enfoque:

• Soporta entradas inciertas y suposiciones ambientales, permitiendo una inferencia refinada basada en el conocimiento experto.
• Permite el diagnóstico en línea aprovechando el razonamiento simbólico para producir veredictos en cada punto temporal.
• Ofrece una combinación sinérgica donde las fortalezas de la RV (monitoreo eficiente y continuo) y el MBD (análisis de causa raíz basado en principios) se unifican.
• Proporciona un marco sólido (sound) donde el monitor simbólico asegura que los valores deducidos sean consistentes con todos los mundos posibles definidos por las restricciones.

El trabajo se presenta como una prueba de concepto que demuestra la viabilidad de utilizar Lola para tareas diagnósticas complejas, ofreciendo una base teórica para futuras aplicaciones prácticas en sistemas críticos para la seguridad.