💻 computer science

Formally Guaranteed Control Adaptation for ODD-Resilient Autonomous Systems

Ce papier propose une approche d'adaptation formellement garantie des modèles probabilistes des systèmes autonomes pour étendre leur couverture opérationnelle et assurer des performances fiables même dans des situations imprévues en dehors de leur domaine de conception.

Auteurs originaux : Gricel Vázquez, Calum Imrie, Sepeedeh Shahbeigi, Nawshin Mannan Proma, Tian Gan, Victoria J Hodge, John Molloy, Simos Gerasimou

Publié 2026-04-10

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Gricel Vázquez, Calum Imrie, Sepeedeh Shahbeigi, Nawshin Mannan Proma, Tian Gan, Victoria J Hodge, John Molloy, Simos Gerasimou

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.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

🚢 Le "Pilote Automatique" qui ne panique jamais : L'histoire de SAVE

Imaginez que vous conduisez une voiture autonome sur une route très connue. Vous connaissez chaque virage, chaque feu rouge et chaque panneau. C'est ce qu'on appelle le ODD (Domaine de Conception Opérationnelle). Tout se passe bien tant que vous restez sur cette route familière.

Mais que se passe-t-il si, soudainement, vous vous retrouvez dans une tempête de neige que personne n'avait prévue, ou si un animal inconnu traverse la route ? C'est ce qu'on appelle une situation "hors ODD". Là, le système habituel risque de paniquer, de faire une erreur, ou pire, de provoquer un accident.

Les chercheurs de l'Université de York ont créé une solution intelligente appelée SAVE. Voici comment cela fonctionne, avec quelques analogies amusantes.

1. La Carte au Trésor (Le Modèle de Probabilité)

Avant même que le bateau (ou la voiture) ne quitte le port, les chercheurs créent une "carte au trésor" très détaillée.

L'analogie : Imaginez un jeu de société géant où chaque case représente une situation possible (ex: "un autre bateau est proche", "la visibilité est faible").
Le génie de SAVE : Au lieu de juste dessiner les cases, ils ajoutent des flèches qui montrent la probabilité de passer d'une case à l'autre. Ils utilisent des tests de simulation pour dire : "Si on est dans cette situation, il y a 90 % de chances qu'on aille vers la sécurité, mais 10 % de chances qu'on tombe dans un piège."

2. L'Inspecteur Rigoureux (Avant le départ)

Avant de lancer le système, SAVE joue au "juge sévère".

L'analogie : C'est comme un entraîneur de sport qui regarde les statistiques de ses joueurs. Il dit : "Attends, si on joue contre cette équipe (situation critique), il y a un risque que le joueur perde le match. On ne peut pas le laisser jouer dans ce cas-là."
Ce qu'il fait : Il identifie les situations les plus dangereuses (celles où les règles de sécurité risquent d'être violées) et note leur "niveau de dangerosité".

3. Le Super-Héros Adaptatif (Pendant le voyage)

C'est là que la magie opère. Une fois le système en route, il ne reste pas figé. Il observe tout en temps réel.

La situation : Le système détecte quelque chose d'inattendu (une situation "hors ODD"). Par exemple, un bateau qui fonce vers lui à une vitesse folle, ce qui n'était pas prévu sur la carte initiale.
La réaction de SAVE : Au lieu de paniquer, SAVE agit comme un chef d'orchestre qui improvise.
1. Il regarde la nouvelle situation.
2. Il se demande : "Est-ce que cette nouvelle situation va me faire violer mes règles de sécurité ?"
3. Si oui : Il dit "Stop !" Il modifie instantanément ses règles de conduite. Il dit au système : "Oublie la route habituelle, on ne va plus dans cette direction. On va faire demi-tour ou on va s'arrêter tout de suite."
4. Il crée une "barrière invisible" autour du danger pour s'assurer que le système ne peut plus y entrer.

4. La Preuve Mathématique (Le Garant de Sécurité)

Ce qui rend SAVE spécial, c'est qu'il ne se contente pas de dire "Je pense que c'est sûr". Il prouve mathématiquement que sa nouvelle stratégie est sûre.

