💻 computer science

A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA

Cet article présente un cadre unifié qui intègre la vérification à l'exécution et le diagnostic basé sur des modèles au sein du langage de spécification de flux LOLA afin de permettre une localisation de fautes continue et en ligne parallèlement à la détection, sans nécessiter de chaînes d'outils distinctes.

Auteurs originaux : Raik Hipler, Martin Leucker, Patrick Rodler

Publié 2026-06-24

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Raik Hipler, Martin Leucker, Patrick Rodler

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 êtes le chef mécanicien d'une voiture très complexe et de haute technologie qui conduit toute seule. Cette voiture a deux missions principales :

Le Système d'Alarme (Vérification au moment de l'exécution) : Il surveille constamment la vitesse et la température du moteur. Si quelque chose semble anormal (comme un moteur qui surchauffe), il déclenche immédiatement une sirène : « Quelque chose ne va pas ! »
Le Détective (Diagnostic basé sur un modèle) : Une fois que la sirène retentit, le détective intervient pour comprendre ce qui est cassé. Est-ce le radiateur ? Le ventilateur ? Un fil desserré ?

Le Problème : Habituellement, ces deux tâches sont effectuées par des personnes différentes utilisant des outils différents. Le système d'alarme est excellent pour dire « Hé, il y a un problème ! », mais il est mauvais pour expliquer pourquoi. Le détective est excellent pour trouver la pièce cassée, mais il n'intervient généralement qu'après que le problème est déjà connu, et il peut ne pas savoir comment la voiture se comporte pendant qu'elle roule.

La Solution du Papier :
Ce papier présente un nouveau cadre unifié appelé Lola qui combine le Système d'Alarme et le Détective en un seul flux de pensée intelligent et continu. Au lieu de changer d'outil, le système utilise un langage unique pour surveiller la voiture, repérer l'erreur, et résoudre le mystère tout à la fois.

Voici comment cela fonctionne, décomposé en concepts simples :

1. Le « Flux » du Temps

Considérez les données de la voiture non pas comme un instantané unique, mais comme une bobine de film (un flux). Chaque seconde, de nouvelles images de données arrivent (température, vitesse, lectures de capteurs).

L'ancienne méthode : Vous prenez une photo de la voiture, vous vérifiez si elle est cassée, puis vous prenez une autre photo plus tard.
La méthode Lola : Vous regardez le film en temps réel. Le système sait que ce qui s'est passé il y a 5 secondes peut être la raison pour laquelle la voiture se comporte bizarrement en ce moment même.

2. Gérer les Informations « Floues »

Parfois, les capteurs sont un peu bruyants. Peut-être que le capteur de température dit « La température est comprise entre 80 et 90 degrés », ou peut-être qu'il est complètement vide parce qu'un fil est desserré.

La Magie : Lola n'a pas besoin de chiffres parfaits. Il peut raisonner avec des « peut-être » et des « plages de valeurs ». Il utilise une logique spéciale (comme un solveur de casse-tête mathématique super intelligent) pour dire : « Même si nous ne connaissons pas la température exacte, nous savons que le ventilateur doit être cassé parce que le calcul ne correspond pas. »

3. Trois Façons de Résoudre le Mystère

Le papier explique trois façons différentes dont ce système peut agir comme un détective, selon la situation :

