💻 computer science

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

Cet article présente TREBL, une extension relative complète de la logique Event-B permettant d'exprimer et de vérifier les conditions de vivacité via des règles de déduction soundes, en s'appuyant sur des raffinements de machines où des termes de variante sont définissables, tout en illustrant la théorie par des exemples de sécurité.

Auteurs originaux : Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

Publié 2026-04-22

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

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 d'orchestre d'un grand système informatique, comme une usine automatisée ou un système de sécurité bancaire. Votre travail consiste à vous assurer que tout fonctionne non seulement correctement à chaque instant, mais aussi dans le temps.

C'est là que ce papier scientifique, intitulé TREBL, intervient. Il propose une nouvelle façon de vérifier que ces systèmes ne vont pas se bloquer ou faire des choses interdites, en utilisant une logique mathématique très puissante mais expliquée ici simplement.

Voici l'explication de ce travail, imagée et simplifiée :

1. Le Problème : Le "Film" vs La "Photo"

Dans les méthodes de vérification classiques (comme Event-B), on regarde le système comme une série de photos.

La photo (l'état actuel) : "Le stock est à 50 unités."
Le problème : On sait que si le stock est à 50, il peut passer à 49 ou 51. Mais la logique classique a du mal à dire : "Peu importe les photos intermédiaires, finalement, le stock va toujours retomber à 0" ou "Le système ne va jamais se figer".

Les logiques temporelles classiques (comme LTL) sont faites pour regarder le film (la séquence complète des événements). Mais elles sont trop "bêtes" : elles ne comprennent pas la complexité mathématique de votre système (les ensembles, les variables). C'est comme essayer de décrire un film complexe avec des mots très simples : ça manque de précision.

D'un autre côté, si on essaie de tout mélanger, on obtient un système si compliqué qu'on ne peut plus jamais prouver qu'il est correct (c'est le problème de l'incomplétude).

2. La Solution de TREBL : Le "Télécommande Magique"

Les auteurs (Klaus-Dieter Schewe et son équipe) ont eu une idée géniale. Au lieu de regarder le film entier, ils disent : "L'état actuel détermine tout le futur."

Imaginez que votre système est un labyrinthe.

L'approche classique : Il faut simuler tous les chemins possibles pour voir si on sort du labyrinthe.
L'approche TREBL : Ils disent : "Si vous êtes à ce carrefour précis (l'état actuel), vous avez une télécommande magique (appelée update set ou ensemble de mise à jour). Cette télécommande contient déjà les instructions de tous les futurs mouvements possibles."

Grâce à cette idée, ils peuvent définir des opérateurs temporels (comme "Toujours", "Finalement", "Jusqu'à") non pas comme des règles pour regarder le film, mais comme des raccourcis mathématiques basés sur l'état actuel.

Au lieu de dire : "Regardez le film, est-ce qu'il pleut un jour ?", ils disent : "Regardez la télécommande actuelle : est-ce qu'elle contient une instruction pour faire pleuvoir ?"

Cela permet de garder la puissance des mathématiques complexes tout en restant dans un cadre où l'on peut prouver que tout est correct.

3. Les "Variants" : Les Sabliers de la Preuve

Pour prouver que le système va finalement atteindre un but (par exemple, vider le tampon de données), les auteurs utilisent des variants.

Imaginez un sablier posé sur une table.

Chaque fois qu'un événement se produit (une pièce tombe), le niveau de sable baisse.
La règle est simple : le sable ne peut pas descendre indéfiniment. Il finit par atteindre le fond.
Si vous pouvez prouver que chaque action du système fait baisser le niveau du sable, alors vous savez mathématiquement que le système va finalement s'arrêter ou atteindre son but.