L'analogie : C'est comme si, avant de prendre une décision, le système sortait un certificat officiel signé par un mathématicien qui dit : "Je garantis à 99,9 % que cette nouvelle manœuvre ne provoquera pas d'accident."

🌊 L'Exemple du Bateau

Dans l'article, ils testent cette idée avec un bateau autonome.

Le problème : Un jour, un autre bateau se comporte bizarrement (vitesse trop rapide, trajectoire imprévue). Le système habituel aurait pu entrer en collision.
La solution SAVE : Dès qu'il détecte ce comportement étrange, il calcule immédiatement le danger. Il voit que continuer comme avant serait une erreur. Il modifie donc son "cerveau" (son contrôleur) pour éviter le danger, même si cela signifie qu'il doit s'arrêter ou changer de cap de manière radicale.
Le résultat : Dans les tests, SAVE a réussi à éviter les collisions dans la grande majorité des cas imprévus, là où les systèmes classiques échouaient.

En résumé

SAVE, c'est comme donner à un robot une boussole magique et un cerveau flexible.

Il connaît les règles de la route.
Il sait anticiper les dangers grâce à des simulations.
S'il rencontre l'inconnu, il ne panique pas : il se recalcule instantanément pour rester dans la zone de sécurité.
Et surtout, il a toujours une preuve mathématique que sa nouvelle décision est sûre.

C'est une étape majeure pour rendre nos voitures, bateaux et robots plus sûrs, même quand ils rencontrent des situations que les humains n'avaient pas prévues ! 🚀🛡️

1. Problématique

L'intégration croissante de systèmes autonomes dans des domaines critiques (santé, transport maritime) exige des garanties de sécurité rigoureuses. Le défi principal réside dans la résilience de ces systèmes face à des situations extérieures à leur Domaine de Conception Opérationnel (ODD - Operational Design Domain).

Limites de l'ODD : À la conception, l'ODD définit les conditions de fonctionnement sûr. Cependant, la complexité du monde réel et l'évolution des environnements entraînent inévitablement des situations « hors-ODD » (out-of-ODD).
Conséquences : Ces situations rendent le comportement du système incertain. Les mises à jour logicielles classiques (reconception, réentraînement) sont souvent impossibles à l'exécution (runtime) en raison de contraintes de temps et de coûts.
Échec des approches actuelles : Les systèmes adaptatifs existants (SAS) et les méthodes de vérification à l'exécution détectent les déviations, mais manquent souvent d'un cadre pour adapter dynamiquement les modèles sous-jacents et synthétiser de nouveaux contrôleurs tout en respectant des exigences de sécurité strictes et quantitatives.

2. Méthodologie : L'approche SAVE

Les auteurs proposent SAVE (Situation-Aware Verification and control synthEsis), une approche centrée sur la situation et pilotée par l'ODD. Elle combine la couverture de situations, les modèles probabilistes et la vérification formelle.

Le processus est divisé en deux phases principales (illustrées par le cycle MAPE-K) :

A. Phase Pré-déploiement (Conception et Analyse)

Augmentation de la Grille de Couverture de Situation (SCG) :
- L'ODD est structuré en un ensemble discret de situations (tuples d'attributs).
- Une SCG est générée et enrichie avec des probabilités de transition dérivées de données empiriques et de scénarios de défaillance.
- Cela crée une SCG augmentée définissant les transitions entre situations normales et états d'échec.
Modélisation Probabiliste :
- Pour chaque situation, un Chaîne de Markov à Temps Discret (DTMC) est généré.
- Ces modèles sont vérifiés formellement à l'aide de la Vérification de Modèle Probabiliste (PMC) via l'outil PRISM et la logique PCTL.
Analyse des Situations Critiques :
- Un score de criticité est attribué à chaque situation en fonction de la violation des propriétés de sécurité (ex: probabilité de collision).
- Les situations les plus critiques sont identifiées pour guider la conception initiale des contrôleurs.

