Thèse (Ph. D.)--Université Laval, 2009. / Titre de l'écran-titre (visionné le 25 mars 2009). Bibliogr.

Thèse (M.Sc.)--Université Laval, 2009. / Titre de l'écran-titre (visionné le 16 juin 2009). Bibliogr.

Augsburg, University, Diss., 2003.

Nous rappelons d’abord le concept d’algèbre de Kleene avec domaine (AKD). Puis, nous expliquons comment utiliser les opérateurs des AKD pour définir un ordre partiel appelé raffinement démoniaque ainsi que d’autres opérateurs démoniaques (plusieurs de ces définitions proviennent de la littérature). Nous cherchons à comprendre comment se comportent les AKD munies des opérateurs démoniaques quand on exclut les opérateurs angéliques usuels. C’est ainsi que les propriétés de ces opérateurs démoniaques nous servent de base pour axiomatiser une algèbre que nous appelons Algèbre démoniaque avec domaine et opérateur t-conditionnel (ADD-[opérateur t-conditionnel]). Les lois des ADD-[opérateur t-conditionnel] qui ne concernent pas l’opérateur de domaine correspondent à celles présentées dans l’article Laws of programming par Hoare et al. publié dans la revue Communications of the ACM en 1987. Ensuite, nous étudions les liens entre les ADD-[opérateur t-conditionnel] et les AKD munies des opérateurs démoniaques. La question est de savoir si ces structures sont isomorphes. Nous démontrons que ce n’est pas le cas en général et nous caractérisons celles qui le sont. En effet, nous montrons qu’une AKD peut être transformée en une ADD-[opérateur t-conditionnel] qui peut être transformée à son tour en l’AKD de départ. Puis, nous présentons les conditions nécessaires et suffisantes pour qu’une ADD-[opérateur t-conditionnel] puisse être transformée en une AKD qui peut être transformée à nouveau en l’ADD-[opérateur t-conditionnel] de départ. Les conditions nécessaires et suffisantes mentionnées précédemment font intervenir un nouveau concept, celui de décomposition. Dans un contexte démoniaque, il est difficile de distinguer des transitions qui, à partir d’un même état, mènent à des états différents. Le concept de décomposition permet d’y arriver simplement. Nous présentons sa définition ainsi que plusieurs de ses propriétés. / We first recall the concept of Kleene algebra with domain (KAD). Then we explain how to use the operators of KAD to define a demonic refinement ordering and demonic operators (many of these definitions come from the literature). We want to know how do KADs with the demonic operators but without the usual angelic ones behave. Then, taking the properties of the KAD-based demonic operators as a guideline, we axiomatise an algebra that we call Demonic algebra with domain and t-conditional (DAD-[opérateur t-conditionnel]). The laws of DAD-[opérateur t-conditionnel] not concerning the domain operator agree with those given in the 1987 Communications of the ACM paper Laws of programming by Hoare et al. Then, we investigate the relationship between DAD-[opérateur t-conditionnel] and KAD-based demonic algebras. The question is whether every DAD-[opérateur t-conditionnel] is isomorphic to a KAD-based demonic algebra. We show that it is not the case in general. However, we characterise those that are. Indeed, we demonstrate that a KAD can be transformed into a DAD-[opérateur t-conditionnel] which can be transformed back into the initial KAD. We also establish necessary and sufficient conditions for which a DAD-[opérateur t-conditionnel] can be transformed into a KAD which can be transformed back into the initial DAD-[opérateur t-conditionnel]. Finally, we define the concept of decomposition. This notion is involved in the necessary and sufficient conditions previously mentioned. In a demonic context, it is difficult to distinguish between transitions that, from a given state, go to different states. The concept of decomposition enables to do it easily. We present its definition together with some of its properties.

Au fil des ans, l'algèbre de Kleene s'est avérée être un outil formel très pratique et flexible quant vient le temps de raisonner sur les programmes informatiques. Cependant, actuellement, la plupart des applications à l'analyse de programmes de l'algèbre de Kleene se font en sélectionnant un problème précis et en voyant comment l'algèbre de Kleene permet de le résoudre, ce qui limite les applications possibles. L'objectif visé par ce mémoire est de déterminer dans quelle mesure la résolution d'équations, en algèbre de Kleene, peut être utilisée en analyse de programmes. Une grande partie de ce mémoire est donc consacrée à la résolution de différents types d'équations dans différentes variantes de l'algèbre de Kleene. Puis nous montrons comment la vérification de programmes ainsi que la synthèse de contrôleurs peuvent tirer profit de la résolution d'équations en algèbre de Kleene.