Le Détective « Instantané » (Diagnostic à l'instant 0) :
Ce détective ne regarde que l'image actuelle du film. « Le moteur est chaud en ce moment, donc le ventilateur est cassé en ce moment même ». C'est rapide, mais cela peut passer à côté de la vue d'ensemble.
Le Détective « Historien » (Diagnostic multi-instantané) :
Ce détectif regarde les dernières minutes du film. « Le moteur est chaud depuis 3 minutes, et le ventilateur se comporte bizarrement depuis tout ce temps ». C'est idéal pour les choses qui ne changent pas, comme un fusible cassé qui reste cassé. Il combine les indices du passé pour trouver le coupable.
Le Détective « Voyageur du Temps » (Diagnostic temporel) :
C'est le détective le plus avancé. Il réalise que des pièces peuvent se casser et se réparer d'elles-mêmes (ou se casser à nouveau).
- Scénario : Le ventilateur fonctionnait bien à 1h00, est tombé en panne à 1h05, et a recommencé à fonctionner à 1h10 parce que le moteur a refroidi.
- Le Résultat : Ce détective peut dire : « Le ventilateur était cassé à 1h05, mais il va bien maintenant. » C'est crucial pour les éléments comme un routeur qui perd une connexion pendant une seconde puis se reconnecte.

4. L'Astuce de l'« Hypothèse »

Le système utilise également des « Hypothèses » comme le carnet de notes d'un détective.

Exemple : « Nous supposons que la porte est fermée. » Si le calcul indique que la porte doit être ouverte pour que la température soit aussi élevée, le système réalise que son hypothèse était fausse, ou qu'un capteur ment. Il utilise ces hypothèses pour filtrer les scénarios impossibles et trouver le vrai problème.

5. Est-ce que ça a fonctionné ?

Les auteurs ont construit un prototype de ce système et l'ont testé sur deux circuits numériques standards (comme de minuscules puces informatiques simplifiées).

Ils ont intentionnellement cassé des parties de ces circuits (comme rendre un fil « bloqué » en position éteinte).
Le système a réussi à surveiller le flux de données, à repérer l'erreur, et à identifier correctement exactement quelle partie était cassée, même lorsque les données étaient floues ou que la panne s'était produite dans le passé.
Il l'a fait assez rapidement pour être utile en surveillance en temps réel.

Résumé

Ce papier propose une nouvelle façon de surveiller des machines complexes. Au lieu d'avoir un système d'alarme séparé et un manuel de réparation distinct, il combine les deux en un seul détective continu basé sur un flux. Il peut gérer des données floues, regarder en arrière dans le temps pour trouver la cause profonde, et même suivre des pannes qui apparaissent et disparaissent, tout en faisant fonctionner la machine. C'est comme donner à votre voiture un mécanicien qui ne dort jamais, qui ne manque jamais un indice, et qui peut vous dire exactement ce qui s'est cassé et quand, même si les capteurs sont un peu instables.

Résumé Technique : Un Cadre Unifié pour la Vérification au Moment de l'Exécution et le Diagnostic Basé sur Modèle dans Lola

Énoncé du Problème

Les systèmes critiques pour la sécurité nécessitent non seulement la détection des défaillances, mais aussi la localisation de leurs causes racines pour permettre une atténuation efficace. Alors que la Vérification au Moment de l'Exécution (Runtime Verification - RV) est efficace pour détecter les écarts par rapport au comportement spécifié pendant l'exécution, et que le Diagnostic Basé sur Modèle (Model-Based Diagnosis - MBD) est un cadre fondé sur des principes pour identifier les composants défectueux, ces deux techniques ont historiquement fonctionné de manière isolée. Les moniteurs de RV traditionnels analysent le comportement du système sur des séquences d'états potentiellement illimitées pour détecter des violations, tandis que le MBD opère généralement à un point unique et non spécifié dans le temps après qu'une faute a été détectée. De plus, les intégrations existantes échouent souvent à mapper directement les actions de défaillance détectées vers des composants anormaux au sens du MBD ou manquent de la capacité de gérer les entrées incertaines et la dynamique temporelle des fautes au sein d'un cadre de raisonnement unifié basé sur les flux.

Méthodologie

Le papier propose un cadre unifié qui intègre la RV basée sur les flux et le MBD au sein de Lola, un langage de spécification synchrone basé sur les flux. La méthodologie centrale consiste à encoder à la fois la vérification et l'information de diagnostic sous forme de flux spécialisés, permettant une observation continue et un raisonnement symbolique sous incertitude.

1. Encodage Unifié dans Lola

Les auteurs mappent un système diagnostiqué $S = (sd, comps)$ vers un Système Lola $(\phi, comps)$ :

Description du Système ($sd$) : Encodée dans le flux d'hypothèse ( $\alpha$ ), qui est vrai par définition. Ce flux contient la connaissance comportementale (par exemple, $\neg ab(c) \to beh_c$ ) et la connaissance générale du système.
Composants ($comps$) : Chaque composant $c$ est représenté par un flux booléen interne où true indique que le composant est anormal ($ab(c)$).
Observations : Les variables observables du système (entrées/sorties) sont modélisées comme des flux d'entrée, qui peuvent être certains (déterministes) ou incertains (intervalles ou ensembles non-déterministes).
Variables Non Observables : Les valeurs internes du système non mesurées directement sont modélisées comme des flux internes.
Instance de Problème de Diagnostic (DPI) : Un tuple $(\phi, comps, \Psi)$ , où $\Psi$ représente l'historique des contraintes d'entrée jusqu'au temps actuel.

2. Raisonnement Symbolique et Calcul de Diagnostic

Le cadre utilise un moniteur symbolique qui maintient un ensemble de contraintes $[\phi]_{\Psi}^{\leq t}$ représentant tous les comportements de système possibles cohérents avec les observations jusqu'au temps $t$ .

Résolution de Contraintes : Un solveur SMT (par exemple, Z3) est utilisé pour vérifier la cohérence et dériver des implications.
Dérivation de Diagnostic : Un diagnostic est une hypothèse sur l'état (normal/anormal) des composants qui rend la description du système cohérente avec les observations. Le cadre calcule les diagnostics minimaux en identifiant les conflits minimaux (ensembles de composants qui ne peuvent pas tous être normaux) et en calculant leurs ensembles de frappe minimaux (minimal hitting sets).
Élagage : Pour assurer un monitoring à temps constant et espace constant, les stratégies d'élagage réécrivent les contraintes pour borner la taille de l'ensemble de contraintes, ne conservant que l'information historique nécessaire.

3. Scénarios de Diagnostic

Le cadre prend en charge trois modes de diagnostic distincts basés sur la nature temporelle des fautes des composants :

Diagnostic Multi-Instantané : Suppose que les états des composants sont statiques sur une fenêtre de $k$ instants passés ( $t-k$ à $t$ ). Un diagnostic à $k$ -instants explique toutes les observations au sein de cette fenêtre. Le papier prouve que pour les spécifications atemporelles, les diagnostics à $k$ -instants sont équivalents à l'agrégation de diagnostics à instant unique, mais pour les spécifications temporelles (avec des décalages non nuls), ils fournissent des résultats plus ciblés.
Diagnostic Temporel : Permet aux états des composants de changer au fil du temps. Un diagnostic à $k$ -temporel est un ensemble de paires $(c, t')$ indiquant que le composant $c$ est anormal spécifiquement au temps $t'$ . Ceci est critique pour identifier les défaillances transitoires (ex: surchauffe) ou les fautes qui se manifestent plus tard par propagation.
Paramètres Étendus : Le cadre incorpore naturellement les connaissances de fond (forçant les composants à être normaux), les modèles de fautes forts (spécifiant des comportements défectueux spécifiques) et la modélisation abstraite.

Contributions Clés

Encodage Unifié : Une méthode pour exprimer les descriptions de système et les hypothèses de diagnostic sous forme de flux spécialisés dans Lola, représentant implicitement tous les diagnostics valides pour un comportement observé.
Théorie du Diagnostic Multi-Instantané : Une théorie généralisée pour diagnostiquer les fautes invariantes dans le temps sur une fenêtre d'observations glissante, qui subsume le diagnostic multi-observation standard comme un cas particulier.
Diagnostic Temporel : Support pour l'anormalité variant dans le temps, permettant l'identification de quand une faute se produit, et pas seulement de quel composant est défectueux.
Scénarios de Diagnostic Flexibles : La capacité de gérer élégamment les connaissances de fond, la modélisation abstraite et divers types de fautes (persistantes vs transitoires) au sein d'un seul cadre basé sur les flux.
Implémentation et Évaluation : Une implémentation prototype intégrant l'algorithme HS-Tree, QuickXplain et Z3, validée sur les benchmarks ISCAS85 et ISCAS89.

Résultats

Les auteurs ont évalué le cadre sur deux circuits booléens :

c17 (ISCAS85) : Un circuit purement combinatoire avec 6 composants.
s27 (ISCAS89) : Un circuit séquentiel avec 14 composants.

Constatations :

Faisabilité : Le cadre a réussi à identifier les fautes réellement injectées (stuck-at-false) dans les deux circuits.
Précision Temporelle : Pour le circuit séquentiel (s27), le cadre a correctement localisé les fautes uniquement lorsque la fenêtre d'observation ( $k$ ) était suffisamment grande pour couvrir l'origine de la faute et le temps de propagation.
Performance :
- Le temps d'exécution augmente avec des valeurs de $k$ plus grandes. Pour c17, le diagnostic à $k$ -instants a pris jusqu'à 246 ms ( $k=0$ ) et 775 ms ( $k=31$ ) par instant.
- Le diagnostic temporel était significativement plus coûteux en raison de l'explosion combinatoire du traitement de $(c, t')$ comme des composants distincts. Pour c17, le diagnostic temporel a pris jusqu'à 8,7 secondes par instant pour $k=5$ et 136 secondes pour $k=12$ .
- Malgré le coût computationnel, les auteurs notent qu'avec un $k$ constant, les temps d'exécution restent indépendants de la longueur totale de la trace, confirmant la viabilité des stratégies d'élagage.

Signification et Revendications

Le papier affirme fournir une intégration compacte et bien fondée de la Vérification au Moment de l'Exécution et du Diagnostic Basé sur Modèle. Sa signification réside dans le fait de combler le fossé entre la détection automatique de fautes (RV) et la localisation systématique des causes racines (MBD) au sein d'un cadre unique basé sur les flux.

Les auteurs soulignent que cette approche :

Supporte les entrées incertaines et les hypothèses environnementales, permettant un raisonnement affiné basé sur l'expertise.
Permet un diagnostic en ligne en exploitant le raisonnement symbolique pour produire des verdicts à chaque point temporel.
Offre une combinaison synergique où les forces de la RV (monitoring efficace et continu) et du MBD (analyse de cause racine rigoureuse) sont unifiées.
Fournit un cadre sûr (sound) où le moniteur symbolique garantit que les valeurs déduites sont cohérentes avec tous les mondes possibles définis par les contraintes.

Ce travail est présenté comme une preuve de concept démontrant la faisabilité de l'utilisation de Lola pour des tâches de diagnostic complexes, offrant une base théorique pour de futures applications pratiques dans les systèmes critiques pour la sécurité.