Dans TREBL, ils montrent comment construire ces sabliers (appelés variant terms) pour n'importe quel système, même très complexe. Et le plus beau, c'est qu'ils prouvent qu'on peut toujours ajouter un sablier à notre système (en le "raffinant" ou en l'améliorant) si on en a besoin pour la preuve.

4. Pourquoi c'est important pour la Sécurité ?

Le papier utilise des exemples de sécurité, comme un système de non-interférence.

Scénario : Imaginez un bâtiment avec des niveaux de sécurité (Public, Confidentiel, Secret).
Le risque : Un espion au niveau "Public" ne doit jamais pouvoir deviner ce qui se passe au niveau "Secret", même en observant les mouvements du système.
L'apport de TREBL : Avec cette nouvelle logique, on peut écrire une règle simple : "Peu importe ce qui se passe dans les étages secrets, l'aspect visible depuis l'extérieur ne change jamais." TREBL permet de prouver cela de manière automatique et rigoureuse, là où les anciennes méthodes échouaient ou étaient trop lourdes.

En Résumé

Ce papier est une avancée majeure car il résout un vieux débat : "On veut de la puissance (pour décrire des systèmes complexes) OU on veut de la certitude (pouvoir prouver que ça marche) ?"

TREBL dit : "Non, on peut avoir les deux !"

Il transforme la logique temporelle (le temps) en logique d'état (l'instant présent) grâce à une astuce mathématique.
Il fournit des règles claires (comme des recettes de cuisine) pour prouver que les systèmes ne vont jamais se bloquer.
Il garantit que si une propriété est vraie, on peut toujours trouver la preuve mathématique, à condition d'avoir bien défini nos "sabliers" (les variants).

C'est comme passer d'une vérification à l'aveugle (regarder le film) à une vérification par la structure même du système (regarder la télécommande), rendant la sécurité des logiciels beaucoup plus fiable et vérifiable.

1. Problématique

La vérification des conditions de vivacité (liveness) est un défi majeur dans les méthodes rigoureuses basées sur les états, telles que Event-B, B, TLA+ ou les Machines à États Abstraits (ASM).

