💻 computer science

Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

Cet article présente une technique de compilation du fragment synchrone de la logique temporelle de signal (SSTL) en observateurs synchrones modulaires au sein du langage Lustre, permettant ainsi la vérification statique et au moment de l'exécution des systèmes cyber-physiques tout en prenant en charge l'imbrication arbitraire de propriétés bornées et un opérateur extérieur globalement non borné pour la surveillance en ligne.

Auteurs originaux : Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

Publié 2026-08-14

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Logan Kenwright, Partha Roop, Sobhan Chatterjee, Nathan Allen

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

Imaginez que vous construisez un robot qui conduit une voiture, ou un drone qui livre des colis. Ces machines vivent dans un monde de mouvement continu, mais leurs cerveaux sont des ordinateurs numériques qui pensent par petites étapes discrètes, comme les images d'un film. Pour garantir leur sécurité, les ingénieurs écrivent des règles : « Ne jamais s'approcher à moins de 6 mètres de la voiture de devant », ou « Si vous heurtez une bosse, vous devez être de retour sur votre trajectoire en moins de 4 secondes ». Vérifier si ces règles sont respectées est délicat. Vous ne pouvez pas simplement observer tout le futur d'un coup car le robot ne sait pas ce qui va arriver ensuite. Vous devez surveiller chaque mouvement, tic par tic, comme un arbitre qui siffle une faute seulement quand elle est certaine, et non quand c'est juste un « peut-être ».

C'est là qu'intervient un domaine appelé la « Vérification au Temps d'Exécution » (Runtime Verification). C'est comme avoir un copilote super vigilant qui surveille chaque mouvement du robot en temps réel. Les règles sont souvent écrites dans un langage spécial appelé la Logique Temporelle de Signal (Signal Temporal Logic ou STL), qui est excellent pour décrire des règles basées sur le temps. Cependant, il y a un piège : la plupart des outils qui vérifient ces règles sont comme des auditeurs séparés qui examinent un enregistrement après coup, ou ils utilisent un langage différent du cerveau du robot. Cela crée un fossé. Si l'auditeur parle une langue différente, vous ne pouvez pas être sûr à 100 % que le robot suit réellement les règles pendant qu'il conduit. Vous avez besoin d'un copilote qui parle exactement la même langue que le conducteur, qui pense exactement à la même vitesse, et qui puisse dire « Je suis sûr que c'est sûr », « Je suis sûr que c'est un accident », ou « J'attends encore de voir » en plein milieu de l'action.

Ce papier présente une nouvelle façon ingénieuse de construire ce copilote parfait. Les auteurs, travaillant avec un langage appelé Lustre (un outil standard pour la construction de logiciels critiques pour la sécurité), ont créé une technique pour transformer des règles temporelles imbriquées complexes directement en code qui s'exécute aux côtés du robot. Imaginez que vous traduisiez un ensemble d'instructions compliquées en une application native qui vit à l'intérieur du cerveau du robot.

La grande avancée ici est la gestion des règles « imbriquées ». Imaginez une règle qui dit : « À chaque instant au cours des 10 prochaines secondes, vous devez être capable de trouver un emplacement sûr dans les 4 secondes suivantes. » C'est une règle à l'intérieur d'une règle. Les outils précédents peinaient face à cette complexité ou ne pouvaient pas les exécuter en temps réel. La méthode des auteurs décompose ces règles complexes en une équipe de petits observateurs simples (appelés « feuilles » ou « leaves ») qui travaillent ensemble. Chaque observateur a un travail spécifique : il surveille un événement précis dans une fenêtre de temps donnée. Si l'événement se produit, il crie « Oui ! » ; si la fenêtre se ferme sans que l'événement ne soit survenu, il crie « Non ! » ; et s'il est encore en attente, il dit « Inconnu ».

Ce qui rend cela spécial, c'est la gestion de l'état « Inconnu ». Au lieu de rester bloqué ou de deviner, le système utilise une logique dite « à trois valeurs ». Il sait exactement quand il dispose d'assez d'informations pour prendre une décision finale. Par exemple, si une règle exige qu'un intervalle de sécurité soit maintenu pendant 5 secondes, le système n'a pas besoin d'attendre que les 5 secondes soient écoulées pour savoir qu'une violation est impossible. Si la voiture a un accident à la 2ème seconde, le système le sait immédiatement et déclare un « Non ». Si la voiture reste en sécurité pendant 3 secondes mais que la fenêtre est toujours ouverte, il dira « Inconnu » jusqu'à ce que la fenêtre se ferme. Cela permet au système de donner une réponse définitive plus tôt que l'échéance totale de la règle, ce qui est une victoire majeure pour la sécurité.

