Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

Résumé Technique : Contraintes Différées dans l'Élargissement pour les Analyses Logiques des Systèmes Temps Réel

Énoncé du Problème
L'analyse formelle des systèmes temps réel fait face à deux défis primordiaux concernant l'infinitude : le potentiel d'un nombre non borné d'agents et de messages, et un espace d'états qui est infini en raison du temps dense. Les méthodes de vérification traditionnelles en Logique de Réécriture (RL), particulièrement celles implémentées dans le moteur de réécriture Maude, ont été historiquement limitées. Bien que Maude supporte la vérification d'invariants pour des systèmes avec des composants entièrement spécifiés (termes de base) et des contraintes SMT, il peine avec les systèmes contenant un nombre inconnu d'agents ou des paramètres arbitraires. De plus, les techniques symboliques précédentes reposaient souvent sur l'échantillonnage temporel, ce qui manque de correction et de complétude dans les contextes de temps dense. Les approches existantes utilisant des variables logiques pour des agents non bornés entraînent souvent des procédures de semi-décision avec des espaces de recherche infinis, manquant de mécanismes pour garantir la terminaison.

Méthodologie
Les auteurs proposent un nouveau cadre de vérification qui intègre trois techniques fondamentales pour répondre à ces limitations :

1. Réécriture modulo SMT : Utilisation des théories SMT pour la représentation symbolique des contraintes temporelles.
2. Élargissement (Narrowing) avec Variables Logiques : Emploi de variables logiques pour raisonner sur des systèmes avec un nombre inconnu ou arbitraire d'agents.
3. Contraintes Différées et Repli (Folding) : Introduction d'un magasin de contraintes sur des termes partiellement instanciés, inspiré de la Programmation Logique par Contraintes (CLP).

L'innovation centrale est l'Élargissement avec Repli Différé (Delayed Folding Narrowing). Contraなり à l'élargissement standard, cette méthode permet aux expressions SMT dans les conditions de règles de contenir des parties « différées » — des sous-expressions qui ne peuvent être évaluées que lorsque les termes sont davantage instanciés. Ceci est réalisé grâce à une Extension SMT où les expressions SMT non valides (par exemple, mte(t, T') représentant un temps d'écoulement maximal) sont abstraites en de nouvelles variables. Ces contraintes sont accumulées et ne sont résolues ou propagées qu'une fois que les termes sont suffisamment instanciés.

Le cadre définit des Théories de Réécriture Temps Réel Logiques, qui étendent les théories de réécriture temps réel standards pour permettre :

• Des conditions dans les règles de réécriture incluant des expressions SMT avec des parties différées.
• Des membres de droite (RHS) incluant des variables non présentes dans le membre de gauche (LHS).
• Des requêtes contenant des variables partagées dans les états initiaux et cibles.

Pour assurer la terminaison, la méthode emploie un mécanisme de repli (folding). Un graphe d'états est construit où un état symbolique $v'$ est supprimé s'il est une instance d'un état précédemment exploré modulo la théorie équationnelle. Les auteurs prouvent que, sous des conditions spécifiques (notamment une hiérarchie de sorts soigneusement conçue), ce préordre de repli garantit un espace de recherche fini, transformant la procédure de semi-décision en une procédure de décision pour la vérification d'invariants.

Contributions Clés

1. Élargissement avec Repli Différé : La définition et l'implémentation d'une relation d'élargissement qui gère les expressions SMT étendues avec des contraintes différées. Cela permet la vérification de systèmes avec des variables logiques et SMT arbitraires tant dans la configuration initiale que dans l'invariant.
2. Vérification du Protocole de Fischer Temporel : Le papier présente la première vérification automatique de la correction du protocole d'exclusion mutuelle de Fischer temporel dans son cadre le plus général. Cela inclut un nombre arbitraire de processus et des paramètres temporels arbitraires ($\gamma$ et $\delta$). Ceci a été accompli en concevant une hiérarchie de sorts spécifique pour garantir la terminaison de la procédure de repli et en utilisant des variables logiques pour représenter le nombre non spécifié de processus.
3. Synthèse de Contrôleur pour les Philosophes de la Faim : Le cadre est appliqué à un problème de philosophes de la faim temporel pour synthétiser un contrôleur (le « lackey »). En laissant les transitions du contrôleur non spécifiées (représentées par des variables logiques), la procédure d'élargissement synthétise les transitions manquantes nécessaires pour satisfaire une propriété de raggiungibilité (par exemple, l'entrée de philosophes spécifiques dans la salle à manger avant une échéance).

Résultats
La méthode a été implémentée comme une extension du moteur de réécriture Maude en utilisant des fonctionnalités de méta-niveau.

• Protocole de Fischer : Les auteurs ont vérifié avec succès l'exclusion mutuelle pour un nombre arbitraire de processus. Lorsque l'état initial était contraint tel que $\gamma > \delta$, l'espace de recherche était fini (contenant seulement 3 états grâce au repli), et l'outil a confirmé qu'aucun état atteignable ne violait l'invariant. Inversement, lorsque $\delta \ge \gamma$, un contre-exemple a été trouvé.
• Philosophes de la Faim : Le système a synthétisé avec succès un automate « lackey » permettant à des philosophes spécifiques d'entrer dans la salle à manger. La sortie a fourni un ensemble concret de transitions et de localisations pour le contrôleur, démontrant la capacité du cadre à gérer des tâches de synthèse.
• Efficacité : Le mécanisme de repli a considérablement réduit l'espace de recherche, permettant l'analyse de systèmes qui seraient autrement intraçables en raison d'espaces d'états infinis.

Signification et Revendications
Le papier affirme fournir une base sonore et expressive pour la vérification symbolique des théories de réécriture temps réel. Sa signification réside dans le pont jeté entre l'expressivité de la programmation logique (gestion des agents non bornés via des variables logiques) et la précision de l'analyse temps réel (gestion du temps dense via SMT et contraintes différées).

Les auteurs soulignent que leur approche va au-delà de Maude « standard » et des outils existants pour les Automates Temporels Paramétriques (PTA), qui nécessitent typiquement un nombre fixe de processus ou des limites temporelles fixes. En supportant des paramètres arbitraires et un nombre non borné d'agents au sein d'un même cadre, la méthode offre une approche uniforme pour analyser des modèles temps réel complexes, incluant la synthèse de composants système manquants. Le travail suggère que les contraintes différées sont un mécanisme crucial pour atteindre la terminaison dans les analyses symboliques de systèmes temps réel à états infinis.