Caractérisation de points-fixes concluants par formules logiques

Dans la complétion d’automates d’arbres, la vérification d’une propriété de sûreté consiste à montrer qu’un ensemble de termes interdits Bad ne peut pas être atteint de- puis un ensemble d’états initiaux. Étant donné que l’ensemble des états accessibles n’est généralement pas calculable, une sur-approximation de cet ensemble est généralement calculée. La principale difficulté de ce calcul est de calculer une sur-approximation suf- fisamment précise pour ne pas accepter de termes interdits, et apporter une réponse au problème de vérification. Autrement dit, cette sur-approximation doit être concluante. Comme nous l’avons vu en section 3.3, cette précision est le plus souvent définie ma- nuellement par un paramétrage implémentant le calcul de la sur-approximation. Nous proposons alors dans ce chapitre une caractérisation de ce qu’est une sur- approximation concluante, par des formules logiques générées grâce à un nouveau type d’automate appelé automate d’arbres symbolique. Résoudre ces formules, pour une taille d’automate d’arbres symbolique donnée, permet alors de trouver une sur-approximation concluante de taille équivalente, sans avoir recours à aucun paramétrage manuel. Si aucune solution n’est trouvée pour la taille donnée, alors la taille de l’automate d’arbres symbolique est augmentée et le calcul des formules est répété.

Nous avons vu lors des chapitres précédents de cette thèse, que la technique de vérifi- cation que nous utilisons représente les ensembles de configurations du système par des automate d’arbres, et le comportement du système par un système de réécriture. Rap- pelons brièvement que dans ce contexte, les auteurs de [Genet et Rusu, 2010, Feuillade et al., 2004] proposent une analyse d’atteignabilité grâce à un algorithme de complé- tion (section 2.4). Soit Bad un ensemble de termes interdits, la complétion consiste donc à prouver qu’aucun des éléments de Bad n’est accessible, en calculant une sur- approximation régulière de l’ensemble des termes accessibles qui ne contienne aucun termes interdit. Cette technique est paramétrée par une fonction d’approximation ou un ensemble d’équations (section 2.4.2) : ce paramétrage détermine la qualité de l’ap- proximation et se révèle donc crucial pour l’analyse d’atteignabilité.tème. En revanche, si le langage de la sur-approximation calculée contient des termes interdits, il s’agit peut-être de faux contre-exemples. Dans ce cas, cela signifie que le pa- ramétrage choisi pour l’approximation n’est pas le bon et que l’algorithme de complétion calcule une sur-approximation trop grossière. Afin d’éliminer les faux contre-exemples, on doit alors procéder à un raffinement de l’abstraction, mais cette procédure est géné- ralement coûteuse (voir section 3.3.6).Or il est difficile d’établir une bonne fonction d’approximation permettant de calculer une sur-approximation suffisamment fine pour de pas admettre de faux contre-exemple. Ce paramétrage requiert souvent une expertise hautement spécialisée pour pouvoir es- pérer une analyse concluante : le vérificateur doit alors maitriser à la fois la technique d’approximation utilisée et le type de système vérifié. Dans [Boichut et al., 2006], où les auteurs proposent une vérification des programmes Java par complétion d’automate d’arbres, les approximations doivent être très précisément définies pour permettre la convergence du système, nécessitant une étude préalable très pointue.

Par la suite, une sur-approximation concluante peut également être appelée point-fixe concluant. Afin de calculer un point-fixe concluant, nous caractérisons, par une formule logique, les critères permettant d’obtenir une telle approximation dans le cadre de la technique de complétion proposée par [Genet, 1998, Feuillade et al., 2004, Genet et Rusu, 2010]. Au lieu de raisonner avec des automate d’arbres classiques, ces derniers sont généralisés par un automate d’arbres symbolique AS (Symbolic Tree Automaton :et R un système de réécriture. Les formules caractérisant un point-fixe concluant pour A et R sont composées de combinaisons booléennes d’égalités ou d’inégalités sur les variables de l’automate d’arbres symbolique (STA) correspondant à A. Étant donné queseur calculé à chaque étape de complétion est déjà déterminé par la fonction d’approxi- mation ou l’ensemble d’équations. Il n’y a alors qu’un successeur possible, qu’un chemin possible, et un seul résultat. Si l’approximation n’est pas assez fine, il faut alors revenir en arrière et changer le paramétrage (voir section 3.3.6 et [Boichut et al., 2008a, Boi- chut et al., 2012]). Dans notre cas, un STA permet de représenter tous les successeurs possibles à une étape donnée de la complétion : toutes les instances possibles d’un STA représentent toutes les approximations possibles à une étape donnée. La figure 4.2 représente trois approximations possibles, selon trois instanciations différentes des va- riables X1 à X4 de l’automate d’arbres symbolique. Soit AS le STA possédant les transi.