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.

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.

Ce mémoire présente une nouvelle approche pour sécuriser du code potentiellement malicieux à l'aide d'un moniteur incorporé au code. Les premiers chapitres du mémoire introduisent les notions préliminaires à la présentation de l'approche. Plus précisément, les concepts fondamentaux de la vérification de modèle et du contrôle des systèmes à événements discrets. Le dernier chapitre présente les fondements théoriques de l'approche en généralisant les résultats de Ligatti, Bauer et Walker, et montre une classe de moniteurs qui est plus puissante lorsqu'on précise son contexte d'application. Cette observation mène à l'élaboration d'une approche consistant à instrumenter un programme, dans le but de le rendre sécuritaire, à partir d'un modèle du programme et d'une propriété de sécurité représentée par un automate de Rabin.

A wireless sensor network (WSN) consists of a large number of sensor nodes that are capable of detecting many types of information from the environment, including temperature, light, humidity, radiation and seismic vibrations. Current applications of WSNs include: physical security, air traffic control, video surveillance, environment and building monitoring. Such applications require that each sensor node knows its exact location. In this context, the received signal strength indicator (RSSI) is often used for distance measurements between the sensor nodes. This thesis presents a method for the evaluation of the RSSI properties in application to node localization in WSN. More specifically, a WSN application is implemented for collecting RSSI measurement in different conditions. The application consists of two parts: an experiment control script which runs on a computer, and an experiment mote firmware which runs on each WSN node. Statistical analysis of variance (ANOVA) was performed to determine the factors affecting the RSSI measurements. Result analysis shows that: the relation between RSSI values and distances depends on the environment; the used WSN motes are manufactured with enough precision, as the differences between the motes are insignificant; even if the RSSI measurements have significant variation, the mean RSSI values correlate with the distances; using different transmission power levels can provide additional information about the distances.

Les systèmes à événements discrets sont des systèmes dynamiques particuliers. Ils changent d’état de fa¸con discrète et le terme événement est utilisé afin de représenter l’occurrence de changements discontinus. Ces systèmes sont principalement construits par l’homme et on les retrouve surtout dans les secteurs manufacturier, de la circu- lation automobile, des bases de données et des protocoles de communication. Cette thèse s’intéresse au contrôle des systèmes paramétrés à événements discrets où les spécifications sont exprimées à l’aide de prédicats et satisfont une condition de similarité. Des conditions sont données afin de déduire des propriétés, en observation partielle ou totale, pour un système composé de n processus similaires à partir d’un système com- posé de n0 processus, avec n ≥ n0. De plus, il est montré comment inférer des politiques de contrôle en présence de relations d’interconnexion entre les processus. Cette étude est principalement motivée par la faiblesse des méthodes actuelles de synthèse pour le traitement des problèmes industriels de taille réelle. / Discrete event systems are a special type of dynamic systems. The state of these systems changes only at discrete instants of time and the term event is used to represent the occurrence of discontinuous changes. These systems are mostly man-made and arise in the domains of manufacturing systems, traffic systems, database management systems and communication protocols. This thesis investigates the control of parameterized discrete event systems when specifications are given in terms of predicates and satisfy a similarity assumption. For systems consisting of similar processes under total or partial observation, conditions are given to deduce properties of a system of n processes from properties of a system of n0 processes, with n ≥ n0. Furthermore, it is shown how to infer a control policy for the former from the latter’s, while taking into account interconnections between processes. This study is motivated by a weakness in current synthesis methods that do not scale well to huge systems.

Le but de ce mémoire est de présenter une approche orientée objet pour l’élaboration d’un Système de Maintien de Vérité à base de Justifications à Négation et Non Monotone (SMVJNNM). Un SMV est un module utilisé dans les systèmes à base de connaissances pour réviser des croyances. On distingue trois principaux types de SMV: à base de justifications, à base logique et à base d'assomptions. Ils utilisent des structures en réseau pour enregistrer les instances d'un ensemble de règles et tous s'inscrivent dans un paradigme orienté listes. Nous proposons un paradigme objet pour l’élaboration d’un SMV. Les étapes de la démarche suivie sont: étude des SMV existants, modélisation d’un SMV au niveau des connaissances, conception par patrons, implémentation et tests. Deux exemples tirés de la documentation scientifique montrent que notre système offre des fonctionnalités équivalentes à celles des SMV étudiés. Notre système a aussi été utilisé comme mini-moteur de recherche. / The objective of this master’s degree dissertation is to propose an object oriented approach for the design of negated non-monotonic justifications-based truth maintenance systems (NNMJTMS). A truth maintenance system (TMS) is a module assisting knowledge-based systems to conduct belief revision. There are three main types of TMS: justification-based, logical-based and assumption-based. All of these systems use network structures to register instances of a set of production rules according to a list-oriented paradigm. We propose in our work to adopt an object-oriented approach for the design of a TMS. We went through the following steps: review of existing TMS, modeling a TMS at the knowledge level, design and implementation using patterns and testing. To test the TMS in conjunction with a client system, two examples borrowed from scientific literature indicate that our system offers functionalities equivalent to those of the TMS found in the literature. In the first example, we validate some textbook cases. And in the second one, we test the load capacity of the TMS system while assisting a tiny search engine.

