Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

Sintesi Tecnica: Autocodifica Automatica e Credibile di un Controllore per Veicolo Unmanned con Manovre Aggressive

Definizione del Problema
Questo articolo affronta la sfida di applicare framework di autocodifica credibili a sistemi di controllo caratterizzati da dinamiche completamente non lineari. Mentre il precedente lavoro degli autori ha dimostrato con successo un framework automatizzato per controllori lineari e quasi-non lineari (sistemi con non linearità limitate nel feedback), tali metodi si basavano su invarianti quadratici derivati da prove di stabilità di Lyapunov. Il problema specifico affrontato qui è l'autocodifica di un controllore per auto non lineare che non può essere riformulato come un sistema lineare con non linearità limitate. Questo sistema utilizza una funzione di Lyapunov non quadratica, risultando in un invariante non quadratico che gli strumenti prototipali esistenti non potevano gestire. Inoltre, la presenza di funzioni trascendenti e la necessità di garantire l'assenza di errori a runtime (come l'overflow) nel codice generato rappresentano ostacoli significativi per la verifica automatica.

Metodologia
Gli autori estendono il loro esistente framework di "autocodifica con semantica di controllo", che sfrutta prove di teoria del controllo per generare codice e verificare proprietà funzionali di alto livello. La metodologia prevede i seguenti passaggi:

1. Estensione del Framework: Gli autori propongono l'estensione del linguaggio di annotazione dei dati del prototipo (basato su Simulink e Gene-Auto) con nuovi simboli di annotazione. Nello specifico, introducono:

   • Un blocco osservatore sincrono generalizzato capace di accettare qualsiasi formula logica esprimibile dal linguaggio sottostante, rimuovendo le restrizioni sulla struttura delle proprietà osservate.
   • Un blocco pianta generalizzato capace di definire sistemi a transizione di stato non lineari, anziché essere limitato a modelli di spazio di stato lineari.

2. Modellazione del Sistema: Il caso di studio è un controllore per auto non lineare basato sul modo a scorrimento (sliding-mode) progettato per stabilizzare un modello di auto a singolo binario attorno a un equilibrio di percorrenza in curva a regime stazionario. L'architettura del controllore consiste in due sottosistemi:

   • Un Sottosistema Lineare: Un controllore LQR che guida il modello linearizzato verso un punto di equilibrio, governato da un invariante quadratico.
   • Un Sottosistema a Modo a Scorrimento: Un controllore che gestisce le velocità angolari delle ruote per corrispondere agli slip comandati, governato da un invariante non quadratico ($z^T z \leq 1$) derivato da una funzione di Lyapunov non quadratica.

3. Annotazione Manuale e Traduzione: A causa delle limitazioni dell'attuale prototipo nel gestire completamente in modo automatico gli invarianti non quadratici, gli autori ne dimostrano il processo manualmente. Incorporano il modello della pianta linearizzata e la dinamica ausiliaria nel modello Simulink. Le prove di stabilità sono espresse come annotazioni:

   • La parte lineare utilizza un esistente blocco ellissoide per l'invariante quadratico.
   • La parte non lineare utilizza il nuovo osservatore sincrono generalizzato per esprimere l'invariante non quadratico.
   • L'output è tradotto in codice Matlab (usato come proxy per il codice C target) con annotazioni simili allo standard ACSL (ANSI/ISO C Specification Language).

4. Logica di Verifica: L'articolo dettaglia come gli invarianti vengano mappati nel codice. Gli invarianti lineari sono propagati utilizzando tecniche di trasformazione affine. Per l'invariante non quadratico, gli autori impiegano la propagazione all'indietro utilizzando le regole assiomatiche della logica di Hoare. Notano che dimostrare l'implicazione tra pre-condizioni e post-condizioni per il caso non lineare richiede un dimostratore di teoremi, poiché la presenza di operatori di saturazione impedisce l'uso di procedure decisionali generali singole per funzioni polinomiali o regolari.

Contributi Chiave

• Estensione del Linguaggio di Annotazione: La proposta di nuovi blocchi di annotazione (osservatore e pianta generalizzati) per supportare predicati generali e sistemi dinamici, andando oltre i vincoli delle assunzioni lineari/quadratiche.
• Dimostrazione su Sistemi Non Quadratici: Una dimostrazione manuale di come il framework esteso gestisce un controllore per auto completamente non lineare con un invariante non quadratico, uno scenario precedentemente non supportato dal prototipo.
• Garanzie di Errore a Runtime: Derivazione teorica che mostra come l'invariante non quadratico ($z^T z \leq 1$) possa essere utilizzato per stabilire limiti sulle variabili di sistema (come le velocità angolari delle ruote), fungendo così da certificato per l'assenza di errori a runtime, a condizione che i vincoli fisici siano noti.

Risultati
L'articolo presenta un esempio annotato manualmente del controllore dell'auto in Matlab, mostrando l'inserimento di pre-condizioni, post-condizioni e assunzioni derivate dalla semantica di controllo.

• Per il loop lineare, il sistema identifica con successo l'invariante quadratico e lo propaga attraverso il codice.
• Per il loop non lineare, il sistema inserisce con successo l'invariante non quadratico come condizione.
• Gli autori dimostrano che, sebbene il framework possa generare il codice annotato, la verifica automatica dell'implicazione $A \to B$ (dove $A$ e $B$ sono insiemi definiti dagli invarianti) non è ancora completamente automatica per il caso non lineare a causa della complessità delle funzioni coinvolte (specificamente la saturazione). La verifica attualmente si affida all'inserimento da parte dell'utente dei fatti necessari relativi all'invariante per assistere l'analizzatore backend.

Significatività e Rivendicazioni
L'articolo sostiene che questo lavoro rappresenti un passo necessario verso l'estensione dell'autocodifica credibile a sistemi non lineari generali. La significatività risiede nella capacità di generare codice che trasporta "certificati" di buon comportamento del sistema (stabilità) e sicurezza a runtime (limitatezza) direttamente dalle prove di teoria del controllo.

• Rivendicazioni Modeste: Gli autori sono espliciti nell'affermare che l'attuale implementazione per il caso completamente non lineare non è del tutto automatica. Affermano che il processo "non può essere completamente automatizzato per la maggior parte" e richiede all'utente finale di inserire manualmente le prove di stabilità utilizzando i nuovi blocchi osservatore.
• Scalabilità: L'articolo conclude riconoscendo che l'analisi e la verifica automatica del codice documentato affrontano problemi di scalabilità, in particolare riguardo alla necessità di dimostratori di teoremi per gestire funzioni non polinomiali derivanti da saturazione e operazioni trascendenti. Il lavoro funge da prova di concetto per l'estensibilità del framework piuttosto che per uno strumento completamente realizzato e automatizzato per tutti i controllori non lineari.