💻 computer science

Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

Este artículo presenta una técnica para compilar el fragmento síncrono de la Lógica Temporal de Señales (SSTL) en observadores síncronos modulares dentro del lenguaje Lustre, permitiendo tanto la verificación estática como la de tiempo de ejecución de sistemas ciberfísicos mientras soporta un anidamiento arbitrario de propiedades acotadas y un operador externo globalmente no acotado para el monitoreo en línea.

Autores originales: Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

Publicado 2026-08-14

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás construyendo un robot que conduce un coche, o un dron que entrega paquetes. Estas máquinas viven en un mundo de movimiento continuo, pero sus cerebros son computadoras digitales que piensan en pasos discretos y diminutos, como los fotogramas de una película. Para mantenerlas seguras, los ingenieros escriben reglas: "Nunca te acerques a menos de 6 metros del coche de adelante", o "Si golpeas un bache, debes volver a tu trayectoria en un plazo de 4 segundos". Comprobar si se siguen estas reglas es complicado. No puedes mirar todo el futuro a la vez porque el robot no sabe qué vendrá después. Tienes que observar tick por tick, como un árbitro que solo pita una falta cuando esta es segura, no cuando es solo un "tal vez".

Aquí es donde entra un campo llamado "Verificación en Tiempo de Ejecución" (Runtime Verification). Es como tener un copiloto supervigilante que observa cada movimiento del robot en tiempo real. Las reglas suelen escribirse en un lenguaje especial llamado Lógica Temporal de Señales (STL), que es excelente para describir reglas basadas en el tiempo. Sin embargo, hay un inconveniente: la mayoría de las herramientas que comprueban estas reglas son como auditores separados que revisan una grabación después de los hechos, o utilizan un lenguaje diferente al del cerebro del robot. Esto crea una brecha. Si el auditor habla un idioma distinto, no puedes estar 100% seguro de que el robot esté siguiendo las reglas mientras conduce. Necesitas un copiloto que hable exactamente el mismo idioma que el conductor, piense a la misma velocidad exacta y pueda decir "estoy seguro de que es seguro", "estoy seguro de que es un choque" o "todavía estoy esperando a ver" en el preciso momento.

Este artículo presenta una nueva y astuta forma de construir ese copiloto perfecto. Los autores, trabajando con un lenguaje llamado Lustre (una herramienta estándar para construir software de seguridad crítica), crearon una técnica para convertir reglas temporales complejas y anidadas directamente en código que se ejecuta junto al robot. Piensa en esto como traducir un conjunto de instrucciones complicadas en una aplicación nativa que vive dentro del cerebro del robot.

El gran avance aquí es el manejo de las reglas "anidadas". Imagina una regla que dice: "En cada momento de los próximos 10 segundos, debes ser capaz de encontrar un lugar seguro dentro de los próximos 4 segundos". Esta es una regla dentro de otra regla. Las herramientas anteriores tenían dificultades con esta complejidad o no podían ejecutarlas en tiempo real. El método de los autores descompone estas reglas complejas en un equipo de observadores diminutos y simples (llamados "hojas") que trabajan juntos. Cada observador tiene un trabajo específico: vigila un evento concreto dentro de una ventana de tiempo determinada. Si el evento ocurre, grita "¡Sí!"; si la ventana se cierra y el evento no ocurrió, grita "¡No!"; y si todavía está esperando, dice "Desconocido".

Lo que hace que esto sea especial es cómo manejan el estado de "Desconocido". En lugar de quedarse estancados o adivinar, el sistema utiliza una lógica de "tres valores". Sabe exactamente cuándo tiene información suficiente para tomar una decisión final. Por ejemplo, si una regla requiere mantener un espacio seguro durante 5 segundos, el sistema no tiene que esperar hasta que pasen los 5 segundos completos para saber si una violación es imposible. Si el coche choca en el segundo 2, el sistema lo sabe inmediatamente como un "No". Si el coche se mantiene seguro durante 3 segundos pero la ventana sigue abierta, dice "Desconocido" hasta que la ventana se cierre. Esto permite que el sistema dé una respuesta definitiva antes de que el límite de tiempo total de la regla obligue a tomar una decisión, lo cual es una gran victoria para la seguridad.

Los autores probaron esto en dos escenarios: un sistema de masa-resorte que rebota (como la suspensión de un coche) y un coche autónomo que sigue a otro coche que frena de repente. Demostraron que su sistema podía detectar violaciones de seguridad en tiempo real, decidiendo a menudo el resultado varios "ticks" (pasos de tiempo) antes de que el plazo de la regla forzara una decisión. También construyeron un visualizador interactivo y divertido que permite observar cómo se desarrollan estas reglas anidadas en una pantalla, mostrando exactamente qué parte de la regla se cumplió y cuándo.

