Return to search

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

La 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é. / Inscrit au Tableau d'honneur de la Faculté des études supérieures

Identiferoai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2006/23845
Date08 1900
CreatorsMathieu, Vincent
ContributorsDesharnais, Jules
PublisherUniversité Laval
Source SetsLibrary and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada
LanguageFrench
Detected LanguageFrench
TypeElectronic Thesis or Dissertation
Formattext/html, application/pdf
Rights© Vincent Mathieu, 2006

Page generated in 0.0019 seconds