No description available.

L’analyse statique des programmes est une technique de vérification qui permet de statuer si un programme est conforme à une propriété donnée. Pour l’atteinte de cet objectif, il faudrait disposer d’une abstraction du programme à vérifier et d’une définition des propriétés. Dans la mesure où l’outil de vérification prend place dans un cadre algébrique, la définition des propriétés ainsi que la modélisation du programme sont représentées sous la forme d’expressions régulières. Ce mémoire traite en premier lieu de la traduction des programmes écrits en langage C vers une abstraction sous forme d’expressions régulières. La méthode de traduction proposée, ainsi que les différentes étapes de transformations y sont exposées. Les premiers chapitres du présent mémoire énoncent les connaissances élémentaires de la théorie des langages ainsi que de la compilation des programmes. Un bref aperçu des différentes méthodes de vérification des programmes est présenté comme une mise en contexte. Finalement, la dernière partie concerne la traduction des programmes ainsi que la description de l’outil de traduction qui a été réalisé.

Les analyses interprocédurales automatiques de programmes qui sont basées sur des théories mathématiques rigoureuses sont complexes à réaliser, mais elles sont d'excellents outils pour augmenter notre conance envers les comportements possibles d'un programme. Les méthodes classiques pour réaliser ces analyses sont l'analyse de modè- les, l'interprétation abstraite et la démonstration automatique de théorèmes. La base d'un démonstrateur automatique de théorèmes est une logique ou une algèbre et le choix de celle-ci a un impact sur la complexité de trouver une preuve pour un théorème donné. Cette dissertation développe un formalisme algébrique concis pouvant être utilisé en démonstration automatique de théorèmes. Ce formalisme est appellé algèbre de Kleene à pile visible. Cette dissertation explique comment ce formalisme peut être utilisé pour réaliser des analyses interprocédurales de programmes, comme des vérications formelles et des vérications d'optimisations efectuées par des compilateurs. Cette dissertation apporte aussi des preuves que ces analyses pourraient être automatisées. L'algèbre de Kleene à pile visible est une extension de l'algèbre de Kleene, un excellent formalisme pour réaliser des analyses intraprocédurales de programmes. En bref, l'algèbre de Kleene est la théorie algébrique des automates nis et des expressions régulières. Donc, cette algèbre à elle seule n'est pas appropriée pour faire des analyses interprocédurales de programmes car la puissance des langages non contextuels est souvent nécessaire pour représenter le lot de contrôle d'un tel programme. L'algèbre de Kleene à pile visible étend celle-ci en lui ajoutant une famille d'opérateurs de plus petit point xe qui est basée sur une restriction des grammaires non contextuelles. En fait, cette algèbre axiomatise exactement la théorie équationnelle des langages à pile visibles. Ces langages sont une sous-classe des langages non contextuels et ont été dénis par Alur et Madhusudan pour faire de l'analyse de modèles. La complexité résultante de la théorie équationnelle de l'algèbre proposée est EXPTIME-complète. / Automatic interprocedural program analyses based on rigorous mathematical theories are complex to do, but they are great tools to increase our condence in the behaviour of a program. Classical ways of doing them is either by model checking, by abstract interpretation or by automated theorem proving. The basis of an automated theorem prover is a logic or an algebra and the choice of this basis will have an impact in the complexity of nding a proof for a given theorem. This dissertation develops a lightweight algebraic formalism for the automated theorem proving approach. This formalism is called visibly pushdown Kleene algebra. This dissertation explains how to do some interprocedural program analyses, like formal veri cation and verication of compiler optimizations, with this formalism. Evidence is provided that the analyses can be automated. The proposed algebraic formalism is an extension of Kleene algebra, a formalism for doing intraprocedural program analyses. In a nutshell, Kleene algebra is the algebraic theory of nite automata and regular expressions. So, Kleene algebra alone is not well suited to do interprocedural program analyses, where the power of context-free languages is often needed to represent the control flow of a program. Visibly pushdown Kleene algebra extends Kleene algebra by adding a family of implicit least xed point operators based on a restriction of context-free grammars. In fact, visibly pushdown Kleene algebra axiomatises exactly the equational theory of visibly pushdown languages. Visibly pushdown languages are a subclass of context-free languages dened by Alur and Madhusudan in the model checking framework to model check interprocedural programs while remaining decidable. The resulting complexity of the equational theory of visibly pushdown Kleene algebra is EXPTIME-complete whereas that of Kleene algebra is PSPACE-complete.

No description available.

No description available.

No description available.

