Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

Resumen Técnico: Autocodificación Automatizada y Creíble de un Controlador de Vehículo de Maniobras Agresivas No Tripulado

Planteamiento del Problema
Este artículo aborda el desafío de aplicar marcos de autocodificación creíbles a sistemas de control caracterizados por dinámicas totalmente no lineales. El trabajo previo de los autores demostró con éxito un marco automatizado para controladores lineales y cuasi-no lineales (sistemas con no linealidades acotadas en la retroalimentación), pero estos métodos dependían de invariantes cuadráticos derivados de pruebas de estabilidad de Lyapunov. El problema específico que se aborda aquí es la autocodificación de un controlador de vehículo no lineal que no puede reformularse como un sistema lineal con no linealidades acotadas. Este sistema utiliza una función de Lyapunov no cuadrática, lo que resulta en un invariante no cuadrático que las herramientas de prototipo existentes no podían manejar. Además, la presencia de funciones trascendentales y la necesidad de garantizar la ausencia de errores en tiempo de ejecución (como el desbordamiento o overflow) en el código generado presentan obstáculos significativos para la verificación automática.

Metodología
Los autores extienden su marco existente de "autocodificación con semántica de control", el cual aprovecha las pruebas de la teoría de control para generar código y verificar propiedades funcionales de alto nivel. La metodología consta de los siguientes pasos:

1. Extensión del Marco: Los autores proponen extender el lenguaje de anotación de flujo de datos del prototipo (basado en Simulink y Gene-Auto) con nuevos símbolos de anotación. Específicamente, introducen:

   • Un bloque de observador sincrónico generalizado capaz de aceptar cualquier fórmula lógica expresable por el lenguaje subyacente, eliminando las restricciones sobre la estructura de las propiedades observadas.
   • Un bloque de planta generalizada capaz de definir sistemas de transición de estados no lineales, en lugar de estar limitado a modelos de espacio de estados lineales.

2. Modelado del Sistema: El caso de estudio es un controlador de vehículo no lineal basado en el modo deslizante (sliding-mode), diseñado para estabilizar un modelo de vehículo de vía única alrededor de un equilibrio de giro en estado estacionario. La arquitectura del controlador consta de dos subsistemas:

   • Un Subsistema Lineal: Un controlador LQR que lleva el modelo linealizado hacia un punto de equilibrio, gobernado por un invariante cuadrático.
   • Un Subsistema de Modo Deslizante: Un controlador que gestiona las velocidades angulares de las ruedas para igualar las derivas (slips) comandadas, gobernado por un invariante no cuadrático ($z^T z \leq 1$) derivado de una función de Lyapunov no cuadrática.

3. Anotación y Traducción Manual: Debido a las limitaciones del prototipo actual para automatizar completamente el análisis de invariantes no cuadráticos, los autores demuestran el proceso manualmente. Incrustan el modelo de la planta linealizada y la dinámica auxiliar en el modelo Simulink. Las pruebas de estabilidad se expresan como anotaciones:

   • La parte lineal utiliza un bloque elipsoide existente para el invariante cuadrático.
   • La parte no lineal utiliza el nuevo observador sincrónico generalizado para expresar el invariante no cuadrático.
   • El resultado se traduce a código Matlab (utilizado como sustituto del código C objetivo) con anotaciones similares al estándar de lenguaje de especificación ACSL (ANSI/ISO C Specification Language).

4. Lógica de Verificación: El artículo detalla cómo se mapean los invariantes al código. Los invariantes lineales se propagan mediante técnicas de transformación afín. Para el invariante no cuadrático, los autores emplean la propagación hacia atrás utilizando reglas axiomáticas de la lógica de Hoare. Observan que demostrar la implicación entre las precondiciones y postcondiciones para el caso no lineal requiere un demostrador de teoremas, ya que la presencia de operadores de saturación impide el uso de procedimientos de decisión generales únicos para funciones polinómicas o suaves.

Contribuciones Clave

• Extensión del Lenguaje de Anotación: La propuesta de nuevos bloques de anotación (observador y planta generalizados) para soportar predicados generales y sistemas dinámicos, yendo más allá de las restricciones de los supuestos lineales/cuadráticos.
• Demostración en Sistemas No Cuadráticos: Una demostración manual de cómo el marco extendido maneja un controlador de vehículo totalmente no lineal con un invariante no cuadrático, un escenario previamente no soportado por el prototipo.
• Garantías de Errores en Tiempo de Ejecución: La derivación teórica que muestra cómo el invariante no cuadrático ($z^T z \leq 1$) puede utilizarse para establecer límites en las variables del sistema (como las velocidades angulares de las ruedas), sirviendo así como un certificado para la ausencia de errores en tiempo de ejecución, siempre que se conozcan las restricciones físicas.

Resultados
El artículo presenta un ejemplo anotado manualmente del controlador de vehículo en Matlab, mostrando la inserción de precondiciones, postcondiciones y supuestos derivados de la semántica de control.

• Para el bucle lineal, el sistema identifica con éxito el invariante cuadrático y lo propaga a través del código.
• Para el bucle no lineal, el sistema inserta con éxito el invariante no cuadrático como una condición.
• Los autores demuestran que, si bien el marco puede generar el código anotado, la verificación automática de la implicación $A \to B$ (donde $A$ y $B$ son conjuntos definidos por los invariantes) aún no está totalmente automatizada para el caso no lineal debido a la complejidad de las funciones involucradas (específicamente la saturación). La verificación depende actualmente de que el usuario inserte los hechos de los invariantes necesarios para asistir al analizador de fondo (backend).

Significancia y Reivindicaciones
El artículo afirma que este trabajo representa un paso necesario hacia la extensión de la autocodificación creíble a sistemas no lineales generales. La significancia radica en la capacidad de generar código que porta "certificados" de buen comportamiento del sistema (estabilidad) y seguridad en tiempo de ejecución (acotamiento) directamente desde las pruebas de la teoría de control.

• Reivindicaciones Modestas: Los autores son explícitos al señalar que la implementación actual para el caso totalmente no lineal no es totalmente automática. Afirman que el proceso "no puede ser totalmente automatizado en su mayor parte" y requiere que el usuario final inserte manualmente las pruebas de estabilidad utilizando los nuevos bloques de observador.
• Escalabilidad: El artículo concluye reconociendo que el análisis y la verificación automáticos del código documentado enfrentan problemas de escalabilidad, particularmente en lo que respecta a la necesidad de demostradores de teoremas para manejar funciones no polinómicas derivadas de la saturación y operaciones trascendentales. El trabajo sirve como una prueba de concepto para la extensibilidad del marco más que como una herramienta plenamente realizada y automatizada para todos los controladores no lineales.