Tableau d’honneur de la Faculté des études supérieures et postdoctorales, 2008-2009 / L'augmentation dans les dernières décennies du nombre de véhicules présents sur les routes ne s'est pas passée sans son lot d'impacts négatifs sur la société. Même s'ils ont joué un rôle important dans le développement économique des régions urbaines à travers le monde, les véhicules sont aussi responsables d'impacts négatifs sur les entreprises, car l'inefficacité du ot de traffic cause chaque jour d'importantes pertes en productivité. De plus, la sécurité des passagers est toujours problématique car les accidents de voiture sont encore aujourd'hui parmi les premières causes de blessures et de morts accidentelles dans les pays industrialisés. Ces dernières années, les aspects environnementaux ont aussi pris de plus en plus de place dans l'esprit des consommateurs, qui demandent désormais des véhicules efficaces au niveau énergétique et minimisant leurs impacts sur l'environnement. évidemment, les gouvernements de pays industrialisés ainsi que les manufacturiers de véhicules sont conscients de ces problèmes et tentent de développer des technologies capables de les résoudre. Parmi les travaux de recherche en ce sens, le domaine des Systèmes de Transport Intelligents (STI) a récemment reçu beaucoup d'attention. Ces systèmes proposent d'intégrer des systèmes électroniques avancés dans le développement de solutions intelligentes conçues pour résoudre les problèmes liés au transport automobile cités plus haut. Ce mémoire se penche donc sur un sous-domaine des STI qui étudie la résolution de ces problèmes gr^ace au développement de véhicules intelligents. Plus particulièrement, ce mémoire propose d'utiliser une approche relativement nouvelle de conception de tels systèmes, basée sur l'apprentissage machine. Ce mémoire va donc montrer comment les techniques d'apprentissage par renforcement peuvent être utilisées afin d'obtenir des contrôleurs capables d'effectuer le suivi automatisés de véhicules. Même si ces efforts de développement en sont encore à une étape préliminaire, ce mémoire illustre bien le potentiel de telles approches pour le développement futur de véhicules plus \intelligents". / The impressive growth, in the past decades, of the number of vehicles on the road has not come without its share of negative impacts on society. Even though vehicles play an active role in the economical development of urban regions around the world, they unfortunately also have negative effects on businesses as the poor efficiency of the traffic ow results in important losses in productivity each day. Moreover, numerous concerns have been raised in relation to the safety of passengers, as automotive transportation is still among the first causes of accidental casualties in developed countries. In recent years, environmental issues have also been taking more and more place in the mind of customers, that now demand energy-efficient vehicles that limit the impacts on the environment. Of course, both the governments of industrialized countries and the vehicle manufacturers have been aware of these problems, and have been trying to develop technologies in order to solve these issues. Among these research efforts, the field of Intelligent Transportation Systems (ITS) has been gathering much interest as of late, as it is considered an efficient approach to tackle these problems. ITS propose to integrate advanced electronic systems in the development of intelligent solutions designed to address the current issues of automotive transportation. This thesis focuses on a sub-field ITS since it studies the resolution of these problems through the development of Intelligent Vehicle (IV) systems. In particular, this thesis proposes a relatively novel approach for the design of such systems, based on modern machine learning. More specifically, it shows how reinforcement learning techniques can be used in order to obtain an autonomous vehicle controller for longitudinal vehiclefollowing behavior. Even if these efforts are still at a preliminary stage, this thesis illustrates the potential of using these approaches for future development of \intelligent" vehicles.

