Counterexample-Guided Interval Weakening

1. Énoncé du problème

Les systèmes opérant dans des environnements dynamiques subissent souvent une dégradation des performances (par exemple, pannes matérielles, contraintes de ressources) qui invalide leurs garanties temporelles initiales, même si leur logique fonctionnelle reste correcte. Ces garanties temporelles sont généralement spécifiées à l'aide de la Logique Temporelle Métrique (MTL).

• Le Défi : Lorsqu'un système se dégrade, une spécification MTL idéale (par exemple, « arriver dans les 30 secondes ») peut ne plus être vérifiée. Cependant, une variante logiquement plus faible (par exemple, « arriver dans les 60 secondes ») pourrait encore être satisfaite et utile.
• Le Vide : Les méthodes existantes de réparation de spécifications se concentrent souvent sur des exigences irréalisables (trouver n'importe quelle implémentation) ou utilisent des approches heuristiques et non déterministes (comme les algorithmes génétiques) qui ne garantissent pas l'affaiblissement le plus fort possible. Il manque des méthodes formelles et sémantiques pour dériver automatiquement l'intervalle affaibli optimal (le plus fort) pour un modèle de système dégradé spécifique.

2. Méthodologie : L'algorithme CEGIW

Les auteurs proposent CEGIW (Counterexample-Guided Interval Weakening), un algorithme itératif qui ajuste automatiquement les intervalles de temps dans les spécifications MTL pour les rendre vérifiables sur un modèle de système donné.

Concepts de base

• Contextes : L'algorithme traite la formule MTL comme un « contexte » $C$ avec un « trou » $[-]$ où réside le sous-formule spécifique contenant l'intervalle à affaiblir. Cela permet à l'algorithme de préserver la structure logique de la spécification originale tout en ne modifiant que les bornes des intervalles.
• Ordre d'affaiblissement :
  • Pour l'opérateur Jusqu'à ($U$), l'affaiblissement correspond à étendre la borne droite de l'intervalle (permettre plus de temps).
  • Pour l'opérateur Relâchement ($R$), l'affaiblissement correspond à contracter la borne droite de l'intervalle (exiger moins de temps).
  • Le papier démontre que ces modifications créent un ordre total, permettant à l'algorithme d'identifier un affaiblissement « optimal » unique.

Flux de travail de l'algorithme

L'algorithme fonctionne à deux niveaux imbriqués :

1. Boucle itérative (Niveau supérieur) :

   • Un vérificateur de modèle (spécifiquement nuXmv) vérifie si la propriété MTL actuelle est vérifiée sur le modèle du système.
   • Si la propriété échoue, le vérificateur de modèle produit une trace de contre-exemple (spécifiquement une « trace en lasso », composée d'un préfixe fini et d'un suffixe répétitif).
   • L'algorithme appelle la fonction Weaken (Affaiblir) pour ajuster l'intervalle en fonction de ce contre-exemple spécifique.
   • Le processus se répète avec la nouvelle propriété affaiblie jusqu'à ce que la propriété soit vérifiée sur le modèle ou qu'aucun affaiblissement valide n'existe.

2. Affaiblissement sur les contre-exemples (Niveau inférieur) :

   • Couverture par lasso : Au lieu d'itérer sur des traces infinies, l'algorithme utilise un « intervalle de couverture » pour déterminer la satisfaction sur la trace en lasso infinie en utilisant uniquement un calcul fini.
   • Parcours récursif : La fonction Weaken parcourt récursivement le contexte MTL.
     • Cas de base : Calcule directement l'extension minimale d'intervalle (pour $U$) ou la contraction (pour $R$) requise pour satisfaire la trace spécifique.
     • Cas inductifs : Propage les exigences d'affaiblissement vers le haut de l'arbre syntaxique. Par exemple, si une sous-formule est l'opérande gauche d'un opérateur $U$, l'algorithme doit trouver un intervalle qui satisfait la condition pour tous les pas de temps jusqu'à ce que l'opérande droit devienne vrai, en sélectionnant l'intervalle le plus faible couvrant toutes les exigences.

3. Contributions clés

• Algorithme CEGIW : Un algorithme itératif novateur, guidé par contre-exemple, qui dérive automatiquement l'affaiblissement d'intervalle le plus fort possible pour les spécifications MTL étant donné un modèle de système dégradé.
• Garanties formelles : Les auteurs fournissent des preuves rigoureuses pour :
  • Correction : Si l'algorithme renvoie un intervalle, la propriété affaiblie est vérifiée sur le système.
  • Optimalité : L'intervalle renvoyé est l'affaiblissement « le plus fort » possible (c'est-à-dire qu'aucun intervalle strictement plus fort ne satisferait le système).
• Préservation du contexte : La méthode modifie uniquement les bornes numériques des intervalles, préservant la structure logique et la sémantique de la spécification originale, ce qui est crucial pour maintenir l'intention des exigences critiques pour la sécurité.
• Validation empirique : L'approche a été testée sur des études de cas réels utilisant le framework FRET (Formal Requirements Elicitation Tool).

4. Résultats et évaluation

Les auteurs ont évalué CEGIW en utilisant deux questions de recherche :

• RQ1 : Capacité de diagnostic (Étude de cas du robot de fourrage) :

  • Appliqué à un modèle de vol d'essaims de robots, CEGIW a d'abord identifié un défaut de conception (une boucle infinie) où aucun affaiblissement n'existait.
  • Après la correction du modèle, CEGIW a dérivé avec succès les bornes temporelles optimales : étendant le temps de « retour à la maison » de 3 à 20 unités et contractant le temps de « rester à l'écart » de 20 à 3 unités.
  • Cela démontre la capacité de CEGIW à la fois à diagnostiquer les erreurs de modélisation et à quantifier la résilience du système.

• RQ2 : Applicabilité aux exigences du monde réel :

  • Analyse de 419 exigences provenant de 8 études de cas réelles (par exemple, ventilateurs pulmonaires mécaniques, drones autonomes, contrôleurs d'aéronefs).
  • Résultats : 124 exigences sur 419 (environ 30 %) étaient susceptibles d'un affaiblissement d'intervalle.
  • Interprétation : 116 nécessitaient une extension d'intervalle (par exemple, permettre plus de temps à une boucle de contrôle en raison de la latence réseau), et 11 nécessitaient une contraction (par exemple, un ventilateur doit rester allumé au moins pendant un certain temps, donc la borne inférieure est resserrée).
  • L'étude confirme que l'affaiblissement d'intervalle est un outil pratique pour les domaines critiques pour la sécurité où la dégradation est attendue.

5. Importance et travaux futurs

• Importance : CEGIW comble le fossé entre la vérification formelle et la dégradation des systèmes. Il va au-delà de la simple vérification « réussite/échec » pour fournir des retours quantitatifs et exploitables sur la mesure dans laquelle les performances d'un système peuvent se dégrader avant que ses garanties ne tombent en panne. Cela est vital pour concevoir des systèmes critiques pour la sécurité résilients.
• Limites et travaux futurs :
  • Actuellement, l'algorithme ne modifie que la borne droite des intervalles. Les travaux futurs visent à gérer les bornes gauche et droite, ce qui introduit un ordre partiel et complique la définition de « l'optimalité ».
  • Actuellement, un seul intervalle est affaibli à la fois. Les travaux futurs prévoient d'intégrer une optimisation multi-objectifs (optimalité de Pareto) pour affaiblir plusieurs intervalles simultanément.
  • Le champ d'application est actuellement limité aux modifications d'intervalle ; les recherches futures pourraient explorer les changements syntaxiques de la structure de la formule elle-même.

En résumé, le papier présente un cadre robuste et mathématiquement fondé pour réparer automatiquement les spécifications temporelles dans les systèmes dégradés, offrant aux ingénieurs un moyen précis de comprendre et de quantifier la résilience du système.