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
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2006/23845 |
| Date | 08 1900 |
| Creators | Mathieu, Vincent |
| Contributors | Desharnais, Jules |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | text/html, application/pdf |
| Rights | © Vincent Mathieu, 2006 |
Page generated in 0.0019 seconds