Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

Resumo Técnico: Autocodificação Automatizada e Crível de um Controlador de Carro de Manobra Agressiva Não Tripulado

Definição do Problema
Este artigo aborda o desafio de aplicar frameworks de autocodificação críveis a sistemas de controle caracterizados por dinâmicas totalmente não lineares. Trabalhos anteriores dos autores demonstraram com sucesso um framework automatizado para controladores lineares e quase-não lineares (sistemas com não linearidades limitadas no feedback); no entanto, esses métodos dependiam de invariantes quadráticos derivados de provas de estabilidade de Lyapunov. O problema específico tratado aqui é a autocodificação de um controlador de carro não linear que não pode ser reformulado como um sistema linear com não linearidades limitadas. Este sistema utiliza uma função de Lyapunov não quadrática, resultando em um invariante não quadrático que as ferramentas de protótipo existentes não conseguiam lidar. Além disso, a presença de funções transcendentais e a necessidade de garantir a ausência de erros de tempo de execução (como overflow) no código gerado apresentam obstáculos significativos para a verificação automática.

Metodologia
Os autores estendem seu framework existente de "autocodificação com semântica de controle", que utiliza provas de teoria de controle para gerar código e verificar propriedades funcionais de alto nível. A metodologia envolve as seguintes etapas:

1. Extensão do Framework: Os autores propõem a extensão da linguagem de anotação de fluxo de dados do protótipo (baseada em Simulink e Gene-Auto) com novos símbolos de anotação. Especificamente, eles introduzem:

   • Um bloco de observador síncrono generalizado capaz de aceitar qualquer fórmula lógica expressável pela linguagem subjacente, removendo restrições sobre a estrutura das propriedades observadas.
   • Um bloco de planta generalizada capaz de definir sistemas de transição de estado não lineares, em vez de ser limitado a modelos de espaço de estados lineares.

2. Modelagem do Sistema: O estudo de caso é um controlador de carro não linear baseado em modo deslizante (sliding-mode) projetado para estabilizar um modelo de carro de trilha única (single-track car) em torno de um equilíbrio de curva em regime permanente. A arquitetura do controlador consiste em dois subsistemas:

   • Um Subsistema Linear: Um controlador LQR que conduz o modelo linearizado a um ponto de equilíbrio, regido por um invariante quadrático.
   • Um Subsistema de Modo Deslizante: Um controlador que gerencia as velocidades angulares das rodas para corresponder aos deslizes comandados, regido por um invariante não quadrático ($z^T z \leq 1$) derivado de uma função de Lyapunov não quadrática.

3. Anotação e Tradução Manual: Devido às limitações do protótipo atual em automatizar totalmente a análise de invariantes não quadráticos, os autores demonstram o processo manualmente. Eles incorporam o modelo da planta linearizada e a dinâmica auxiliar no modelo Simulink. As provas de estabilidade são expressas como anotações:

   • A parte linear utiliza um bloco de elipsoide existente para o invariante quadrático.
   • A parte não linear utiliza o novo observador síncrono generalizado para expressar o invariante não quadrático.
   • A saída é traduzida para código Matlab (usado como um substituto para o código C alvo) com anotações semelhantes ao padrão ACSL (ANSI/ISO C Specification Language).

4. Lógica de Verificação: O artigo detalha como os invariantes são mapeados para o código. Invariantes lineares são propagados usando técnicas de transformação afim. Para o invariante não quadrático, os autores empregam propagação reversa usando regras axiomáticas da lógica de Hoare. Eles observam que provar a implicação entre pré e pós-condições para o caso não linear requer um provador de teoremas, pois a presença de operadores de saturação impede o uso de procedimentos de decisão gerais únicos para funções polinomiais ou suaves.

Principais Contribuições

• Extensão da Linguagem de Anotação: A proposta de novos blocos de anotação (observador e planta generalizados) para suportar predicados gerais e sistemas dinâmicos, indo além das restrições de suposições lineares/quadráticas.
• Demonstração em Sistemas Não Quadráticos: Uma demonstração manual de como o framework estendido lida com um controlador de carro totalmente não linear com um invariante não quadrático, um cenário anteriormente não suportado pelo protótipo.
• Garantias de Erros de Tempo de Execução: Derivação teórica mostrando como o invariante não quadrático ($z^T z \leq 1$) pode ser usado para estabelecer limites nas variáveis do sistema (como velocidades angulares das rodas), servindo assim como um certificado para a ausência de erros de tempo de execução, desde que as restrições físicas sejam conhecidas.

Resultos
O artigo apresenta um exemplo anotado manualmente do controlador de carro em Matlab, mostrando a inserção de pré-condições, pós-condições e suposições derivadas das semânticas de controle.

• Para o loop linear, o sistema identifica com sucesso o invariante quadrático e o propaga através do código.
• Para o loop não linear, o sistema insere com sucesso o invariante não quadrático como uma condição.
• Os autores demonstram que, embora o framework possa gerar o código anotado, a verificação automática da implicação $A \to B$ (onde $A$ e $B$ são conjuntos definidos pelos invariantes) ainda não é totalmente automatizada para o caso não linear devido à complexidade das funções envolvidas (especificamente a saturação). A verificação atualmente depende do usuário inserir os fatos de invariante necessários para auxiliar o analisador de backend.

Significância e Alegações
O artigo afirma que este trabalho representa um passo necessário para estender a autocodificação crível para sistemas não lineares gerais. A significância reside na capacidade de gerar código que carrega "certificados" de bom comportamento do sistema (estabilidade) e segurança de tempo de execução (limitação/boundedness) diretamente das provas de teoria de controle.

• Alegações Modestas: Os autores são explícitos ao afirmar que a implementação atual para o caso totalmente não linear não é totalmente automática. Eles afirmam que o processo "não pode ser totalmente automatizado na maior parte" e requer que o usuário final insira manualmente as provas de estabilidade usando os novos blocos de observador.
• Escalabilidade: O trabalho conclui reconhecendo que a análise e verificação automática do código de saída documentado enfrentam problemas de escalabilidade, particularmente em relação à necessidade de provadores de teoremas para lidar com funções não polinomiais decorrentes de operações de saturação e transcendentais. O trabalho serve como uma prova de conceito para a extensibilidade do framework em vez de uma ferramenta totalmente realizada e automatizada para todos os controladores não lineares.