Crucialmente, debido a que este "copiloto" está escrito en el mismo lenguaje que el robot, puede ser verificado por un verificador de modelos (una herramienta que demuestra matemáticamente que el software está libre de errores) antes de que el robot salga siquiera de la fábrica. Esto significa que la misma pieza de código sirve a dos señores: actúa como un monitor de seguridad en vivo mientras el robot funciona, y actúa como una prueba matemática de seguridad antes de que comience. Los autores demostraron que su método es sólido y completo, lo que significa que nunca pierde una violación y nunca da una falsa alarma, siempre que las reglas se mantengan dentro de los límites de tiempo "acotados" que diseñaron. Incluso demostraron que, si bien el sistema no puede predecir el futuro infinito, puede vigilar eficazmente violaciones en sistemas que funcionan para siempre utilizando un ingenioso truco de "registro de desplazamiento" que recicla observadores antiguos para nuevos momentos en el tiempo.

En resumen, este artículo cierra la brecha entre las reglas complejas basadas en el tiempo y la ejecución en el mundo real. Convierte la lógica abstracta en una parte viva y palpitante de la máquina, permitiendo que los sistemas ciberfísicos sean más seguros y fiables, pudiendo demostrar que son seguros mientras están trabajando realmente.

Resumen Técnico: Revisitando los Observadores Síncronos para la Verificación en Tiempo de Ejecución de Lustre mediante STL

Planteamiento del Problema
La Lógica Temporal de Señales (STL) es un formalismo estándar para especificar propiedades de seguridad temporal en sistemas ciberfísicos (CPS), particularmente para la verificación en tiempo de ejecución. Sin embargo, las herramientas de STL existentes suelen operar sobre señales pregrabadas o simuladas, o sobre modelos de autómatas abstractos, en lugar de sobre el código ejecutable que se despliega realmente. En consecuencia, existe una falta de semántica con equivalencia de ejecución en tiempo real para propiedades de STL anidadas que se ejecuten en sincronía con el sistema monitoreado. Además, mientras que los lenguajes síncronos como Lustre utilizan "observadores síncronos" para la verificación estática, el potencial de estos observadores para la verificación en tiempo de ejecución ha sido poco explorado. Un desafío específico radica en el manejo de la naturaleza "trivalorada" del monitoreo en línea: debido a que los operadores temporales acotados miran hacia el futuro, un monitor no siempre puede decidir una propiedad inmediatamente tras un tic, lo que conduce a un retraso antes de que se alcance un veredicto definitivo.

Metodología
Los autores proponen una técnica para compilar el fragmento síncrono de STL (SSTL) directamente en observadores síncronos dentro del lenguaje de flujo de datos Lustre. El núcleo de la metodología consiste en "desenrollar" fórmulas anidadas en una colección finita de obligaciones no anidadas, cada una de las cuales monitorea una ventana fija de ticks de tiempo discretos.

Semántica de Flujo Trivalorada: El enfoque adopta una semántica de Kleene trivalorada (def_true, def_false, unknown). En cada tic, el observador emite un veredicto basado en el prefijo observado hasta el momento. Unknown indica que el horizonte de la fórmula aún no ha transcurrido. Esto se implementa utilizando un par de señales booleanas (pos, neg) que representan la verdad definitiva y la falsedad definitiva, respectivamente.
Construcción Primitiva (until_leaf): Los autores sintetizan un nodo de Lustre reutilizable y único, until_leaf, que implementa el operador "hasta" acotado ( $U_{[a,b]}$ ). Este primitivo rastrea una precondición (la señal "vivo" o alive) y una postcondición (la señal "encontrado" o found) a lo largo de una ventana específica. Emite def_true al encontrar un testigo y def_false ya sea por terminación temprana (falla de la precondición) o por expiración de la ventana.
Síntesis Recursiva: Las fórmulas anidadas se sintetizan de abajo hacia arriba. El sistema instancia copias del primitivo until_leaf para cada tic de inicio requerido por los operadores externos. Estas copias se conectan utilizando reglas de lógica de Kleene para conjunciones, disyunciones y negaciones.
- Para operadores acotados ( $\square_{[a,b]}$ , $\diamond_{[a,b]}$ ), la síntesis desenrolla la fórmula en un conjunto de hojas correspondientes a cada desplazamiento de inicio dentro del intervalo.
- Para el operador Global no acotado ( $\square$ ), que es común en sistemas de ejecución libre, los autores introducen una construcción de registro de desplazamiento (shift-register). En lugar de instanciar observadores infinitos, un registro de tamaño $H+1$ (donde $H$ es el horizonte interno) recicla el estado, permitiendo al monitor rastrear las copias "vivas" de la fórmula interna indefinidamente.
Visualización: Se proporciona una herramienta interactiva basada en el navegador para renderizar los veredictos trivalorados de los observadores anidados sobre trazas editables, lo que ayuda en la depuración e intuición de comportamientos temporales anidados complejos.