Le développement et la prolifération des réseaux sans fil a contribué à l’évolution de notre quotidien. Toute cette multitude de technologies sans fil existantes permet, malgré sa complexité, d’offrir aux utilisateurs des services diversifiés, voix et données, de la manière la plus convenable, tout en permettant l’ubiquité des services dans une optique ABC (Always Best Connected). Ces réseaux utilisent des technologies différentes, mais en même temps, offrent des caractéristiques complémentaires. Ainsi, ce point s’avère attrayant dans la mesure où nous pourrons bénéficier des avantages de chacune des technologies en les interconnectant toutes afin de former un large réseau hétérogène. La mobilité, ou plus particulièrement la relève, que nous nous proposons d’étudier dans ce mémoire s’impose comme axe de recherche intéressant, et encore plus complexe dans un environnement hétérogène. Dans ce mémoire, deux architectures interconnectant un réseau UMTS et un autre Wimax ont été présentées. Plus précisément, nous avons mis l’emphase sur la procédure de relève verticale lors du passage de l’utilisateur d’un réseau Wimax à un réseau UMTS. Chacune des deux architectures utilise un protocole pour la gestion de la mobilité, en l’occurrence le MIP (Mobile Internet Protocol) et le SIP (Session Initiation Protocol). Afin d’évaluer les deux procédures, nous nous sommes donnés deux indicateurs, notamment le coût de signalisation et la durée de la procédure de relève verticale. Pour ce faire, nous avons spécifié un diagramme d’échanges des messages de signalisation propre à chacun des scénarios, un basé sur le MIP et l’autre basé sur le SIP. Ensuite, nous avons établi des expressions pour chacun des deux indicateurs précédemment cités qui ont été implémentées sous MATLAB. Les résultats démontrent que, généralement, le scénario de relève verticale basé sur le MIP présente une durée et un coût de signalisation moins élevé que celui basé sur le protocole SIP. / The development and proliferation of wireless networks has contributed to the evolution of our daily lives. Mobile users can move between heterogeneous networks, using terminals with multiple access interfaces. Thus, the most important issue in such environment is the Always Best Connected (ABC) concept allowing the best connectivity to applications anywhere at anytime. To answer ABC requirement, various vertical handover decision strategies have been proposed using advanced tools and proven concepts. In this paper, two architectures interconnecting a UMTS network and another Wimax have been presented. Each architecture uses a protocol for mobility management, namely MIP and SIP. To evaluate the two procedures, we are given two indicators, the signaling cost and the vertical handover delay. To evaluate our scenarios, we have established a specified signaling messages flow diagram specific to each scenario, one based on the MIP and the other based on the SIP. Then, we have given expressions for each of the two indicators mentioned above that we have implemented in MATLAB. The results show that, generally, the scenario based on MIP has lower signaling cost and delay than the scenario based on SIP.

Nous avons élaboré un Modèle de l’Apprenant (MA) dans le but de donner des conseils personnalisés en fonction des connaissances de l’apprenant dans le cadre des Environnements Informatiques pour l’Apprentissage Humain (EIAH) à partir d’exemples. Le MA proposé contient cinq catégories de paramètres : les données personnelles, les caractéristiques de l'apprenant, l'état d'apprentissage, les interactions entre l'environnement et l'apprenant et les connaissances de l'apprenant. Notre travail a été effectué à l’aide de la méthode CommonKADS. Un prototype montre notamment sa représentation et l'algorithme de l'évaluation des connaissances de l'apprenant. Une valildation de cette évaluation a permis de vérifier le bon fonctionnement du prototype. Un cadre générique pour modéliser les connaissances de l’apprenant pour un EIAH en général a aussi été développé. Ce modèle pourrait servir d’un guide pour faciliter le développement de MA qui aident à améliorer l’intelligence des EIAH. / We elaborated a Learner Model (LM) that allows the environment to give personalized advices according to a learner’s knowledge. The elaboration is regarding to the learning-by-examples environments. The LM we proposed contains five categories of parameters: personal data, learner’s characteristics, learning state, learner’s interactions with the system, and learner’s knowledge. Our model was designed based on CommonKADS. A prototype demonstrates especially its representation and the algorithm of assessing the learner’s knowledge. A validation on this assessment alowed to verify the good functioning of the prototype. A generic framework for modeling learner’s knowledge in a general learning environment is also developed. The model could serve as a guideline to facilitate developments of LM, which help to improve the intelligence of the environments.

L'objectif de ce mémoire est d'introduire le lecteur à la compression de données générale et sans perte et de présenter deux nouvelles techniques que nous avons développées et implantées afin de contribuer au domaine. La première technique que nous avons développée est le recyclage de bits et elle a pour objectif de réduire la taille des fichiers compressés en profitant du fait que plusieurs techniques de compression de données ont la particularité de pouvoir produire plusieurs fichiers compressés différents à partir d'un même document original. La multiplicité des encodages possibles pour un même fichier compressé cause de la redondance. Nous allons démontrer qu'il est possible d'utiliser cette redondance pour diminuer la taille des fichiers compressés. La deuxième technique que nous avons développée est en fait une méthode qui repose sur l'énumération des sous-chaînes d'un fichier à compresser. La méthode est inspirée de la famille des méthodes PPM (prediction by partial matching). Nous allons montrer comment la méthode fonctionne sur un fichier à compresser et nous allons analyser les résultats que nous avons obtenus empiriquement.

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.