⚡ electrical engineering

Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

Cet article présente une extension d'un cadre d'autocodage crédible pour gérer des contrôleurs de voiture non linéaires en introduisant de nouveaux symboles d'annotation pour les prédicats généraux et les systèmes dynamiques, démontrant la génération de code avec des garanties vérifiables de manière indépendante des propriétés fonctionnelles et de l'absence d'erreurs d'exécution.

Auteurs originaux : Timothy Wang, Eric Feron

Publié 2026-06-04

📖 5 min de lecture🧠 Analyse approfondie

CC BY 3.0

Auteurs originaux : Timothy Wang, Eric Feron

Article original sous licence CC BY 3.0 (http://creativecommons.org/licenses/by/3.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous construisez une voiture de course autonome qui doit effectuer des virages agressifs à grande vitesse. Vous écrivez un programme informatique (un contrôleur) pour dire à la voiture comment diriger et accélérer. Mais voici le problème : les ordinateurs sont littéraux et sans pitié. Si votre code contient une minuscule erreur, la voiture pourrait partir en tête-à-queue.

Habituellement, les ingénieurs écrivent le code, puis le testent en faisant percuter la voiture (virtuellement ou physiquement) des milliers de fois pour voir si elle casse. Ce document propose une méthode plus intelligente : l'Autocodage Crédible Automatisé.

Considérez ce processus non pas comme un « test », mais comme la construction d'une garantie mathématique parallèlement au code.

L'idée centrale : Le système de « double vérification »

Les auteurs ont créé un système qui fait deux choses à la fois :

Génère le code : Il prend une conception de haut niveau du cerveau de la voiture et écrit automatiquement les instructions informatiques réelles (le code).
Génère le « certificat » : En même temps, il rédige une preuve mathématique qui dit : « Je promets que ce code ne plantera jamais et ne se comportera pas malartement. »

C'est comme une usine qui ne se contente pas de construire une voiture ; elle imprime aussi un certificat de garantie qui prouve mathématiquement que le moteur n'explosera pas, que les freins ne lâcheront pas et que la direction fonctionnera toujours, avant même que la voiture ne quitte l'usine.

Le défi : La nuance « non linéaire »

Dans leurs travaux précédents, les auteurs pouvaient faire cela pour des systèmes simples et prévisibles (comme une voiture roulant en ligne droite). Mais la course automobile implique des dynamiques non linéaires.

L'analogie : Imaginez conduire sur une route droite. Si vous tournez un peu le volant, la voiture tourne un peu. C'est « linéaire » et facile à prédire.
La réalité : Maintenant, imaginez conduire sur une route de montagne sinueuse et glissante. Si vous tournez un peu le volant, la voiture peut glisser, pivoter ou accrocher différemment selon la vitesse et l'angle. C'est « non linéaire ». C'est chaotique et difficile à prédire.

Le contrôleur de la voiture dans ce document est conçu pour ces manœuvres chaotiques et agressives. La mathématique derrière cela est complexe (utilisant ce qu'on appelle un contrôleur à « mode de glissement » et une « fonction de Lyapunov »), et elle ne suit pas de simples règles de ligne droite.

Ce qu'ils ont fait : Élargir la boîte à outils

Les auteurs ont pris leur machine existante de « génération de preuves » et l'ont mise à niveau pour qu'elle puisse gérer cette voiture non linéaire et complexe.

Nouveaux outils : Ils ont ajouté de nouveaux « blocs d'annotation » à leur logiciel. Considérez cela comme des notes autocollantes spéciales que l'on peut coller sur le plan de conception.
- Une note dit : « Cette partie de la voiture est le moteur (la plante/le système). »
- Une autre note dit : « Cette partie est la règle de sécurité (l'invariant). »
L'« invariant » (La bulle de sécurité) : En termes mathématiques, un « invariant » est une règle qui ne se brise jamais. Pour cette voiture, la règle est : « Peu importe l'intensité du virage, l'état de la voiture restera toujours à l'intérieur de cette bulle de sécurité invisible. »
- Pour les voitures simples, cette bulle est un cercle parfait (une forme quadratique).
- Pour cette voiture agressive, la bulle est une forme étrange et irrégulière (un invariant non quadratique). Les auteurs ont dû apprendre à leur machine à comprendre ces formes bizarres.

Le résultat : Une démonstration manuelle

Le document montre comment ils ont pris la conception de ce contrôleur de voiture agressive, ont ajouté leurs notes spéciales de « bulle de sécurité », et l'ont passée dans leur système.

Le résultat : Le système a produit du code (écrit dans un langage appelé Matlab pour cette démo) avec les règles de sécurité intégrées directement dedans.
Le bémol : Comme le comportement de la voiture est si complexe, le système ne pouvait pas encore tout faire automatiquement. Les auteurs ont dû insérer manuellement certaines des preuves de sécurité complexes dans le code, comme un expert humain intervenant pour valider les parties les plus délicates des mathématiques.

Pourquoi cela importe

L'objectif ultime de ce travail est la confiance.

Prévention des erreurs d'exécution : Les mathématiques prouvent que le code ne plantera pas à cause de phénomènes tels que des nombres devenant trop grands ou une division par zéro.
Garantie de comportement : Cela prouve que la voiture restera stable même lors de manœuvres agressives.

L'essentiel

Ce document est une preuve de concept. Il dit : « Nous avons une machine capable d'écrire automatiquement du code et de prouver qu'il est sûr pour des voitures simples. Nous avons maintenant mis à niveau cette machine pour qu'elle puisse gérer une voiture de course agressive et très difficile. Nous avons montré que cela fonctionne, mais pour les parties les plus complexes, nous avons encore besoin d'un humain pour aider à rédiger le certificat de sécurité final. »

Ils ne disent pas que c'est prêt pour toutes les voitures sur la route aujourd'hui ; ils disent qu'ils ont réussi à construire le pont entre les mathématiques complexes et chaotiques et un code informatique fiable et vérifié.

Résumé technique : Autocodage automatisé et crédible d'un contrôleur de voiture avec manœuvres agressives non pilotées

Énoncé du problème
Cet article traite du défi que représente l'application de cadres d'autocodage crédibles aux systèmes de contrôle caractérisés par des dynamiques entièrement non linéaires. Alors que les travaux précédents des auteurs ont démontré avec succès un cadre automatisé pour les contrôleurs linéaires et quasi-non linéaires (systèmes avec des non-linéarités bornées dans la rétroaction), ces méthodes reposaient sur des invariants quadratiques dérivés de preuves de stabilité de Lyapunov. Le problème spécifique abordé ici est l'autocodage d'un contrôleur de voiture non linéaire qui ne peut pas être reformulé en tant que système linéaire avec des non-linéarités bornées. Ce système utilise une fonction de Lyapunov non quadratique, résultant en un invariant non quadratique que les outils prototypes existants ne pouvaient pas gérer. De plus, la présence de fonctions transcendantes et la nécessité de garantir l'absence d'erreurs d'exécution (telles que le dépassement de capacité ou overflow) dans le code généré présentent des obstacles importants pour la vérification automatique.

Méthodologie
Les auteurs étendent leur cadre existant d'« autocodage avec sémantique de contrôle », qui exploite des preuves de théorie du contrôle pour générer du code et vérifier des propriétés fonctionnelles de haut niveau. La méthodologie comprend les étapes suivantes :

Extension du cadre : Les auteurs proposent d'étendre le langage d'annotation de flux de données du prototype (basé sur Simulink et Gene-Auto) avec de nouveaux symboles d'annotation. Plus précisément, ils introduisent :
- Un bloc d'observateur synchrone généralisé capable d'accepter toute formule logique exprimable par le langage sous-jacent, supprimant ainsi les restrictions sur la structure des propriétés observées.
- Un bloc de plante généralisé capable de définir des systèmes de transition d'état non linéaires, plutôt que d'être limité à des modèles d'espace d'état linéaires.
Modélisation du système : L'étude de cas est un contrôleur de voiture non linéaire basé sur le mode glissant (sliding-mode) conçu pour stabiliser un modèle de voiture à voie unique autour d'un équilibre de virage en régime permanent. L'architecture du contrôleur se compose de deux sous-systèmes :
- Un sous-système linéaire : Un contrôleur LQR pilotant le modèle linéarisé vers un point d'équilibre, régi par un invariant quadratique.
- Un sous-système de mode glissant : Un contrôleur gérant les vitesses angulaires des roues pour correspondir aux glissements commandés, régi par un invariant non quadratique ( $z^T z \leq 1$ ) dérivé d'une fonction de Lyapunov non quadratique.
Annotation manuelle et traduction : En raison des limites du prototype actuel pour analyser entièrement les invariants non quadratiques, les auteurs démontrent le processus manuellement. Ils intègrent le modèle de plante linéarisé et la dynamique auxiliaire dans le modèle Simulink. Les preuves de stabilité sont exprimées sous forme d'annotations :
- La partie linéaire utilise un bloc ellipsoïde existant pour l'invariant quadratique.
- La partie non linéaire utilise le nouvel observateur synchrone généralisé pour exprimer l'invariant non quadratique.
- La sortie est traduite en code Matlab (utilisé comme substitut au code C cible) avec des annotations similaires à la norme ACSL (ANSI/ISO C Specification Language).
Logique de vérification : L'article détaille comment les invariants sont mappés vers le code. Les invariants linéaires sont propagés à l'aide de techniques de transformation affine. Pour l'invariant non quadratique, les auteurs emploient la propagation vers l'arrière en utilisant les règles axiomatiques de la logique de Hoare. Ils notent que la preuve de l'implication entre les pré-conditions et les post-conditions pour le cas non linéaire nécessite un prouveur de théorèmes, car la présence d'opérateurs de saturation empêche l'utilisation de procédures de décision générales uniques pour les fonctions polynomiales ou lisses.

Contributions clés

Extension du langage d'annotation : La proposition de nouveaux blocs d'annotation (observateur et plante généralisés) pour supporter des prédicats généraux et des systèmes dynamiques, dépassant les contraintes des hypothèses linéaires/quadratiques.
Démonstration sur des systèmes non quadratiques : Une démonstration manuelle de la manière dont le cadre étendu gère un contrôleur de voiture entièrement non linéaire avec un invariant non quadratique, un scénario auparavant non supporté par le prototype.
Garanties d'erreur d'exécution : Dérivation théorique montrant comment l'invariant non quadratique ( $z^T z \leq 1$ ) peut être utilisé pour établir des bornes sur les variables du système (telles que les vitesses angulaires des roues), servant ainsi de certificat pour l'absence d'erreurs d'exécution, à condition que les contraintes physiques soient connues.

Résultats
L'article présente un exemple annoté manuellement du contrôleur de voiture en Matlab, montrant l'insertion de pré-conditions, de post-conditions et d'hypothèses dérivées des sémantiques de contrôle.

Pour la boucle linéaire, le système identifie avec succès l'invariant quadratique et le propage à travers le code.
Pour la boucle non linéaire, le système insère avec succès l'invariant non quadratique comme une condition.
Les auteurs démontrent que, bien que le cadre puisse générer le code annoté, la vérification automatique de l'implication $A \to B$ (où $A$ et $B$ sont des ensembles définis par les invariants) n'est pas encore totalement automatisée pour le cas non linéaire en raison de la complexité des fonctions impliquées (spécifiquement la saturation). La vérification repose actuellement sur l'insertion par l'utilisateur des faits d'invariants nécessaires pour assister l'analyseur de fond.

Signification et affirmations
L'article affirme que ce travail représente une étape nécessaire vers l'extension de l'autocodage crédible aux systèmes non linéaires généraux. La signification réside dans la capacité à générer du code qui porte des « certificats » de bon comportement du système (stabilité) et de sécurité d'exécution (bornage) directement à partir des preuves de théorie du contrôle.

Revendications modestes : Les auteurs sont explicites sur le fait que l'implémentation actuelle pour le cas entièrement non linéaire n'est pas totalement automatique. Ils déclarent que le processus « ne peut pas être entièrement automatisé pour la majeure partie » et nécessite que l'utilisateur final insère manuellement les preuves de stabilité en utilisant les nouveaux blocs d'observateur.
Scalabilité : L'article conclut en reconnaissant que l'analyse et la vérification automatiques du code documenté font face à des problèmes d'évolutivité (scalability), notamment en ce qui concerne la nécessité de prouveurs de théorèmes pour gérer les fonctions non polynomiales découlant de la saturation et des opérations transcendantes. Le travail sert de preuve de concept pour l'extensibilité du cadre plutôt que d'un outil pleinement réalisé et automatisé pour tous les contrôleurs non linéaires.