B. Phase de Déploiement (Adaptation à l'Exécution)

Le système fonctionne en boucle fermée :

Surveillance (Monitoring) : Détection en temps réel de la situation actuelle ( $\rho_t$ ) et des défaillances.
Mise à jour du Modèle (Model Update) :
- Les probabilités de transition sont mises à jour dynamiquement (approches fréquentistes ou bayésiennes) en fonction des nouvelles données observées.
- De nouveaux modèles DTMC ( $M_t$ ) sont construits.
Analyse et Synthèse de Contrôleur :
- Si une violation est détectée (score de criticité > 0), SAVE déclenche une synthèse adaptative.
- Algorithme d'élimination : La situation la plus critique est identifiée. Son état est transformé en « état puits » (sink state) dans le modèle, bloquant ainsi toute transition vers cette condition dangereuse.
- Les scores de criticité sont recalculés pour les situations restantes.
- Ce cycle se répète jusqu'à ce qu'un contrôleur vérifié comme sûr soit synthétisé ou qu'un nombre maximal d'itérations soit atteint.
Exécution : Le nouveau contrôleur est déployé, garantissant que le système évite les situations hors-ODD dangereuses.

3. Contributions Clés

Approche centrée sur la situation : Une méthode novatrice générant des modèles probabilistes directement à partir de situations extraites de l'ODD, permettant la synthèse de contrôleurs avec des garanties quantitatives formelles.
Métrique de criticité et mise à jour des données : Un mécanisme pour encoder les transitions probabilistes entre situations et attribuer un score de criticité, intégrant des mises à jour basées sur les données en temps réel.
Boucle d'adaptation pilotée par la vérification : Un mécanisme capable de détecter les violations de sécurité à l'exécution et de synthétiser dynamiquement des contrôleurs mis à jour qui restent sûrs, même en cas de dérive de l'ODD.

4. Résultats et Évaluation

L'évaluation a été menée sur une étude de cas maritime impliquant un navire autonome de surface (MASS) naviguant parmi d'autres navires.

Scénario : Le navire doit éviter les collisions (situations de face-à-face, croisement, dépassement) avec des navires de types A et B.
Propriétés de sécurité :
- $\Phi_1$ : Probabilité de défaillance (temps de réaction insuffisant) < 0.99.
- $\Phi_2$ : Probabilité de collision quasi-catastrophique < 0.95.
Performance (RQ1 & RQ2) :
- Sur 20 variantes de scénarios perturbés (hors-ODD), SAVE a réussi à éviter les violations de exigences dans 14 cas (70%), là où le système de base (contrôleur fixe) échouait systématiquement.
- SAVE a démontré sa capacité à adapter le contrôleur en temps réel pour éviter des collisions imminentes (ex: manœuvre d'arrêt d'urgence COLREGs).
- Les violations restantes (6 cas) correspondaient à des situations où le score de criticité dépassait 0.04, indiquant des scénarios trop dangereux pour qu'un contrôleur sûr puisse être synthétisé sans bloquer totalement le système.
Évolutivité (RQ3) :
- L'analyse de temps d'exécution montre que le temps de calcul pour obtenir les scores de criticité augmente avec le nombre de situations. Bien que le nombre de transitions croisse exponentiellement (pire cas), les résultats préliminaires suggèrent la faisabilité de cette approche pour des systèmes critiques, notamment grâce à la nature discrète des situations.

5. Signification et Conclusion

L'article SAVE marque une avancée significative dans le domaine des systèmes autonomes adaptatifs :

Garanties Formelles à l'Exécution : Contrairement aux approches purement heuristiques ou basées sur l'apprentissage, SAVE fournit des garanties mathématiques de sécurité même face à des situations imprévues.
Boucle de rétroaction ODD : Il établit une traçabilité explicite entre la conception (ODD), les tests et la vérification à l'exécution, comblant le fossé entre la modélisation statique et la dynamique du monde réel.
Résilience Opérationnelle : L'approche permet aux systèmes de continuer à fonctionner de manière sûre en dégradant intelligemment leurs capacités (en évitant les situations critiques) plutôt que de tomber en panne ou de violer les règles de sécurité.

Les travaux futurs visent à intégrer des mécanismes de sécurité complets (comme les manœuvres d'arrêt d'urgence) et à étendre l'évaluation à d'autres domaines de systèmes cyber-physiques.