Limites des logiques existantes : Les logiques temporelles classiques (LTL, CTL) sont souvent limitées par leur nature propositionnelle, ce qui restreint leur expressivité lorsqu'elles sont appliquées à des systèmes complexes. À l'inverse, les extensions temporelles de la logique du premier ordre (comme LTL(EB)) offrent une grande expressivité mais souffrent d'incomplétude, rendant impossible la garantie qu'une propriété valide puisse être prouvée mécaniquement.
Le compromis Expressivité vs Complétude : Il existe un dilemme fondamental : soit on utilise des logiques propositionnelles (complètes mais peu expressives), soit des logiques du premier ordre enrichies (expressives mais incomplètes).
Spécificité d'Event-B : Dans Event-B, un état détermine l'ensemble des traces possibles qui en découlent. Cependant, les approches précédentes (comme LTL(EB)) interprétaient les formules temporelles sur des traces arbitraires, ce qui complexifiait la preuve de complétude et nécessitait des hypothèses restrictives (comme l'homogénéité des queues de traces, ou tail-homogeneity).

L'objectif est de définir une logique temporelle pour Event-B qui soit à la fois expressive (capable de décrire des propriétés sur les traces) et relativement complète (toute propriété valide est dérivable), tout en conservant l'interprétation des formules sur les états plutôt que sur les traces.

2. Méthodologie

Les auteurs proposent une extension de la logique d'Event-B, appelée TREBL (Temporal Event-B Logic), reposant sur les piliers suivants :

Extension de la logique (Lext) : Au lieu d'interpréter les formules sur des traces, les auteurs étendent la logique d'Event-B pour inclure des ensembles de mises à jour (update sets) et leurs effets.
- Ils introduisent des opérateurs modaux $[X]\phi$ signifiant "après l'application de l'ensemble de mises à jour $X$ , la propriété $\phi$ est vraie".
- Ils définissent des ensembles de mises à jour pour des séquences de $k$ étapes ( $USet^*(k, X)$ ), permettant de raisonner sur l'évolution de l'état sur plusieurs pas de temps.
Opérateurs temporels comme raccourcis : Les opérateurs temporels classiques ( $\square$ $□$ toujours, $\diamond$ $⋄$ éventuellement, $U$ $U$ jusqu'à) sont définis comme des raccourcis syntaxiques de formules complexes de $Lext$ interprétées sur les états initiaux.
- Exemple : $\square \phi$ signifie que pour tout $n$ et tout ensemble de mises à jour $X$ correspondant à $n$ étapes, l'état résultant satisfait $\phi$ .
Gestion des traces définissables : La logique permet de quantifier sur des ensembles de traces définis par des conditions temporelles (sémantique de type "team"), éliminant ainsi la nécessité de l'hypothèse d'homogénéité des queues de traces.
Règles de dérivation et Variants : Pour prouver la vivacité, l'article introduit une série de règles de dérivation basées sur des termes de variant (c-variants, d-variants, e-variants, etc.). Ces termes prennent des valeurs dans un ensemble bien fondé et décroissent strictement pour garantir la convergence ou la persistance.
Raffinement conservatif : Un point clé de la méthodologie est la démonstration que pour toute machine satisfaisant une propriété de vivacité, il existe un raffinement conservatif de cette machine dans lequel les termes de variant nécessaires peuvent être explicitement définis.

3. Contributions Clés

Définition de TREBL : Une logique temporelle fragmentaire d'Event-B capable d'exprimer l'invariance, l'existence, le progrès, la persistance et l'accessibilité, tant pour toutes les traces que pour une seule trace ou des sous-ensembles définissables.
Interprétation sur les états : Contrairement aux logiques temporelles traditionnelles, TREBL interprète les formules sur les états initiaux des machines, exploitant le fait qu'un état détermine ses traces futures. Cela simplifie la sémantique et la preuve.
Système de règles de dérivation complet :
- Introduction de règles pour l'invariance, l'existence, la persistance et le progrès.
- Développement de variants complexes : variants simultanés (pour la convergence et la divergence combinées), variants conditionnels (avec variables booléennes pour suivre l'état de la trace), et variants de préfixe.
- Ces règles couvrent les combinaisons d'opérateurs quantificateurs de traces ( $\square, \square_1$ ) et d'opérateurs temporels ( $\diamond, \diamond_1$ ).
Preuve de Complétude Relative :
- Les auteurs prouvent que le système de règles est relativement complet. Cela signifie que si une formule est valide ( $M \models \phi$ ), alors elle est dérivable ( $M \vdash \phi$ ), à condition que la machine soit "suffisamment raffinée" pour permettre la définition des termes de variant requis.
- Ils démontrent que de tels raffinements existent toujours, rendant la complétude relative atteignable en pratique.
Élimination des restrictions : Contrairement aux travaux antérieurs (comme [FRS+24]), cette approche supprime la restriction d'homogénéité des queues de traces (tail-homogeneity), élargissant ainsi le champ d'application de la logique.

4. Résultats

Théorème de Complétude Relative (Théorème 3.2) : Le système de règles $R$ est relativement complet pour TREBL. Pour toute formule TREBL $\phi$ valide sur une machine $M$ satisfaisant les hypothèses de relativité (cohérence, inclusion des invariants, raffinement suffisant), il existe une dérivation formelle de $\phi$ .
Preuve de Soundness (Sûreté) : Toutes les règles de dérivation présentées sont prouvées sûres (sound), garantissant que si une propriété est dérivable, elle est bien vraie sur la machine.
Applications à la Sécurité : L'article illustre la puissance de TREBL sur des exemples de sécurité complexes :
- Non-interférence : Démontrée comme une condition d'invariance simple avec des formules de transition, là où les logiques LTL/CTL traditionnelles auraient du mal à exprimer les conditions de transition.
- Deducibilité bornée (Bounded Deducibility) : Capturée via des invariants de transition, évitant la complexité des contraintes de traces multiples.
Exemples de Vivacité : La logique est appliquée avec succès à des systèmes producteur-consommateur pour prouver des propriétés de progrès (service garanti) et de persistance (stabilité finale).

5. Signification et Impact

Avancée Théorique : Ce travail résout le problème de la complétude pour les logiques temporelles dans les méthodes formelles basées sur les états. Il offre un cadre où l'on peut raisonner sur les traces sans perdre la propriété de complétude relative, en exploitant la structure des machines Event-B.
Praticité pour la Vérification : En rendant les preuves de vivacité mécanisables via des règles de dérivation standard et des variants, TREBL facilite l'usage d'outils comme RODIN. La nécessité de définir des variants explicites est présentée non pas comme une contrainte, mais comme une opportunité de raffiner le modèle pour mieux capturer la dynamique du système.
Généralité : Bien que centré sur Event-B, l'approche est conçue pour être adaptable à d'autres méthodes rigoureuses basées sur les états (ASM, B, TLA+), car elle repose sur des concepts fondamentaux (ensembles de mises à jour, raffinement, variants).
Perspectives : La Partie II de la série (annoncée) traitera de l'implémentation de ces règles dans l'outil RODIN via la méta-théorie EB4EB, fournissant ainsi un support de preuve mécanique complet.

En résumé, TREBL représente une percée majeure en unifiant expressivité et complétude relative pour la vérification de vivacité dans les systèmes critiques, en transformant les propriétés temporelles complexes en problèmes de logique du premier ordre sur les états, résolubles par raffinement et induction.