Soutenance mémoire
Télécharger le fichier pdf d’un mémoire de fin d’études
L’ensemble d’atteignabilité vu comme un calcul de point-fixe
De fait, la sémantique d’un programme peut être vue comme un système de transition hC;C0; !i, son ensemble d’atteignabilité est Post (C0). Nous introduisons alors la fonction : F : 2C 7!2C X 7!C0 [ Post( X ).
Le plus petit point-fixe de cette fonction dans le treillis = 2C , noté lfp(F), est égal à Post (C0). Le théorème de Kleene nous donne donc un moyen de calculer cet ensemble d’atteignabilité. Cependant, pour rendre ce calcul e ectif, il nous faut faire des approximations.
En interprétation abstraite, deux méthodes d’approximation sont employées pour approximer ce plus petit point-fixe :
1. Les approximations statiques : plutôt que de chercher le plus petit point-fixe de F dans son treillis
original ( ; v), nous calculons le plus petit point-fixe de son abstraction F] dans un treillis abstrait ( ; v] ), lié à à l’aide d’une correspondance de Galois. Le treillis abstrait est choisi de telle manière que le calcul d’un point-fixe dans ce treillis est plus simple à calculer que dans l’original.
2. Les approximations dynamiques : quand un treillis abstrait ne satisfait pas la condition de chaîne ascendante, on cherche à deviner la limite de la suite (un )n 2N à l’aide d’un opérateur d’élargisse-ment qui assure la terminaison du calcul au prix d’une certaine approximation.
Approximations statiques : correspondance de Galois
Nous supposons que le treillis (dit concret) ( ; v) est un treillis complet et nous considérons un autre treillis, dit abstrait, ( ; v] ). Une correspondance de Galois est donnée par deux fonctions : 7! et : 7! qui sont respectivement la fonction d’abstraction et la fonction de concrétisation, définies telles que : 8s 2 ; 8a 2 ; (s) v] a , s v (a).
Cette correspondance de Galois est notée :v] ).
Aussi, F] est définie par F] = F , avec la propriété suivante : lfp(F) v (lfp(F] ) ).
Le calcul de lfp(F] ) donne alors une sur-approximation de lfp(F)..
Combinaison de domaines abstraits
Comme présenté dans [CCF13], il est possible de combiner deux domaines abstraits. Une première méthode est d’e ectuer un produit cartésien. Formellement, soit (A; vA; uA; tA ) et (B; vB; uB; tB ), deux domaines abstraits, le produit cartésien de ceux-ci donne le domaine abstrait (C; vC; uC; tC ) où C est le produit des éléments des treillis et la relation d’ordre vC est la conjonction des relations d’ordre : (a1; b1) vC (a2; b2) , a1 vA a2 ^ b1 vB b2 où a1; a2; b1; b2 sont des éléments des treillis. Les opéra-teurs de bornes sont définis par leurs applications un-à-un : (a1; b1) tC (a2; b2) = (a1 tA a2; (b1 tB b2) ) ; (a1; b1) uC (a2; b2) = (a1 uA a2; (b1 uB b2) ). Pareillement, il est possible de combiner les opérateurs d’élargissement et les fonctions de transfert en les appliquant aux éléments associés. On peut définir la fonction d’abstraction comme le produit des applications des deux fonctions d’abstraction sur un élé-ment du domaine concret C (c) = ( A (c); B (c) ). La fonction de concrétisation nécessite cependant d’e ectuer l’intersection des résultats des applications : C ( a; b ) = A ( a ) u B ( b ). Se faisant, ce produit cartésien forme une correspondance de Galois avec le domaine concret : ( ; ) C.
Ainsi, la sémantique du produit cartésien est une sur-approximation sûre de la sémantique concrète. Cependant, le produit cartésien peut contenir des éléments redondants. Par exemple, si l’on considère le produit de deux domaines numériques : celui des intervalles et celui de la parité, les éléments ([2; 4]; Impair); ([2; 3]; Impair); ([3; 4]; Impair) et ([3; 3]; Impair) peuvent être concrétisés en single-ton 3.
Bien que le produit cartésien soit une manière e cace et peu coûteuse de combiner deux domaines abstraits, il est souhaitable que les domaines puissent échanger de l’information dans le but de se ra ner mutuellement. Ce mécanisme se nomme produit réduit [CC77, CCM11]. Soit (a; b) un élément d’un produit réduit composé de deux éléments de deux domaines abstraits di érents et soit c1 et c2 les deux ensembles d’éléments concrets associés à a et b alors (a; b) représente l’ensemble c1 \ c2. La réduction essaie de trouver le plus petit élément (a0; b0) tel que a0 v a et b 0 v b mais leur intersection reste égale à c1 \ c2. La structure de treillis et la sémantique associée restent les mêmes que pour le produit cartésien mais, nous introduisons en plus un opérateur de réduction visant à ra ner les informations portées par les deux domaines et est utilisé après chaque application sémantique. L’opérateur de réduction est défini par : f(a 0; b0) 2 A B j (a; b) v (a 0; b0)g. En général, cette définition n’est pas calculable et on cherche plutôt une version plus relâchée et peu coûteuse. Toutefois, un opérateur de réduction doit satisfaire deux propriétés : le résultat de la réduction doit être un élément abstrait plus précis (a; b) v (a; b) et un élément abstrait et sa réduction conservent les mêmes propriétés ( (a; b) ) = (a; b).
Vérification des propriétés de sûreté
La finalité d’une analyse de programme est de vérifier le « bon comportement » d’un programme. Ce bon comportement peut se traduire par un ensemble de propriétés de sûreté que notre programme se doit de respecter afin d’assurer qu’il ne comporte pas de défaillances critiques. En interprétation abstraite, le résultat d’une analyse est une sur-approximation de l’espace d’états atteignables. Ainsi, prouver le bon comportement d’un programme revient à montrer l’absence de mau-vais comportements . En e et, l’abstraction engendrée peut contenir des comportements pouvant ne pas avoir lieu lors d’une exécution. En revanche, si l’abstraction ne contient pas de mauvais comportements alors nous sommes sûrs que notre programme est correct.
Formellement, soit un ensemble de mauvaises configurations construites à partir des propriétés et
S une sur-approximation de l’espace d’atteignabilité d’un programme :
— Si S \ = ; alors les propriétés sont prouvées .
— Sinon S \ , ; alors deux possibilités .
— L’abstraction contient des mauvaises configurations et celle-ci doit être ra née, on parle alors de fausse alarme .
— L’implantation ne respecte pas la propriété et un bug est présent.
Outils industriels
La théorie de l’interprétation abstraite sort du cadre théorique pour concevoir de nombreux outils d’analyses statiques qui ont été développés et appliqués à des problèmes du « monde réel ». La plu-part des outils existants se concentrent sur l’analyse de code C et sont généralement appliqués à des programmes de l’embarqué critique nécessitant un haut-niveau de certification.
Nous présentons quelques uns des outils reposant sur l’interprétation abstraite.
Frama-C / EVA — [KKP+15] Frama-C est une plate-forme extensible d’analyse statique et de spécification de programmes C. Frama-C dispose d’un système de gre ons pouvant spécialiser di érents types d’analyse. Parmi les gre ons existants, EVA (Evolved Value Analysis), la nouvelle version de Value, utilise l’interprétation abstraite au travers d’une architecture modulaire comprenant un nombre conséquent de domaines abstraits. Frama-C est utilisé, par exemple, dans la vérification de code critique dans l’industrie du nucléaire. Par ailleurs, c’est sur cet outil que nous nous sommes basés pour réaliser l’implantation de notre prototype que nous présentons plus loin. AstrØe — [BCC+02, BCC+03, CCF+05, CCF+09]Astrée est un interpréteur abstrait initialement développé au sein du laboratoire d’informatique de l’École Normale Supérieure en 2001 puis acquis en 2009 par AbsInt. Astrée contient une grande variété de domaines abstraits permettant d’exprimer de nombreux types de propriétés abstraites et d’établir des invariants numériques précis. Astrée possède un système de combinaisons de domaines abstraits basé sur des collaborations par passage de messages. Airbus compte parmi ses utilisateurs historiques.
Verasco — [JLB+15] Verasco est une analyseur par interprétation abstraite formellement prouvé grâce à l’assistant de preuve Coq. Il est intégré au compilateur pour C CompCert [Ler09], lui-même vérifié de la même manière. Ils collaborent de telle manière que les propriétés de sûreté établies par Verasco lors de la compilation peuvent être propagées au binaire généré.
Polyspace — [Deu03] Polyspace est un interpréteur abstrait de code C, C++ et ADA. Comme les outils présentés jusqu’ici, il est capable de détecter des erreurs à l’exécution et de valider des proprié-tés de sûreté. Il dispose d’une interface aboutie et est développé par MathWorks. Il est déployé dans di érents contextes industriels (automobiles, ferroviaire, avionique, spatial, : : :).
Clousot — [FL10] Clousot détecte les erreurs à l’exécution et vérifie des contrats de spécifica-tions de fonctions. Il analyse chaque fonction d’un programme de manière isolée et utilise des pré/post-conditions pour cela. Cet analyseur prend en entrée du code objet (bytecode) de la machine virtuelle .Net de Microsoft.
Vérification de programmes concurrents
La concurrence en informatique s’intéresse à l’exécution de plusieurs processus communiquant entre eux. Les processus peuvent être exécutés de manière parallèle (i.e. ayant chacun une unité de calcul dédiée) ou encore peuvent être agencés, par exemple, sur un seul processeur où un mécanisme d’ordon-nancement leur permettra de prendre la main selon des critères spécifiés. Aujourd’hui, la grande majorité des langages de programmation, tous paradigmes confondus, pro-posent des approches pour programmer de manière concurrente. Cela peut se manifester par une ap-plication web attribuant à chaque client un processus dédié pour répondre à ses requêtes, à des noyaux de calcul d’unité de calcul graphique (Graphics Processing Unit) pour a cher des images ou encore pour des calculs numériques divisés en sous-parties disposées sur plusieurs fils d’exécution à des fin d’accélération. Il existe aussi des propositions en vue de l’intégration de systèmes concurrents dans de l’embarqué critique [WW07].
Cependant, la concurrence est di cile à programmer et encore plus à vérifier. À la di érence du séquentiel, on y trouve de nouvelles problématiques :
— L’orchestration des processus où le non-déterminisme dans la séléction des processus exécutés entraîne une explosion combinatoire du nombre d’états possibles .
— Les situations de compétition (data race) où deux processus tentent d’accèder à une ressource partagée et où, au moins, l’un d’eux modifie celle-ci entraînant généralement des comportements indésirables .
— L’interblocage où un ensemble de processus s’attendent mutuellement pour pouvoir reprendre leurs exécutions et entraînant ainsi un blocage global .
— La famine de processus tentant d’accéder indéfiniment à une ressource « capturé » par d’autres et ne leur permettant plus de l’atteindre. Un exemple de cette situation est le dîner des philo-sophes formulé par Dijkstra [Dij83] : plusieurs philosophes sont disposés autour d’un repas. Il est nécessaire à un philosophe de posséder deux fourchettes pour manger son plat, or le nombre de fourchettes est égal au nombre de philosophes ainsi si chaque philosophe en empoigne une, aucun ne sera capable de manger son plat.
Dans cette section, nous présentons quelques exemples de modèle de concurrence, puis nous intro-duisons quelques travaux de vérification par analyse statique, en particulier, ceux utilisant la méthodo-logie de l’interprétation abstraite.
Modèles de concurrence
Il est important de distinguer les di érents traits caractérisant les modèles de concurrence. Premiè-rement, la mémoire peut être soit partagée, tous les processus disposent du même espace d’adressage, soit distincte (ou répartie), chaque processus possèdent un espace propre auquel lui-seul peut accéder. Le problème de la vérification pour la mémoire partagée est accru de par la présence des mémoires faiblement cohérentes [ABBM10] sur certaines architectures. Les modèles d’exécution doivent alors également prendre en compte : les optimisations du matériel, la cohérence des caches, etc. Il est néces-saire, pour une vérification sûre, de considérer ces comportements lors de l’analyse.
Les processus peuvent, ou non, communiquer entre eux. On distingue deux grandes familles de modèles de communication entre processus :
— Dans le modèle à mémoire partagée, les communications peuvent avoir lieu au travers d’une variable partagée. Il est alors important de protéger les accès en lecture et écriture pour éviter les situations de compétitions comme précédemment évoquées .
— Il est également possible d’établir un protocole afin d’envoyer des messages contenant les don-nées en travaillant par copie. Par ailleurs, il existe di érentes manières d’implanter ce modèle comme, par exemple, l’utilisation d’une file d’attente pour stocker les messages en attente de réception.
Au sein du modèle de passage de messages, il est également possible de spécifier le comportement des envois et des réceptions. L’émetteur ou le récepteur peuvent attendre que l’autre participant soit prêt à e ectuer la communication. On dit que les communications sont synchrones. Ou, au contraire, l’émetteur peut continuer son exécution après avoir envoyé son message. On parle alors d’asynchro-nisme. Ce mécanisme permet de minimiser les temps d’attente liés aux communications et d’améliorer ainsi les performances du système. Néanmoins, les communications synchrones ont pour avantage d’être conceptuellement moins complexes. Un autre aspect de la concurrence à considérer est la possibilité qu’un programme a de créer de nouveaux processus que ceux présents à un état initial. En particulier, certains algorithmes peuvent se contenter d’un nombre fixe de processus pour e ectuer leurs calculs mais il existe des situations où créer ou détruire des processus est utile. Par exemple, un serveur web peut démarrer un nouveau processus servant les requêtes d’un client lorsque celui-ci se connecte.
Lors de l’exécution, il est également important de spécifier quel processus doit avoir la priorité pour s’exécuter si leur nombre est supérieur aux unités de calculs attribuées au programme. Deux possibilités existent : le comportement préemptif, où un ordonnanceur attribue à chaque processus une portion de temps de calcul puis cède la main à un processus de manière arbitraire, généralement à l’aide d’une notion de priorité ; le comportement coopératif où chaque processus doit explicitement céder la main aux autres processus pour qu’ils puissent s’exécuter.
Nous présentons maintenant quelques uns des grands modèles de concurrences :
-calcul . Le -calcul [MPW92] est une algèbre de processus permettant de modéliser de manière formelle des systèmes concurrents. Un système écrit en -calcul décrit un terme représentant un ensemble de processus fP;Q; R; : : :g capables de manipuler des noms. Ces noms décrivent des canaux de communi-cations permettant lecture et écriture par tout processus les connaissant. Le -calcul incorpore alors la notion de passage de message par file d’attente modélisé par les canaux. Les émissions sont, par défini-tion, asynchrones. Il est également possible de paralléliser deux processus P j Q ou d’e ectuer un choix non-déterministe entre l’exécution de deux processus P + Q. Des extensions du -calcul proposent la réplication de processus modélisant ainsi une forme de création dynamique. La vérification du -calcul a été largement étudiée dans la littérature [Dam93, Fer05] où la méthode la plus utilisée repose sur le model checking que nous détaillerons par la suite.
Le modèle Bulk Synchronous Parallel [Val90] est un paradigme de concurrence permettant de re-présenter des calculs parallèles. Le programme exécuté est divisé en super étapes (superstep) où chacun des N processus (où N est fixé) va réaliser son calcul local, e ectuer jusqu’à N 1 communications (soit par passage message, soit par mémoire partagée) puis se mettre en attente via une barrière de syn-chronisation que tous les processus doivent atteindre pour conclure un superstep. Un tel partitionnement des calculs a pour avantage de ne pas pouvoir créer de situation de compétition puisque les barrières empêchent les dépendances circulaires entre données. De plus, l’intérêt de cette approche est de pou-voir prédire de manière relativement simple les performances d’un algorithme. En e et, le coût d’un superstep sera nécessairement le coût du processus le plus coûteux en temps. Il est également possible de modéliser des programmes BSP sous la forme d’automates [Hai17, TLHL17] introduisant alors une sémantique claire et facilitant la vérification de tels programmes.
Analyse statique de programmes concurrents par interprétation abstraite
Dans cette section, nous nous intéressons plus particulièrement aux approches d’analyse statique utilisant la méthode de l’interprétation abstraite.
Un des premiers travaux s’intéressant à l’utilisation de l’interprétation abstraite pour la vérification de modèles de concurrence a été [Fer05] dans lequel l’auteur s’intéresse à la vérification de systèmes écrits en -calcul. Pour ce faire, une sémantique opérationnelle du -calcul est introduite afin de pou-voir utiliser la méthodologie de l’interprétation abstraite. Celle-ci permet de construire deux analyses distinctes : une analyse de flot de contrôle permettant de connaître les canaux de communications em-ployés par chaque processus ; une analyse de comptage d’occurrences qui, dans ce modèle qui permet aux processus de se répliquer, permet de borner le nombre d’instances potentiellement créées. Ainsi, et grâce à la combinaison de ces deux analyses, il est par exemple possible après avoir modélisé un serveur ftp de conclure que le nombre maximum de processus travaillant sur des calculs ne dépassera jamais la limite imposé par le système.
Une des techniques les plus abouties et qui a mené à des prototypes utilisés industriellement est celle, proposée dans [Min12, Min13, Min14] qui a été auparavant proposée par [CH09]. L’idée développée dans ces travaux s’inspire de la méthode de preuve rely-guarantee [Jon83]. Celle-ci permet d’étendre la logique de Hoare aux programmes concurrents notamment en introduisant la possibilité de spécifier des attentes, sous la forme d’invariants, sur l’ensemble des fils d’exécution d’un programme.
Cette méthode s’intéresse à un modèle de concurrence comportant un ensemble fini de processus et un modèle à mémoire partagée. Pour donner une meilleure intuition du modèle, l’outil développé s’ap-plique à la bibliothèque POSIX Threads [But97] sans création dynamique de processus (i.e. les threads sont initialisés au début du programme dans une boucle explicitement bornée). Les communications sont donc réalisées par lectures et écritures de variables partagées. L’idée de cette méthode est de com-mencer par e ectuer une analyse de valeurs classique (par interprétation abstraite) sur chaque thread de manière locale. Cependant, chaque écriture de variable partagée peut avoir un e et de bord sur le flot de contrôle d’un thread di érent. On appelle cet e et une interférence. Ainsi, après cette première analyse, on collecte l’ensemble des interférences possibles en les intégrant à une nouvelle analyse de valeurs. Cependant, de nouveaux comportements peuvent être découverts et, de même, de nouvelles interférences sont possibles. Ce processus est donc réitéré jusqu’à obtenir un point-fixe. Pour illustrer ceci, considérons le programme multi-thread présenté par la Figure 2.4. Les deux threads s’exécutent de manière parallèle et influent l’un sur l’autre de par les écritures des variables partagées X et Y . En supposant X = Y = 0, une première analyse de valeurs, avec les intervalles pour domaine abstrait, donnerait les états finaux suivants : t1 = fX = [0; 0] ; Y = [0; 0]g et t2 = fX = [0; 0] ; Y = [0; 5]g. Après cette itération, l’interférence capturée est « t2 écrit dans Y la valeur abstraite [1; 5] ». En injec-tant cette interférence et en réitérant une analyse, nous obtenons : t1 = fX = [0; 5] ; Y = [0; 5]g et t2 = fX = [0; 0] ; Y = [0; 5]g. La nouvelle interférence provient maintenant du thread t1 qui écrit dans X la valeur abstraite [1; 5]. Après injection et nouvelle analyse, les états de threads n’évoluent plus et nous obtenons l’invariant de programme suivant : X 2 [0; 5] ^ Y 2 [0; 5]. Il est à noter que nous n’obtenons pas l’invariant relationnel X Y . Toutefois, il est possible d’obtenir cet invariant en utilisant des domaines relationnels (e.g. octogones, polyèdres, : : 🙂 dans le but de conserver ces relations entre variables.
Langage de processus communiquants
Nous présentons, en Figure 3.1, la grammaire d’un langage concurrent. Ce langage impératif va permettre de décrire des systèmes concurrents où plusieurs processus s’exécutent en parallèle. Chacun de ces processus va pouvoir e ectuer des calculs numériques, réaliser des communications synchrones au sein du système et créer/détruire dynamiquement de nouveaux processus.
Notre langage possède une structuration par processus nommés : chaque processus exécutera le code de son bloc nommé. Chaque programme débute avec un seul processus lancé et exécutant le bloc main. Ce processus peut alors créer de nouveaux processus grâce aux instructions createL et createR re-cevant des expressions permettant de les initialiser. La mémoire est distribuée, ainsi chaque processus possède sa propre zone mémoire. De ce fait, il n’existe pas de notion de variable partagée. Les com-munications sont synchrones et doivent être symétriques : deux processus peuvent communiquer si l’un est en état d’envoi et l’autre en état de réception. Une fois la communication e ectuée, les processus peuvent progresser à nouveau. Chaque progression des processus est indépendante et entraîne donc des exécutions non-déterministes.
Nos programmes possèdent une notion d’ordre entre processus : chacun d’entre eux sera disposé sur un vecteur entraînant une notion de voisinage entre processus. Dans notre langage, nous limitons la création de nouveaux processus et les communications au voisinage de la position des processus : i.e. à gauche et/ou à droite. Ainsi, les nouveaux processus créés seront disposés à droite (resp. à gauche) de leur créateur qui vient d’exécuter l’instruction createR (resp. createL). Par exemple, un programme contenant initialement un processus P0 qui va créer un processus P1 à sa droite puis, de nouveau, un pro-cessus P2 à sa droite sera respectivement dans l’état hP0i, hP0 P1i, hP0 P2 P1i. Le même mécanisme est appliqué aux communications qui limiteront leur portée aux processus situés dans leur voisinage. Les communications sont synchrones ce qui signifie que dans le cas où un processus tente de communiquer avec l’un de ses voisins qui n’est pas en attente de communication, il sera bloqué jusqu’à ce que son voi-sin soit prêt à communiquer. De plus, si aucun voisin n’est présent pour communiquer (e.g. un processus communiquant à sa gauche tout en étant au début du vecteur) le processus sera bloqué de même.
Nous donnons en exemple, Figure 3.2, un programme reprenant l’idée du passage de jeton (c.f. Figure 2.5) mais en y introduisant des calculs numériques. Dans cet exemple, le processus initial main crée 100 processus token à sa droite (hM0 T100 : : : T1i) qu’il initialise avec des entiers aléatoires compris entre 0 et 9. Après la phase de création, il envoie la valeur 0 au processus situé à sa droite pour démarrer le calcul puis s’auto-détruit. Les processus token_process vont, quant à eux, se mettre en attente d’une communication provenant de leur gauche et conserver la valeur maximum entre la valeur reçue et celle passée à l’initialisation. Finalement, ils envoient à leur tour leur résultat à leur droite avant.
Modélisation des communications
Habituellement, en Regular Model Checking, les communications dans un système sont exprimées via le transducteur par une suite de transitions définissant un chemin empruntable lorsque le système est dans un état particulier (e.g. échange de token Figure 2.5). Ce mécanisme est su sant lorsque l’on mani-pule des structures à alphabet fini. Cependant, pour un alphabet infini, nous ne pouvons pas représenter ces communications sous cette forme. En e et, cela nécessiterait de traiter, pour chaque communication, toutes les valeurs possibles reconnues par les gardes et nécessiterait un nombre, potentiellement infini, d’états et/ou de transitions. Pour cette raison, nous encodons nos communications à l’aide de transitions possédant des gardes multiples. Se faisant, nos fonctions de réécriture associées reçoivent en argument chacun des éléments gardés. Ainsi, nous donnons aux fonctions de réécriture les contextes complets des processus e ectuant une communication.
Nous illustrons ce mécanisme par la Figure 3.4 où l’on manipule des processus dont les états sont représentés par le produit de deux treillis : celui des jetons (i.e. un treillis composé de deux atomes : ft; ng) et celui des intervalles. Le transducteur étendu que nous donnons stipule qu’une communication n’est possible entre deux processus que lorsque le premier possède le jeton et est suivi par un second processus sans le jeton. La sémantique de cette communication est de transmettre le jeton au deuxième et d’ajouter sa valeur à celle du processus recevant le jeton. Comme les états des deux processus reconnus par la garde sont passés en paramètre de chaque fonction de réécriture, celles-ci sont alors capables de raisonner sur les deux états pour en calculer un nouveau. Ici, cela nous permet d’e ectuer une addition des valeurs de deux processus.
|
Table des matières
1 Introduction
1.1 Évolution du matériel
1.2 Bug logiciel
1.3 Vérification logicielle
1.4 Objectifs et contributions
1.5 Plan du document
2 État de l’art
2.1 Préliminaires
2.1.1 Systèmes de transitions
2.1.2 Ordres partiel et treillis
2.1.3 Points-fixes
2.2 Interprétation Abstraite
2.2.1 L’ensemble d’atteignabilité vu comme un calcul de point-fixe
2.2.2 Approximations statiques : correspondance de Galois
2.2.3 Approximations dynamiques : opérateur d’élargissement
2.2.4 Domaines abstraits
2.2.5 Combinaison de domaines abstraits
2.2.6 Vérification des propriétés de sûreté
2.2.7 Outils industriels
2.3 Vérification de programmes concurrents
2.3.1 Modèles de concurrence
2.3.2 Analyse statique de programmes concurrents par interprétation abstraite
2.4 Langages réguliers et automates
2.5 Regular Model Checking
2.5.1 Transducteurs à états finis
2.5.2 Représentation des systèmes
2.5.3 Calcul de l’espace d’atteignabilité
2.6 Transducteurs symboliques
2.7 Automates de treillis
2.8 Conclusion
3 Analyse statique de processus communiquants par voisinage
3.1 Modélisation du système
3.2 Langage de processus communiquants
3.3 Sémantique du système
3.3.1 Définition du transducteur
3.3.2 Modélisation des communications
3.3.3 Création et destruction dynamique
3.3.4 Règles sémantiques
3.4 Sémantique abstraite du système
3.4.1 Transducteurs de treillis
3.5 Vérification du système
3.5.1 Algorithme d’application
3.5.2 Calcul de l’espace d’atteignabilité
3.5.3 Exemple : Moonrobot
3.6 Conclusion
4 Sémantique de communications point-à-point et collectives
4.1 Langage du modèle
4.1.1 Communications point-à-point
4.1.2 Communications collectives
4.2 Sémantique des règles
4.2.1 Définition
4.2.2 Sémantique abstraite des communications
Création dynamique de processus avec taille
Communications point-à-point
Communications collectives
4.3 Vérification du système
4.3.1 Algorithme d’application des règles
Complexité
Correction
4.3.2 Initialisation de la vérification
Configuration initiale
Sélection des domaines abstraits
Traduction vers le modèle
4.4 Calcul de l’espace d’atteignabilité
4.5 Optimisation par ranement de partitions
4.6 Conclusion
5 Application à MPI
5.1 Introduction à MPI
5.1.1 Notions générales
5.1.2 Sous-ensemble des primitives et du langage
Communications point-à-point
Communications collectives
Création dynamique de processus
5.2 Implantation du prototype
5.2.1 Traduction automatique des primitives MPI/C
5.2.2 Domaines abstraits
5.2.3 Analyse et stratégie d’itération
5.2.4 Conclusion
6 Expérimentations
6.1 Comparaison avec ISP
6.1.1 Détection d’interblocages
6.1.2 Passage à l’échelle
6.1.3 Avantages de l’analyse statique
6.2 Analyses de valeurs
6.2.1 Calcul de séries
6.2.2 Calculs numériques avec création dynamique
6.3 Conclusion
7 Conclusion
7.1 Contributions
7.2 Perspectives
Bibliographie
Télécharger le rapport complet