Nous abordons dans cette thèse la problématique liée à la modélisation d'environnements urbains virtuels pour des fins de simulation de la mobilité. En premier lieu, nous proposons une nouvelle approche de conception d'un Environnement Urbain Virtuel (EUV) permettant une modélisation multi-échelle grâce à l'utilisation d'un patron de conception qui met en relation les lieux d'activité et les différents réseaux de transport. Dans ce patron, une notion simple de desserte nous permet de modéliser à la fois l'accès à des lieux, le transfert modal et le changement d'échelle. Ce patron peut être spécialisé dans diverses structures à diverses échelles (macro, méso, micro, etc.). Nous formalisons l'EUV en utilisant la théorie des graphes, ce qui permet une implantation rigoureuse de ces concepts, tout en tenant compte des principales fonctions classiquement utilisées pour la simulation des parcours dans les réseaux de transports. En second lieu, nous proposons une démarche pour enrichir l'EUV avec les données de la population qui l'occupe afin d'aboutir à l'Environnement Urbain Peuplé (EUP). Le modèle de l'EUP regroupe alors à la fois la demande et l'offre en transports. Notre démarche réduit le problème en deux sous-problèmes semblables mais qui se traitent différemment: 1) l'allocation des attributs non spatiaux (donc la génération de la population synthétique) en combinant une approche de reconstruction synthétique avec un algorithme d'apprentissage non supervisé et 2) l'allocation des attributs spatiaux (donc l'assignation des lieux d'occupation) en combinant une approche de prédiction des temps de parcours (avec l'utilisation potentielle d'un algorithme d'apprentissage supervisé) avec un algorithme d'appariement dans un graphe biparti et pondéré. Au niveau de la validation, en plus des méthodes statistiques qui existent pour mesurer la vraisemblance d'une population synthétique, nous proposons une série de validations unitaires devant se faire au moment même de la création de l'EUP. Nous présentons TransNetSim, la plateforme de simulation multi-agent des déplacements que nous avons développée et qui tire partie de tous les avantages de notre modèle de l'EUP. En comparant TransNetSim par rapport à des outils existants, nous montrons qu'il regroupe un ensemble de caractéristiques qui font de lui un prototype prometteur. Particulièrement, le principe de la matrice de routage dans laquelle on compile tous les chemins optimaux en prétraitement offre un grand apport au niveau de la faisabilité computationnelle de l'approche multi-échelle. L'utilisation de la plateforme a été illustrée par la simulation du trafic de véhicules dans la ville de Québec à une échelle méso et dans le campus universitaire à une échelle micro. Finalement, nous montrons comment l'utilisation d'outils SOLAP permet d'une façon simple et efficace d'analyser et de calibrer les résultats de nos simulations (génération de la population synthétique, données résultant de la simulation du trafic).

Peu de modèles et de simulations qui décrivent les comportements de foule en situations de conflit impliquant des forces de l’ordre et des armes non-létales (NLW) existent. Ce mémoire présente des modèles d’agents de la foule et des forces de l’ordre ainsi que des NLWs dans des situations de conflit. Des groupes ainsi que leurs interactions et actions collectives sont explicitement modélisés, ce qui repousse les approches de simulation de foule existantes. Les agents sont caractérisés par des profils d’appréciation de l’agressivité et ils peuvent changer leurs comportements en relation avec la Théorie de l’identité sociale. Un logiciel a été développé et les modèles ont été calibrés avec des scénarios réalistes. Il a démontré la faisabilité technique de modèles sociaux aussi complexes pour des foules de centaines d’agents, en plus de générer des données pour évaluer l’efficacité des techniques d’intervention. / Few models and simulations that describe crowd behaviour in conflict situations involving control forces and non-lethal weapons (NLW) exist. This thesis presents models for crowd agents, control forces, and NLWs in crowd control situations. Groups as well as their interactions and collective actions are explicitly modelled, which pushes further currently existing crowd simulation approaches. Agents are characterized by appreciation of aggressiveness profiles and they can change their behaviours in relation with the Social Identity theory. A software application was developed and the models were calibrated with realistic scenarios. It demonstrated the technical feasibility of such complex social models for crowds of hundreds of agents, as well generating data to assess the efficiency of intervention techniques.

Les protocoles cryptographiques constituent la base de la sécurité des communications faites le long du réseau Internet et des systèmes distribués. Cependant, une faille à l'intérieur d'un protocole peut entraîner des conséquences indésirables et souvent irréversibles autant pour les individus que pour les entreprises. Dans le but de prévenir ces failles, les méthodes formelles se sont imposées comme un choix incontournable pour spécifier et analyser les protocoles cryptographiques. La première tentative d'utilisation des méthodes formelles fût, vu la subtilité du problème, une simple exploration d'un sous ensemble fini des exécutions possibles du protocole analysé, et ce pour dévoiler quelques-unes de ses failles. Cependant, bien que cette technique ait réussi à découvrir plusieurs failles dans de nombreux protocoles, elle reste incapable d'affirmer la correction d'un protocole en absence de la détection d'une faille. De ce fait, les recherches ont été orientées, depuis très récemment, vers la proposition de méthodes formelles permettant de garantir la correction des protocoles cryptographiques par rapport à certaines propriétés de sécurité. Dans cette thèse, nous nous intéressons à ce type de méthodes et nous ramenons les contributions suivantes : L'introduction de la notion de contexte de vérification qui regroupe toutes les hypothèses et les conditions (les capacités de l'intrus, l'algèbre de messages, etc.) faites lors de l'analyse d'un protocole. Cette notion nous a permis d'établir des résultats généraux qui ne dépendent pas d'un contexte de vérification particulier. La proposition de conditions suffisantes permettant de garantir la correction des protocoles cryptographiques par rapport à la propriété de confidentialité. Ces conditions consistent à vérifier si un protocole est croissant par rapport à une fonction spéciale appelée fonction d'interprétation. La proposition d'un guide qui permet la définition des fonctions d'interprétation d'une manière méthodique. L'extension des résultats précédents pour tenir compte des propriétés algébriques des primitives cryptographiques. La mise en oeuvre des résultats précédents pour l'analyse de certains protocoles utilisés dans la vie courante comme Kerberos, SET et NSL, et ce, en présence de la propriété d'homomorphisme de l'opérateur l'encryption.