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

Authors: Mathieu, Vincent
Advisor: Desharnais, Jules
Abstract: 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.
Document Type: Mémoire de maîtrise
Issue Date: 2006
Open Access Date: 12 April 2018
Permalink: http://hdl.handle.net/20.500.11794/18717
Grantor: Université Laval
Collection:Thèses et mémoires

Files in this item:
SizeFormat 
23845.pdf692.8 kBAdobe PDFView/Open
All documents in CorpusUL are protected by Copyright Act of Canada.