Soutenance mémoire
Relations
Une relation R sur E × F est un ensemble R ⊆ E × F. On note x R x 0 quand (x, x0) ∈ R. La relation inverse de R, notée R−1 ⊆ F × E, est définie par (x0 , x) ∈ R−1 si et seulement si (x, x0) ∈ R. L’image de x ∈ E par R est un ensemble R(x) ⊆ F défini par R(x) = {x 0 ∈ F | xRx 0}. Nous étendons la définition à X ⊆ E par R(X) = {x 0 ∈ F | ∃x ∈ X, xRx0}. Étant données deux relations R1 ⊆ E×F et R2 ⊆ F ×G, la composition de R1 et R2, notée R1 • R2, est la relation sur E × G définie par x (R1 • R2) x 00 si et seulement si il existe x 0 ∈ F tel que x R1 x0 et x 0 R2 x00. Une relation binaire sur E est une relation sur E × E. On dira plus simplement une relation sur E. La relation identité IdE sur E se définit par IdE = {(x, x) | x ∈ E}. Une relation R sur E est réflexive si IdE ⊆ R ; transitive si xRx0 et x 0Rx 00 implique xRx 00 pour tout x, x 0, x 00 ; antisymétrique si xRx 0et x0Rx implique x = x0 pour tout x, x0. La relation Ri est une relation binaire définie inductivement par R0 = IdE et Ri+1 = R • Ri . La clôture réflexive et transitive de R, notée R∗ , est définie par R∗ =S i≥0 Ri.
Ensembles clos de Nm
Nous définissons les deux restrictions suivantes de la logique de Presburger : La logique Clos par le Bas (CB) [BM99] est le fragment de la logique de Presburger dans lequel les termes sont de la forme t ::= x ≤ c, avec x une variable libre et c ∈ Nm∞, et φ ::= t|φ ∧ φ|φ ∨ φ|vrai|faux. La logique Clos par le Haut (CH) [BM99] est le fragment de la logique de Presburger dans lequel les termes sont de la forme t ::= x ≥ c, avec x une variable libre et c ∈ Nm∞, et φ ::= t|φ ∧ φ|φ ∨ φ|vrai|faux. Les ensembles CB-définissables sont exactement les ensembles clos par le bas de N m et les ensembles CH-définissables sont exactement les ensembles clos par le haut de N m [BM99].
Cadre de l’accélération plate
Nous proposons le premier cadre théorique pour le model checking avec accélération. Ce cadre s’articule autour de quatre concepts clés. Les deux premiers sont classiques et reprennent des définitions usuelles, les deux autres sont originaux. Le système (définition 2.2.3) est l’abstraction mathématique modélisant les programmes à analyser. Nos systèmes sont composés d’une structure de contrôle et d’un nombre fini de variables, dont les valeurs sont modifiées par le franchissement des transitions. Le cadre symbolique (définition 2.3.1) permet de manipuler des ensembles infinis de configurations via une représentation symbolique et des opérations de base. L’algorithme d’accélération (définition 2.4.1) calcule tous les successeurs d’une configuration donnée par les séquences de transitions appartenant à un langage L sur l’alphabet T des transitions du système. L’heuristique de recherche permet de relier l’algorithme d’accélération au calcul effectif de l’ensemble des configurations accessibles. Nous distinguons trois niveaux d’accélération selon le type de langage L considéré : l’accélération de boucle si L est de la forme t
∗ avec t ∈ T, l’accélération plate si L est de la forme w
∗ avec w ∈ T
∗et l’accélération globale si L
est une expression régulière quelconque sur T. Ces niveaux rendent compte de la plupart des résultats d’accélération sur des systèmes particuliers. On peut citer par exemple le cas des systèmes à files [BH99, ACBJ04] et des systèmes à compteurs [BW94, WB98, FL02]. La section 2.4.2 fait un bilan des nombreuses techniques d’accélération conformes à notre cadre. D’un côté l’accélération de boucle apparaît insuffisante en pratique pour assurer la convergence et beaucoup de résultats d’accélération de boucle peuvent s’étendre à l’accélération plate. D’un autre côté, l’accélération globale assure systématiquement la convergence, et ne peut donc être obtenue pour des classes Turing-complètes. Or c’est précisément la vérification de telles classes qui nous intéresse. L’accélération plate apparaît donc comme le bon compromis.
Heuristique pour l’accélération plate
Nous développons ici de nouveaux concepts pour l’étude algorithmique de l’accélération plate. Systèmes applatissables. Les notions d’applatissement (définition 2.5.2) et de système applatissable (définition 2.5.3) font le lien entre d’un côté les résultats d’accélération plate et de l’autre le calcul effectif de l’ensemble d’accessibilité. Nous montrons que l’ensemble d’accessibilité est calculable par accélération plate si et seulement si le système est applatissable (théorème 2.5.4). C’est la première caractérisation, complète, des systèmes calculables par accélération plate. La majeure partie des systèmes analysés par des outils comme Alv, Fast, Lash ou TReX sont applatissables mais pas plats, ce qui souligne la pertinence de ce concept. De plus de nombreux résultats de calcul effectif d’ensembles d’accessibilité s’avèrent être des résultats d’applatissement et de nombreuses sous-classes standards sont applatissables, par exemple les VASS à deux compteurs [LS04], les automates temporisés [CJ99], les machines à compteurs reversal bornées, les VASS lossy et d’autres sous classes de VASS [LS05]. Procédures. La procédure access2 (procédure 2, section 2.6) est complète dans le sens où elle termine si et seulement si elle est appliquée à un système applatissable (et pas seulement plat). C’est le premier résultat de complétude pour le model checking symbolique avec accélération. La procédure access2 est générique et peut être instanciée de différentes manières. Nous proposons une instanciation access3 (procédure 3, section 2.6.2) visant à trouver efficacement un applatissement d’un système non plat, sans perdre la complétude. Il apparaît qu’un point clé de access3 est la réduction du nombre de circuits que la procédure doît considérer. Nous généralisons la notion de réduction introduite dans [FL02] et nous définissons deux nouvelles réductions indépendantes du domaine de données considéré.
Approches existantes
La bibliothèque CSL [YKTB01] fournit des structures de données génériques pouvant être composées. Cependant comme l’accélération n’est pas prise en compte, la composition des différents types de données est un simple produit cartésien. La bibliothèque contient des booléens codés sous forme de bdd et des entiers codés par des automates binaires ou des formules. L’outil TReX [ABS01] peut manipuler des systèmes avec files lossy, compteurs et horloges. L’accélération sur les horloges et compteurs est une accélération dédiée. Sur les systèmes à files lossy, horloges et compteurs TReX utilise un produit cartésien d’accélérations. Dans [BH99] Bouajjani et Habermehl s’intéressent à l’accélération plate sur des systèmes à files FIFO munis du cadre des cqdd. Les notions de variables d’itération et de synchronisation d’accélérations sont présentes, mais mêlées aux algorithmes sur les cqdd. Ici nous clarifions les idées, en séparant ce qui est général de ce qui dépend des cadres symboliques particuliers utilisés, et nous généralisons à des types de données arbitraires.
Accélération plate de systèmes à compteurs
De nombreux travaux considèrent l’accélération des systèmes à compteurs. On peut citer par exemple [Rev90, BW94, FO97a, FO97b, Boi98,BF99, PS00, AAB00, FL02, Boi03]. Ces approchent fournissent des procédures génériques pour le calcul de l’ensemble d’accessibilité de larges sousclasses de systèmes à compteurs. Nous présentons ici les points clés pour analyser les systèmes à compteurs par accélération plate, à savoir le cadre symbolique et l’algorithme d’accélération. Les systèmes à compteurs affines. Les systèmes à compteurs n’admettent pas d’accélération plate, car le problème de l’accessibilité dans ces systèmes n’est pas décidable (lemme 4.2.1). Nous nous intéressons à la sousclasse des systèmes à compteurs affines où les transitions sont étiquetées par des fonctions affines gardées par une formule de Presburger. Le cadre symbolique. Les ensembles Presburger-définissables peuvent être représentés symboliquement par des automates [BC96, WB00, Ler03a]. Cette représentation définit un cadre symbolique pour les systèmes à compteurs comme décrit au chapitre précédent. L’accélération plate. Boigelot et Wolper dans [BW94, Boi98, Boi03] et Finkel et Leroux dans [FL02] ont montré que sous certaines hypothèses algébriques (finitude du monoïde engendré par les matrices des fonctions affines), l’accélération plate est admise. De plus de tels systèmes sont courants : les VASS et la plupart de leurs extensions [DFS98, FS00], les protocoles broadcast d’Emerson et Namjoshi [EN98, EFM99], et les systèmes à compteurs reversal bornés d’Ibarra [ISD+02] sont des systèmes affines à monoïde fini. Il existe de nombreux résultats d’accélération plate pour des variantes de systèmes à compteurs affines. [Rev90, FO97a, FO97b, BF99] accélèrent automatiquement des cycles non élémentaires. [PS00] considère le problème de l’accélération en utilisant des formules dans une variante de WS1S pour la représentation symbolique des configurations. Parmi les nombreux travaux sur le sujet nous pouvons également citer [BF00] et [BGP99], qui utilisent tous deux l’outil Mona [Mon]. La procédure implantée dans l’outil TReX [AAB00] calcule des itérations de séquences de transitions sur des systèmes à compteurs dont les actions sont des affectations simples xi:= xj + c gardées par des des contraintes diagonales xi − xj{≤, ≥}c, où xi , xj sont des variables et c ∈ N m. Cette procédure n’est pas une accélération au sens strict du chapitre 2. D’un côté, la procédure n’est pas récursive, de l’autre elle permet dans certains cas de calculer des itérations de boucles imbriquées.
Complexité de l’accélération
La question de la complexité de l’accélération n’a guère été étudiée. Dans [BFL04], nous montrons que l’accélération plate définie dans [FL02] peut être bornée en temps et en espace par 3-EXP dans la taille du domaine. Les autres facteurs sont le nombre de variables et la plus grande constante intervenant dans la définition de f. Nous nous intéressons à définir des algorithmes d’accélération plate plus efficaces pour des systèmes à compteurs utilisant des translations convexes et des translations positives.
|
Table des matières
Introduction
1 Avant-propos
1.1 Ensembles, relations, fonctions, ordres
1.1.1 Ensembles
1.1.2 Relations
1.1.3 Fonctions
1.1.4 Ordres et ensembles clos
1.2 Ensembles de nombres
1.2.1 Nombres, vecteurs et matrices
1.2.2 Ensembles Presburger-définissables
1.2.3 Polyèdres convexes
1.2.4 Ensembles clos de Nm
1.3 Langages
1.3.1 Mots
1.3.2 Langages
1.3.3 Sous-classes de langages réguliers
I Théorie de l’accélération
2 Cadre de l’accélération
2.1 Introduction
2.1.1 Cadre de l’accélération plate
2.1.2 Heuristique pour l’accélération plate
2.1.3 Applications
2.2 Systèmes et interprétations
2.2.1 Définitions
2.2.2 Sémantique
2.2.3 Propriétés de sûreté
2.2.4 Familles de systèmes
2.3 Cadre symbolique
2.3.1 Définitions
2.3.2 Limites de l’approche symbolique
2.3.3 Procédure symbolique standard
2.4 Accélération
2.4.1 Niveaux d’accélération
2.4.2 Exemples
2.4.3 L’accélération plate comme meilleur compromis
2.5 Accélération plate
2.5.1 Expressions régulières linéaires restreintes
2.5.2 Systèmes plats
2.5.3 Applatissement de systèmes non plats
2.5.4 Complétude de l’applatissement
2.5.5 Le point sur les systèmes applatissables
2.6 Procédure pour les systèmes applatissables
2.6.1 Première procédure
2.6.2 Raffinement
2.6.3 Réduction du nombre de séquences utiles
2.7 Conclusion
3 Composition d’accélérations
3.1 Introduction
3.1.1 Contexte
3.1.2 Composition d’accélérations
3.1.3 Approches existantes
3.2 Systèmes faiblement hétérogènes
3.3 Composition de cadres symboliques
3.3.1 Produit cartésien de cadres symboliques
3.3.2 Produit cartésien d’accélérations plates
3.4 Composition synchronisée d’accélérations
3.4.1 P-Cadre symbolique
3.4.2 P-Accélérations
3.4.3 Produits synchronisés
3.4.4 Extensions
3.4.5 P-cadres symboliques existants
3.5 Conclusion
II Vérification de systèmes à compteurs
4 Accélération de systèmes à compteurs
4.1 Introduction
4.1.1 Contexte
4.1.2 Accélération plate de systèmes à compteurs
4.1.3 Implantation efficace de l’accélération plate
4.2 Systèmes à compteurs affines
4.2.1 Systèmes à compteurs
4.2.2 Systèmes à compteurs affines
4.2.3 Monoïde d’un système à compteurs affine
4.2.4 Sur les systèmes à compteurs affines
4.3 Cadre symbolique : automates binaires
4.3.1 Automates binaires
4.3.2 Cadre symbolique
4.3.3 Complexité de la construction
4.3.4 Ensembles reconnaissables par automates binaires
4.4 Accélération plate
4.4.1 Accélération plate pour fonctions Presburger-affines
4.4.2 Accélération plate convexe
4.4.3 Accélération plate de translations positives
4.4.4 Expérimentations
4.5 Réduction pour les systèmes à compteurs
4.5.1 Une réduction dédiée aux compteurs
4.5.2 Accélération de boucles imbriquées
4.5.3 Réduction de la longueur des cycles à considérer
4.5.4 Expérimentations
4.6 Conclusion
5 Fast et la vérification du TTP
5.1 Introduction
5.1.1 Architecture
5.1.2 Outils similaires
5.2 Moteur de calcul
5.2.1 Architecture logicielle
5.2.2 Adaptation de l’heuristique access
5.2.3 Autres choix techniques
5.3 Entrées-sorties
5.3.1 Le système
5.3.2 La stratégie
5.3.3 Interface graphique
5.4 Expérimentations
5.4.1 À propos des tests
5.4.2 Le jeu de tests
5.4.3 Résultats
5.4.4 Validation de l’heuristique
5.5 Comparaison à d’autres outils
5.5.1 Les différents outils
5.5.2 Comparaison calcul en avant exact
5.5.3 Co-accessibilité et couverture
5.5.4 Commentaires
5.6 Vérification du protocole TTP
5.6.1 Présentation du protocole TTP
5.6.2 Modélisation
5.6.3 Vérification automatique pour une défaillance
5.6.4 Vérification pour deux défaillances
5.6.5 Résultats
5.6.6 Vérification avec Alv, Lash et TReX
5.7 Vérification du protocole CES
5.7.1 Le protocole CES
5.7.2 Simulation par système à compteurs
5.7.3 Correction de la modélisation des files
5.7.4 Vérification avec Fast
5.7.5 Résultats
5.7.6 Vérification avec Alv et Lash
5.8 Conclusion
III Vérification de systèmes à pointeurs
6 Cadre des systèmes à pointeurs
6.1 Introduction
6.1.1 Contexte
6.1.2 Cadre des systèmes à pointeurs
6.1.3 Approches existantes
6.2 Systèmes à pointeurs
6.2.1 Domaine d’interprétation : graphes mémoire
6.2.2 Actions des systèmes à pointeurs
6.2.3 Sémantique opérationnelle
6.2.4 Famille des systèmes à pointeurs
6.2.5 Propriétés des systèmes à pointeurs
6.3 Cadre symbolique : états mémoire symboliques
6.3.1 États mémoire symboliques
6.3.2 Isomorphisme d’états mémoire symboliques
6.3.3 Graphes mémoires minimaux
6.3.4 Forme atomique minimale
6.3.5 Forme minimale
6.3.6 Minimisation effective
6.3.7 Union, intersection, complément
6.3.8 Inclusion et test du vide
6.3.9 Successeurs symboliques
6.3.10 Propriétés
6.4 Abstraction de systèmes à pointeurs
6.4.1 Graphes mémoire abstraits
6.4.2 États mémoire symboliques abstraits
6.4.3 Graphes mémoire étanches
6.4.4 Graphes mémoire canoniques
6.4.5 Complément d’états mémoire symboliques abstraits
6.4.6 Résumé sur les états mémoire symboliques
6.5 Conclusion
Conclusion
Bibliographie
Télécharger le rapport complet