Les auteurs ont testé cela sur deux scénarios : un système masse-ressort oscillant (comme une suspension de voiture) et une voiture autonome suivant une autre voiture qui pile brusquement. Ils ont montré que leur système pouvait détecter des violations de sécurité en temps réel, décidant souvent de l'issue plusieurs « ticks » (étapes de temps) avant que la limite de la règle ne force une décision. Ils ont également construit un visualiseur interactif amusant qui vous permet de regarder ces règles imbriquées se dérouler sur un écran, montrant exactement quelle partie de la règle a été satisfaite et quand.

Crucialement, parce que ce « copilote » est écrit dans le même langage que le robot, il peut être vérifié par un modèleur (un outil qui prouve mathématiquement qu'un logiciel est exempt de bugs) avant que le robot ne quitte l'usine. Cela signifie que le même morceau de code sert deux maîtres : il agit comme un moniteur de sécurité en direct pendant que le robot fonctionne, et il sert de preuve mathématique de sécurité avant même le démarrage. Les auteurs ont prouvé que leur méthode est saine et complète (sound and complete), ce qui signifie qu'elle ne manque jamais une violation et qu'elle ne donne jamais de fausse alerte, tant que les règles restent dans les limites de temps « bornées » qu'ils ont conçues. Ils ont même montré que, bien que le système ne puisse pas prédire l'avenir infini, il peut surveiller efficacement des systèmes qui fonctionnent indéfiniment en utilisant une astuce de « registre à décalage » (shift register) qui recycle les anciens observateurs pour les nouveaux moments de temps.

En résumé, ce papier comble le fossé entre les règles temporelles abstraites et l'exécution dans le monde réel. Il transforme la logique abstraite en une partie vivante et respirante de la machine, permettant des systèmes cyber-physiques plus sûrs et plus fiables, capables de prouver qu'ils sont sûrs pendant qu'ils sont réellement en train de travailler.

Résumé Technique : Révision des Observateurs Synchrones pour la Vérification au Temps de l'Exécution de Lustre en utilisant STL

Énoncé du Problème
La Logique Temporelle de Signal (STL) est un formalisme standard pour spécifier des propriétés de sûreté temporelles dans les systèmes cyber-physiques (CPS), particulièrement pour la vérification au temps de l'exécution (runtime verification). Cependant, les outils STL existants opèrent généralement sur des signaux pré-enregistrés ou simulés, ou sur des modèles d'automates abstraits, plutôt que sur le code exécutable réellement déployé. Par conséquent, il existe un manque de sémantique équivalente à l'exécution et au temps réel pour les propriétés STL imbriquées qui s'exécutent en synchronisation avec le système surveillé. De plus, bien que les langages synchrones comme Lustre utilisent des « observateurs synchrones » pour la vérification statique, le potentiel de ces observateurs pour la vérification au temps de l'exécution a été sous-exploré. Un défi spécifique réside dans la gestion de la nature « à trois valeurs » de la surveillance en ligne : parce que les opérateurs temporels bornés regardent vers le futur, un moniteur ne peut pas toujours décider d'une propriété immédiatement à chaque cycle (tick), ce qui entraîne un délai avant qu'un verdict définitif ne soit atteint.

Méthodologie
Les auteurs proposent une technique pour compiler le fragment synchrone de la STL (SSTL) directement en observateurs synchrones dans le langage de flux de données Lustre. Le cœur de la méthodologie consiste à « dérouler » (unrolling) les formules imbriquées en une collection finie d'obligations non imbriquées, chacune surveillant une fenêtre fixe de cycles de temps discrets.

Sémantique de Flux à Trois Valeurs : L'approche adopte une sémantique de Kleene à trois valeurs (def_true, def_false, unknown). À chaque cycle, l'observateur émet un verdict basé sur le préfixe observé jusqu'à présent. Unknown indique que l'horizon de la formule n'est pas encore écoulé. Cela est implémenté à l'aide d'une paire de signaux booléens (pos, neg) représentant la vérité définitive et la fausseté définitive, respectivement.
Construction Primitive (until_leaf) : Les auteurs synthétisent un nœud Lustre réutilisable unique, until_leaf, qui implémente l'opérateur « jusqu'à » borné ( $U_{[a,b]}$ ). Cette primitive suit une précondition (le signal « vivant » ou alive) et une postcondition (le signal « trouvé » ou found) sur une fenêtre spécifique. Elle émet def_true lors de la découverte d'un témoin et def_false soit par une terminaison précoce (échec de la précondition), soit par l'expiration de la fenêtre.
Synthèse Récursive : Les formules imbriquées sont synthétisées de bas en haut. Le système instancie des copies de la primitive until_leaf pour chaque cycle de départ requis par les opérateurs extérieurs. Ces copies sont câblées ensemble en utilisant les règles de la logique de Kleene pour la conjonction, la disjonction et la négation.
- Pour les opérateurs bornés ( $\square_{[a,b]}$ , $\diamond_{[a,b]}$ ), la synthèse déroule la formule en un ensemble de feuilles correspondant à chaque décalage de départ au sein de l'intervalle.
- Pour l'opérateur Global non borné ( $\square$ ), qui est courant dans les systèmes tournant en continu, les auteurs introduisent une construction de registre à décalage. Au lieu d'instancier des observateurs infinis, un registre de taille $H+1$ (où $H$ est l'horizon intérieur) recycle l'état, permettant au moniteur de suivre les copies « vivantes » de la formule intérieure indéfiniment.
Visualisation : Un outil interactif, basé sur un navigateur, est fourni pour rendre les verdicts à trois valeurs des observateurs imbriqués sur des traces éditables, facilitant le débogage et l'intuition de comportements temporels imbriqués complexes.

Contributions Clés

Surveillance en Ligne Exécutable : La technique synthétise des observateurs qui sont compilés ensemble avec le système dans le même langage synchrone (Lustre), s'exécutant en synchronisation avec le code exécutable réel plutôt que sur des données simulées.
Imbrication Arbitraire avec Compilation Modulaire : Contrairement aux travaux antérieurs (par exemple, Bellanger et al.) qui étaient limités aux opérateurs non imbriqués, cette méthode supporte l'imbrication arbitraire de propriétés SSTL bornées.
Opérateur Extérieur Non Borné : L'approche admet un opérateur $\square$ globalement non borné, adapté à la surveillance de systèmes tournant en continu, tout en gardant la structure intérieure bornée.
Double Utilité : Les observateurs résultants servent un double usage : ils fonctionnent comme des moniteurs de temps d'exécution et, par un effet secondaire, servent d'obligations de vérification statique pour le modeleur Kind2 sans nécessiter de modèle séparé.
Sémantique à Trois Valeurs pour le Temps Réel : L'implémentation fournit des verdicts de Kleene causaux, permettant aux moniteurs de s'engager sur des réponses définitives dès que le tracé le permet, souvent avant que l'horizon complet de la formule ne soit atteint.

Résultats et Évaluation
Les auteurs ont évalué la technique sur deux études de cas : un système masse-ressort et un scénario de régulateur de vitesse adaptatif (ACC) de suivi de voiture avec freinage d'urgence.

Correction : Tous les observateurs synthétisés ont été vérifiés par rapport au modeleur Kind2. Les verdicts de l'exécution et du statique concordaient sur chaque propriété, y compris l'invariant de l'exclusion mutuelle ( $pos \land neg = \text{false}$ ).
Performance : Les observateurs ont été compilés en C et exécutés via l'interprète lv6. Les coûts d'exécution par cycle ont été mesurés en nanosecondes (allant de ~6,7 ns à ~206,5 ns selon la complexité), bien en dessous des périodes de contrôle typiques de l'ordre de la milliseconde, confirmant la faisabilité pour un déploiement en ligne.
Terminaison Précoce : La sémantique à trois valeurs s'est avérée efficace ; dans les études de cas, les propriétés bornées se sont stabilisées vers des verdicts définitifs bien avant leurs horizons théoriques. Par exemple, une propriété profondément imbriquée ( $P3$ ) s'est stabilisée 15 cycles plus tôt.
Comportement Non Borné : L'opérateur $\square$ non borné a fonctionné comme un mécanisme de falsification uniquement, se verrouillant correctement sur def_false lorsque des violations se produisaient (par exemple, l'écart tombant sous les seuils de sécurité) et restant unknown autrement.

Signification et Revendications
L'article affirme combler le fossé entre la spécification formelle et la surveillance en ligne exécutable pour les systèmes cyber-physiques synchrones. En synthétisant les observateurs directement dans le langage du système, les auteurs éliminent le « fossé de modélisation » souvent trouvé lors de la vérification de modèles abstraits par rapport au code déployé. Le travail démontre que des propriétés temporelles imbriquées complexes peuvent être surveillées en ligne avec une faible latence et une haute fiabilité. Les auteurs positionnent leur travail comme une extension de Bellanger et al. [5], traitant spécifiquement des limitations concernant la profondeur d'imbrication et l'orientation vers la vérification purement statique. La contribution est présentée comme une technique de synthèse systématique qui est saine et complète par rapport à la sémantique explicite à trois valeurs, validée à la fois par l'exécution en temps réel et le model checking statique.

Limites
Les auteurs reconnaissent trois limites principales :

Explosion de l'État : Le nombre de feuilles est le produit des largeurs de fenêtre, ce qui peut faire croître la taille de l'observateur de manière exponentielle avec de grands intervalles (par exemple, $\diamond_{[0,100]}$ ).
Hypothèse de Système Fermé : Les études de cas modélisent la plante au sein de Lustre comme un système fermé. La surveillance de véritables systèmes ouverts avec des entrées de capteurs externes reste une étape future.
Domaine Discret : L'approche actuelle opère strictement dans le domaine échantillonné et discrétisé et ne supporte pas encore les sémantiques de robustesse STL continues.

Articles similaires