Verification of communicating recursive programs via split-width

Vérification de programmes récursifs et communicants via split-width Cette thèse développe des techniques à base d'automates pour la vérification formelle de systèmes physiquement distribués communiquant via des canaux fiables de tailles non bornées. Chaque machine peut exécuter localement plusieurs programmes récursifs (multi-threading). Un programme récursif peut également utiliser pour ses calculs locaux des structures de données non bornées, comme des files ou des piles. Ces systèmes, utilisés en pratique, sont si puissants que tous leurs problèmes de vérification deviennent indécidables. Nous introduisons et étudions un nouveau paramètre, appelé largeur de coupe (split-width), pour l'analyse de ces systèmes. Cette largeur de coupe est définie comme le nombre minimum de scissions nécessaires pour partitioner le graphe d'une exécution en parties sur lesquelles on pourra raisonner de manière indépendante. L'analyse est ainsi réalisée avec une approche diviser pour régner. Lorsqu'on se restreint à la classe des comportements ayant une largeur de coupe bornée par une constante, on obtient des procédures de décision optimales pour divers problèmes de vérification sur ces systèmes tels que l'accessibilité, l'inclusion, etc. ainsi que pour la satisfaisabilité et le model checking par rapport à divers formalismes comme la logique monadique du second ordre, la logique dynamique propositionnelle et des logiques temporelles. On montre aussi que les comportements d'un système ont une largeur de coupe bornée si et seulement si ils ont une largeur de clique bornée. Ainsi, grâce aux résultats de Courcelle sur les graphes de degré uniformément borné, la largeur de coupe est non seulement suffisante, mais aussi nécessaire pour obtenir la décidabilité du problème de satisfaisabilité d'une formule de la logique monadique du second ordre. Nous étudions ensuite l'existence de contrôleurs distribués génériques pour nos systèmes distribués. Nous proposons plusieurs contrôleurs, certains ayant un nombre fini d'états et d'autres étant déterministes, qui assurent que les comportements du système sont des graphes ayant une largeur de coupe bornée. Un système ainsi contrôlé de manière distribuée hérite des procédures de décision optimales pour les différents problèmes de vérification lorsque la largeur de coupe est bornée. Cette classe décidable de système généralise plusieurs sous-classes décidables étudiées précédemment.