La théorie des automates est apparue pour résoudre des problèmes aussi bien pratiques que théoriques, et ceci dès le début de l'informatique. Désormais, les automates font partie des notions fondamentales de l'informatique, et se retrouvent dans la plupart des logiciels. En 1974, Samuel Eilenberg proposa un modèle de calcul qui unifie la plupart des automates (transducteurs, automates à pile et machines de Turing) et qui a une propriété de modularité intéressante au vu d'applications reposant sur différentes couches d'automates ; comme cela peut être le cas en linguistique computationnelle. Nous proposons d'étudier les techniques permettant d'avoir des machines d'Eilenberg effectives. Cette étude commence par la modélisation de relations calculables à base de flux, puis continue avec l'étude de la simulation des machines d'Eilenberg définies avec ces relations. Le simulateur est un programme fonctionnel énumérant progressivement les solutions, en explorant un espace de recherche selon différentes stratégies. Nous introduisons, en particulier, la notion de machine d'Eilenberg finie pour laquelle nous fournissons une preuve formelle de correction de la simulation. Les relations sont une première composante des machines d'Eilenberg, la deuxième composante étant son contrôle, qui est défini par un automate fini. Dans ce contexte, on peut utiliser une expression régulière comme syntaxe pour décrire la composante de contrôle d'une machine d'Eilenberg. Récemment, un ensemble de travaux exploitant la notion de dérivées de Brzozowski, a été la source d'algorithmes efficaces de synthèse d'automates non-déterministes à partir d'expressions régulières. Nous faisons l'état de l'art de ces algorithmes, tout en donnant une implémentation efficace en OCaml permettant de les comparer les uns aux autres.

Covert channels are means of communication that allow agents in a system to transfer information in a manner that violates the system’s security policy. Covert channels have been well studied in the constrained and old sense of the term where two agents are communicating through a channel while an intruder interferes to hide the transmission of a message. In an increasingly connected world where modern computer systems consist of broad and heterogeneous communication networks with many interacting agents, distributed covert channels are becoming increasingly available. For these distributed forms of covert channels, there are shortcomings in the science, mathematics, fundamental theory, and tools for risk assessment, and for proposing mechanisms and design solutions for averting these threats. Since current formal methods for specifying concurrent systems do not provide the tools needed to efficiently tackle the problem of distributed covert channels in systems of communicating agents, this thesis proposes Communicating Concurrent Kleene Algebra (C²KA) which is an extension to the algebraic model of concurrent Kleene algebra (CKA) first presented by Hoare et al. C²KA is used to capture and study the behaviour of agents, and description logic is used to capture and study the knowledge of agents. Using this representation of agents in systems of communicating agents, this thesis presents a formulation and verification approach for the necessary conditions for the existence of distributed covert channels in systems of communicating agents. In this way, this thesis establishes a mathematical framework for the modelling, analysis, and mitigation of distributed covert channels in systems of communicating agents. This framework enhances the understanding of covert channels and provides a basis for thinking and reasoning about covert channels in new ways. This can lead to a formal foundation upon which guidelines and mechanisms for designing and implementing systems of communicating agents that are resilient to covert channels can be devised. / Thesis / Doctor of Philosophy (PhD)

Due to their increasing complexity, today’s computer systems are studied using multiple models and formalisms. Thus, it is necessary to develop theories that unify different approaches in order to limit the risks of errors when moving from one formalism to another. It is in this context that monoids, semirings and Kleene algebras with domain were born about a decade ago. The idea is to define a domain operator on classical algebraic structures, in order to unify algebra and the classical logics of programs. The question of completeness for these algebras is still open. It constitutes the object of this thesis. We define tree structures called trees with a top and represented in matrix form. After having given fundamental properties of these trees, we define relations that make it possible to compare them. Then, we show that, modulo a certain equivalence relation, the set of trees with a top is provided with a monoid with domain structure. This result makes it possible to define a model for semirings with domain and prove its completeness. We also define a model for -continuous Kleene algebras with domain as well and prove its completeness modulo a new axiom.

À cause de la complexité croissante des systèmes informatiques, ces derniers sont aujourd’hui étudiés au moyen de multiples modèles et formalismes. Ainsi, il est nécessaire de développer des théories qui unifient différentes approches aafn de limiter les risques d’erreurs lorsqu’on passe d’un formalisme à l’autre. C’est dans cette optique que les monoïdes avec domaine, demi-anneaux avec domaine et algèbres de Kleene avec domaine ont vu le jour, il y a environ une décennie. L’idée est de définir un opérateur de domaine sur des structures algébriques classiques, afin d’unifier l’algèbre et la logique des programmes. La question concernant la complétude pour ces algèbres est encore ouverte. Elle constitue l’objet de ce mémoire. Nous définissons des structures arborescentes appelées arbres avec sommet et représentées sous forme matricielle. Après avoir donné des propriétés fondamentales de ces arbres, nous définissons des relations permettant de les comparer. Ensuite, nous démontrons que, modulo une certaine relation d’équivalence, l’ensemble des arbres avec sommet est muni d’une structure de monoïde avec domaine. Ce résultat permet de définir un modèle pour les demi-anneaux avec domaine et d’en prouver la complétude. Nous définissons également un modèle pour les algèbres de Kleene avec domaine -continues et prouvons la complétude de ce dernier modulo un nouvel axiome. / Due to their increasing complexity, today’s computer systems are studied using multiple models and formalisms. Thus, it is necessary to develop theories that unify different approaches in order to limit the risks of errors when moving from one formalism to another. It is in this context that monoids, semirings and Kleene algebras with domain were born about a decade ago. The idea is to define a domain operator on classical algebraic structures, in order to unify algebra and the classical logics of programs. The question of completeness for these algebras is still open. It constitutes the object of this thesis. We define tree structures called trees with a top and represented in matrix form. After having given fundamental properties of these trees, we define relations that make it possible to compare them. Then, we show that, modulo a certain equivalence relation, the set of trees with a top is provided with a monoid with domain structure. This result makes it possible to define a model for semirings with domain and prove its completeness. We also define a model for -continuous Kleene algebras with domain as well and prove its completeness modulo a new axiom.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007 / 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é.