L’algèbre de Kleene est la théorie algébrique des automates finis et des expressions régulières. Récemment, Kozen a proposé un cadre de travail basé sur l’algèbre de Kleene avec tests
(une variante de l’algèbre de Kleene) pour vérifier qu’un programme satisfait une politique
de sécurité spécifiée par un automate de sécurité. Malheureusement, cette approche ne permet
pas de vérifier des propriétés de vivacité pour les programmes réactifs (programmes qui
s’exécutent à l’infini). Le but de ce mémoire est d’étendre la méthode de vérification de programmes
proposée par Kozen pour enlever cette limitation. Pour y arriver, nous développons
la théorie de l’oméga-algèbre (une extension de l’algèbre de Kleene qui prend en compte
les exécutions infinies) qui constitue la majeure partie de ce mémoire. En particulier, nous
présentons des résultats de complétude concernant la théorie de Horn de cette algèbre. / Kleene algebra is the algebraic theory of finite automata and regular expressions. Recently,
Kozen has proposed a framework based on Kleene algebra with tests (a variant of
Kleene algebra) for verifying that a program satisfies a security policy specified by a security
automaton. Unfortunately, this approach does not allow to verify liveness properties for
reactive programs (programs that execute forever). The goal of this thesis is to extend the
framework proposed by Kozen for program verification to remove this limitation. For that,
we develop the theory of omega algebra, an extension of Kleene algebra suitable for reasoning
about nonterminating executions. The main part of this thesis is about omega algebra.
In particular, we show some completeness results about the Horn theory of omega algebra. / Inscrit au Tableau d'honneur de la Faculté des études supérieures
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2006/23728 |
| Date | 07 1900 |
| Creators | Bolduc, Claude |
| 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 | © Claude Bolduc, 2006 |
Page generated in 0.0021 seconds