Contribuciones Clave

Monitoreo en Línea Ejecutable: La técnica sintetiza observadores que se compilan junto con el sistema en el mismo lenguaje síncrono (Lustre), ejecutándose en sincronía con el código ejecutable real en lugar de sobre datos simulados.
Anidamiento Arbitrario con Compilación Modular: A diferencia del trabajo previo (por ejemplo, Bellanger et al.), que se limitaba a operadores no anidados, este método soporta el anidamiento arbitrario de propiedades SSTL acotadas.
Operador Externo No Acotado: El enfoque admite un operador externo globalmente no acotado ( $\square$ ) adecuado para monitorear sistemas de ejecución libre, manteniendo la estructura interna acotada.
Utilidad Dual: Los observadores resultantes cumplen un doble propósito: funcionan como monitores en tiempo de ejecución y, como subproducto, sirven como obligaciones de verificación estática para el verificador de modelos Kind2 sin requerir un modelo separado.
Semántica Trivalorada para Tiempo de Ejecución: La implementación proporciona veredictos causales de Kleene, permitiendo que los monitores se comprometan con respuestas definitivas tan pronto como la traza lo permita, a menudo antes de que se alcance el horizonte completo de la fórmula.

Resultos y Evaluación
Los autores evaluaron la técnica en dos casos de estudio: un sistema masa-resorte y un escenario de control de crucero adaptativo (ACC) de seguimiento de vehículos con frenado de emergencia.

Correctitud: Todos los observadores sintetizados fueron verificados contra el verificador de modelos Kind2. Los veredictos de tiempo de ejecución y estáticos coincidieron en cada propiedad, incluyendo la invariante de exclusión mutua ( $pos \land neg = \text{false}$ ).
Rendimiento: Los observadores se compilaron a C y se ejecutaron a través del intérprete lv6. Los costos de ejecución por tic se midieron en nanosegundos (oscilando entre ~6.7 ns y ~206.5 ns dependiendo de la complejidad), muy por debajo de los periodos de control típicos de escala de milisegundos, confirmando su viabilidad para el despliegue en línea.
Terminación Temprana: La semántica trivalorada resultó efectiva; en los casos de estudio, las propiedades acotadas se establecieron en veredictos definitivos estrictamente antes de sus horizontes teóricos. Por ejemplo, una propiedad profundamente anidada ( $P3$ ) se estableció 15 ticks antes.
Comportamiento No Acotado: El operador $\square$ no acotado funcionó como un mecanismo de solo falsificación, registrando correctamente def_false cuando ocurrieron violaciones (por ejemplo, cuando la brecha cayó por debajo de los umbrales de seguridad) y permaneciendo en unknown de lo contrario.

Significancia y Reivindicaciones
El artículo afirma cerrar la brecha entre la especificación formal y el monitoreo ejecutable en tiempo de ejecución para sistemas ciberfísicos síncronos. Al sintetizar los observadores directamente en el lenguaje del sistema, los autores eliminan la "brecha de modelado" que suele encontrarse al verificar modelos abstractos frente al código desplegado. El trabajo demuestra que las propiedades temporales anidadas complejas pueden monitorearse en línea con baja latencia y alta fiabilidad. Los autores posicionan su trabajo como una extensión de Bellanger et al. [5], abordando específicamente las limitaciones respecto a la profundidad de anidamiento y la orientación hacia la verificación únicamente estática. La contribución se presenta como una técnica de síntesis sistemática que es sólida y completa con respecto a la semántica explícita trivalorada, validada tanto mediante la ejecución en tiempo de ejecución como mediante la verificación de modelos estáticos.

Limitaciones
Los autores reconocen tres limitaciones principales:

Explosión de Estados: El número de hojas es el producto de las anchuras de las ventanas, lo que puede causar que el tamaño del observador crezca exponencialmente con intervalos grandes (por ejemplo, $\diamond_{[0,100]}$ ).
Supuesto de Sistema Cerrado: Los casos de estudio modelaron la planta dentro de Lustre como un sistema cerrado. El monitoreo de sistemas abiertos genuinos con entradas de sensores externas sigue siendo un paso futuro.
Dominio Discreto: El enfoque actual opera estrictamente dentro del dominio muestreado y discretizado, y aún no soporta la semántica de robustez de STL continua.

Más como este