Vérification des systèmes à pile au moyen des algèbres de Kleene

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007La vérification de modèle est une technique permettant de faire un modèle représentant le comportement d'un système ou d'un programme, de décrire une propriété à vérifier sur ce dernier et de faire la vérification au moyen d'un algorithme. Dans ce mémoire, nous décrivons notre propre méthode de vérification de modèle basée sur les algèbres de Kleene. Plus particulièrement, nous utilisons une extension appelée omégaalgèbre avec domaine. Cette méthode algébrique permet de vérifier des propriétés pouvant être exprimées au moyen de la logique CTL* basée sur les états et les actions du modèle à vérifier. Nous représentons ces propriétés au moyen d'expressions sur une oméga-algèbre avec domaine.Les modèles que nous pouvons vérifier sont les systèmes à pile, une classe de systèmes de transitions pouvant avoir un nombre infini d'états. Les systèmes à pile peuvent représenter le flot de contrôle des programmes avec appels de procédures, incluant les appels récursifs. Des matrices sur une oméga-algèbre avec domaine sont utilisées pour représenter ces systèmes de transitions. Notre méthode génère, à partir de la matrice représentant le système à pile à vérifier et de l'expression représentant la propriété à vérifier sur ce dernier, une équation qu'il faut démontrer de façon axiomatique afin de conclure que le système satisfait la propriété