Dans ce mémoire nous nous intéressons à une branche de la vérification qui consiste à comparer une spécification (fonctionnement idéal) à son implémentation (système réel). Tous les deux sont sous forme de systèmes probabilistes, c’est-à-dire des systèmes dont le comportement est incertain mais quantifié par des distributions de probabilité. Il y a plusieurs méthodes disponibles pour comparer les systèmes : la bisimulation, la simulation, l’équivalence de traces, ou bien les distances qui s’adaptent au comportement probabiliste auquel nous nous intéressons. En effet, plutôt que de dire si oui ou non les deux systèmes à comparer sont « équivalents » une distance nous donne une valeur qui quantifie leur différence. Si la distance est 0 les deux systèmes sont équivalents. Il y a plusieurs notions de distances pour les systèmes probabilistes, le but de ce mémoire est de comparer trois d’entre elles : -distance, K-moment et Desharnais et al. Le principal résultat de cette comparaison est que les trois méthodes ont des résultats qui ne sont pas fondamentalement différents, bien qu’elles soient conçues de façon difficilement comparable. Il arrive souvent que les distances se suivent. Les principales différences se manifestent dans le temps de calcul, la capacité de traitement et l’atténuation du futur. Nous démontrons que les performances de chaque distance varient selon le type de système traité. Cela signifie que pour choisir la meilleure méthode, il faut déterminer le type de système que nous avons. En prenant par exemple un système dont nous n’avons pas le modèle, c’est la famille K-moment qui sera la seule capable de calculer une distance. Par ailleurs, nous avons pu intégrer dans la -distance un facteur qui atténue les différences les plus lointaines par rapport à celles plus proches. Cela nous a amené à définir une nouvelle distance : -distance atténuée.

La Sécurité des Systèmes d'Information est l'un des défis les plus urgents des différents organismes de la société actuelle. Le problème de sécurité a émergé du progrès technologique rapide qui pousse à l'utilisation des \emph{Systèmes d'Information}. L'un de ces progrès est l'utilisation de code mobile. En effet, pour protéger ses informations critiques d'une éventuelle menace d'un code mobile, un organisme doit chercher des solutions de plus en plus élaborées. Une des approches émergeantes pour aborder ce problème est la compilation certifiée. Il s'agit d'une approche statique, basée sur le langage et génère en plus du code objet, un certificat constitué des informations relatives aux aspects de sécurité d'un programme. En plus des avantages de l'analyse statique, cette approche fait coopérer le producteur du code et son consommateur. De plus, ce dernier n'a plus à faire confiance au producteur. Dans cette thèse nous avons appliqué cette approche au langage Java afin de vérifier statiquement la sécurité. En effet, Java couvre une gamme de périphériques, d'ordinateurs et de réseaux grâce à son évolutivité, son efficacité, sa portabilité et sa sécurité. Toutefois, les propriétés de sécurité de haut niveau sont vérifiées dynamiquement dans Java par le vérificateur du \emph{bytecode} et le gestionnaire de sécurité. Nous proposons alors de concevoir et d'implanter un compilateur certificateur pour Java (JACC) afin d'accroître la flexibilité, l'efficacité et la robustesse de l'architecture de sécurité de Java. Le certificat que génère JACC est vérifié statiquement par le vérificateur de l'architecture JACC. Il est constitué d'annotations qui essaient de reporter et abstraire au mieux le comportement du programme. Les principaux résultats qui nous ont permis d'atteindre ces objectifs sont: \begin{enumerate} \item la définition de la syntaxe et sémantique des annotations du certificat; \item la conception et l'implantation de JACC en partant de Jikes, un compilateur pour le langage Java développé par IBM. Nous avons également pu mener une étude expérimentale pour mesurer la performance de JACC ainsi que la taille des fichiers \emph{.class} générés et nous les avons comparés à Jikes; \item l'élaboration d'un cadre formel pour spécifier le module d'inférence. Cette spécifi\-cation décrit la sémantique opérationnelle de chaque étape d'inférence et ce pour l'ensemble des \emph{opcodes} ainsi qu'un système de types pour les annotations du certificat. \end{enumerate} / Information Systems Security is one of the most pressing challenges facing all kind of organizations today. The security problem has raised from rapid technological advances that are stimulating a greater use of \emph{Information Systems} in world-wide organizations. One of these advances is the use of mobile code. Keeping critical information safe from malicious mobile code is challenging. One way to address the security issue for mobile code is using certifying compilation. The certifying compilation is a language-based, static technique used to collect information (certificate) regarding the safety and security of a software. In addition to the advantages of the static analysis, this approach alleviates the burden on the consumer. The other advantage of this approach is to restrict the trust of the consumer to the verifier only. In this thesis we have applied this approach to Java to check safety and security statically. As we know, Java is present in a wide range of devices, computers, and networks due to it's versatility, efficiency, platform portability and security . Nevertheless, high-level security properties are verified by bytecode verifier and security manager at run time. The main objectives of this thesis are the design and the implementation of a Java certifying compiler (JACC) that helps to increase the flexibility, efficiency and robustness of the Java security architecture. Indeed, JACC certificate is verified statically by the JACC verifier to ensure high-level security properties. The certificate is made up of annotations that try to capture the behavior of a software and represent it in an abstract form. This behavior could be critical and aims to threaten the software user. The main research contributions that led to reach these objectives are: \begin{enumerate} \item the definition of the certificate syntax and semantic; \item the design and the implementation of JACC based on Jikes. We have also measured the generated \emph{.class} files sizes and JACC performance and compared them to Jikes; \item the elaboration of a formal framework in which we formally specify the certificate inference. This specification describes the operational semantic of each inference step as long as a type system for the certificate annotations. \end{enumerate}

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2011-2012 / Dans ce mémoire, nous comparons deux modèles de processus probabilistes évoluant dans un environnement continu. Les processus de Markov étiquetés sont des systèmes de transitions pour lesquels l’ensemble des états est non-dénombrable, mais qui évoluent de manière discrète dans le temps. Les mesures de probabilité définies sur l’ensemble des états peuvent avoir un support infini. Les processus hybrides sont une combinaison d’un processus à espace d’états continu qui évolue de manière continue dans le temps et une composante discrète qui intervient pour contrôler l’évolution. Les extensions probabilistes des processus hybrides présentes dans la littérature restreignent le comportement probabiliste à la composante discrète. Nous utilisons deux exemples de systèmes, un avion et un bateau, pour faire ressortir les divergences entre les deux modèles ainsi que leurs limitations, et nous définissons une généralisation qui peut modéliser fidèlement ces exemples. Nous avons également pu montrer, dans un article publié dans un atelier international, comment utiliser, dans le contexte probabiliste, la «substitution d’horloge» et l’«approximation par portrait» qui sont des techniques proposées par Henzinger et al. pour les processus non probabilistes. Ces techniques permettent, sous certaines conditions, de définir un processus probabiliste rectangulaire à partir d’un qui est non rectangulaire, rendant ainsi possible la vérification formelle de toute classe de système hybride probabiliste. / We compare two models of processes involving uncountable space. Labelled Markov processes are probabilistic transition systems that can have uncountably many states, but still make discrete time steps. The probability measures on the state space may have uncountable support and a tool has been developed for verification of such systems. Hybrid processes are a combination of a continuous space process that evolves continuously with time and of a discrete component, such as a controller. Existing extensions of Hybrid processes with probability restrict the probabilistic behavior to the discrete component. We have also shown, in a paper, how to compute for probabilistic hybrid systems, the clock approximation and linear phase-portrait approximation that have been proposed for non probabilistic processes by Henzinger et al. The techniques permit, under some conditions, to define a rectangular probabilistic process from a non rectangular one, hence allowing the model-checking of any class of systems. To highlight the differences between Labelled Markov processes and probabilistic hybrid systems, we use two examples, the ones of a boat and an aircraft, and

Ce mémoire porte sur le problème de décision CSP (de l'anglais Constraint Satisfaction Problem, c'est-à-dire problème de satisfaction de contraintes), soit le problème pour lequel nous devons assigner des valeurs à des variables de telle sorte que toutes les conditions portant sur ces variables soient remplies. De surcroît, ce mémoire porte sur les problèmes de détection d'homomorphisme entre structures relationelles qui sont équivalents à CSP. Pour être plus précis, nous nous intéressons à l'algorithme de cohérence d'arc pour les instances de CSP, soit ArcjConsistency. Celui-ci suffit à solutionner un certain sous-ensemble de CSP. Or nous étudions quelques-unes de ses variantes qui sont des algorithmes plus coûteux, mais plus puissants, c'est-à-dire que le sous-ensemble de CSP qu'ils solutionnent est plus grand. La nouveauté de ce mémoire est de décrire et d'étudier une variante de ArcjConsistency, soit NLjCohérence, qui est un algorithme moins puissant mais plus efficace. L'objectif pour nous est de trouver des caractéristiques intéressantes au sujet de ce nouvel algorithme, qui se veut être une version « espace logarithmique » de ArcjConsistency. De plus, nous travaillons sur un sous-ensemble de CSP dit implicatif. Nous démontrons que NL_Cohérence solutionne les instances de ce sous-ensemble en espace logarithmique non-déterministe.

Les systèmes informatiques occupent une place grandissante dans notre société actuelle hautement informatisée. À mesure que les systèmes transactionnels traditionnels sont informatisés, une composante de confidentialité vient s'ajouter aux systèmes informatiques. Ces systèmes gagnant en complexité, la vérification manuelle par des êtres humains devient rapidement impraticable. Nous présentons des methods traditionnelles de verification automatique de la conformité d'un programme à une propriété de sécurité. Ensuite, nous présentons une approche originale de Hugues Chabot et al. utilisant des omega-automates, qui permettent de verifier des programmes pour lesquels une execution peut ne jamais se terminer. Nous proposons quelques optimisations puis procédons a son implantation pour en mesurer la performance. Nous présentons finalement une approche alternative, base sur la théorie des transactions logicielles, qui permet de corriger un programme deviant plutôt que de le rejetter. Nous terminons en posant un regrard critique sur le travail accompli.

Les problèmes de satisfaction de contraintes sont parmi les problèmes fréquents qu'on trouve dans des domaines variés tels que la recherche opérationnelle et l'intelligence artificielle. Dans un problème de satisfaction de contraintes, on cherche à assigner aux variables des valeurs de telle sorte que toutes les contraintes fournies en entrée soient satisfaites. Chaque contrainte est une paire contenant un tuple de variables et une relation définissant les combinaisons de valeurs autorisées pour ce tuple. Ce problème est NP-complet, donc il est important d'identifier des cas particuliers résolubles en temps polynomial. Dans ce travail, on s'intéresse à une approche dite algébrique pour découvrir des classes de problèmes de satisfaction de contraintes traitables efficacement. On se base sur le résultat prouvé par Dalmau "en 2006" qui donne un algorithme polynomial pour une classe assez vaste de problèmes. On analyse et implémente un cas particulier de cet algorithme qui permet de résoudre des instances de 2-SAT. Cette implementation nous aidera à faire des expérimentations et à en apprendre plus sur la nature de l'algorithme de Dalmau et son comportement en pratique.

Estimer la pose de la caméra est un défi fondamental en réalité augmentée et permet la superposition d’un modèle à la réalité. Estimer précisément la pose est souvent critique en ingénierie d’infrastructures. Les images omnidirectionnelles ont un champ de vision supérieur aux images planaires communément utilisées en RA. Cette propriété peut bénéficier à l’estimation de la pose. Or, aucun travail ne présente de résultats montrant clairement un gain de précision. Notre objectif est de quantifier la précision de l’estimation de pose omnidirectionnelle et la tester en pratique. Nous proposons une méthode d’estimation de pose pour images omnidirectionnelles et en avons mesuré la précision par des simulations automatisées. Les résultats obtenus confirment que le champ de vision large des images omnidirectionnelles permet d’atteindre une précision de pose supérieure à celle d’images planaires. Nous avons également testé notre méthode sur des données tirées d’environnements réels et discutons les défis et limitations à son utilisation en pratique. / Camera pose estimation is a fundamental problem of augmented reality, and enables registration of a model to the reality. An accurate estimate of the pose is often critical in infrastructure engineering. Omnidirectional images cover a larger field of view than planar images commonly used in AR. This property can be beneficial to pose estimation. However, no existing work present results clearly showing accuracy gains. Our objective is therefore to quantify the accuracy of omnidirectional pose estimation and test it in practice. We propose a pose estimation method for omnidirectional images and have measured its accuracy using automated simulations. Our results show that the large field of view of omnidirectional images increases pose accuracy, compared to poses from planar images. We also tested our method in practice, using data from real environments and discuss challenges and limitations to its use in practice.

Dans le domaine de la classification, les algorithmes d'apprentissage par compression d'échantillons sont des algorithmes qui utilisent les données d'apprentissage disponibles pour construire l'ensemble de classificateurs possibles. Si les données appartiennent seulement à un petit sous-espace de l'espace de toutes les données «possibles», ces algorithmes possédent l'intéressante capacité de ne considérer que les classificateurs qui permettent de distinguer les exemples qui appartiennent à notre domaine d'intérêt. Ceci contraste avec d'autres algorithmes qui doivent considérer l'ensemble des classificateurs avant d'examiner les données d'entraînement. La machine à vecteurs de support (le SVM) est un algorithme d'apprentissage très performant qui peut être considéré comme un algorithme d'apprentissage par compression d'échantillons. Malgré son succès, le SVM est actuellement limité par le fait que sa fonction de similarité doit être un noyau symétrique semi-défini positif. Cette limitation rend le SVM difficilement applicable au cas où on désire utiliser une mesure de similarité quelconque. / In classification, sample compression algorithms are the algorithms that make use of the available training data to construct the set of possible predictors. If the data belongs to only a small subspace of the space of all "possible" data, such algorithms have the interesting ability of considering only the predictors that distinguish examples in our areas of interest. This is in contrast with non sample compressed algorithms which have to consider the set of predictors before seeing the training data. The Support Vector Machine (SVM) is a very successful learning algorithm that can be considered as a sample-compression learning algorithm. Despite its success, the SVM is currently limited by the fact that its similarity function must be a symmetric positive semi-definite kernel. This limitation by design makes SVM hardly applicable for the cases where one would like to be able to use any similarity measure of input example. PAC-Bayesian theory has been shown to be a good starting point for designing learning algorithms. In this thesis, we propose a PAC-Bayes sample-compression approach to kernel methods that can accommodate any bounded similarity function. We show that the support vector classifier is actually a particular case of sample-compressed classifiers known as majority votes of sample-compressed classifiers. We propose two different groups of PAC-Bayesian risk bounds for majority votes of sample-compressed classifiers. The first group of proposed bounds depends on the KL divergence between the prior and the posterior over the set of sample-compressed classifiers. The second group of proposed bounds has the unusual property of having no KL divergence when the posterior is aligned with the prior in some precise way that we define later in this thesis. Finally, for each bound, we provide a new learning algorithm that consists of finding the predictor that minimizes the bound. The computation times of these algorithms are comparable with algorithms like the SVM. We also empirically show that the proposed algorithms are very competitive with the SVM.

Le déploiement des réseaux de senseurs sans fil (WSN : Wireless Sensor Network) soulève un certain nombre de défis liés à la configuration des senseurs, la gestion des ressources et à l'implémentation d'applications. Les travaux récents ont montré la nécessité d'utiliser ces réseaux pour la détection des incendies. Toutefois, pour signaler la présence de ces derniers, il faut s'assurer de mesurer les bons indices, tels que la température, l'humidité et l'intensité lumineuse. Ce mémoire présente la mise en place d'un WSN capable de recueillir et de traiter des informations provenant de l'environnement, comme la température. Dans ce contexte, nous caractérisons d'abord les applications des WSNs. Ensuite, nous identifions les principaux paramètres sur lesquels se basent les applications des WSNs pour détecter les incendies. Finalement, afin d'évaluer l'impact du vent sur les températures recueillies, nous présentons les différentes étapes de la mise en {\oe}uvre d'un WSN pour la détection d'un incendie, ainsi que les expériences réalisées et les résultats obtenus. L'analyse des résultats montre que la vitesse et la direction du vent ont un impact important sur les températures recueillies par le WSN. Il est donc important d'en tenir compte pour pouvoir détecter à temps un incendie. / The deployment of wireless sensor networks (WSN: Wireless Sensor Network) raises a number of challenges related to the configuration of sensors, resource management and implementation of applications. Recent researches proved the necessary use of these networks to detect fires. However, to indicate their presence, make sure to measure the right indicators, such as temperature, humidity and light intensity. This report presents the setting of a WSN that can collect and process information from the environment such as temperature. In this context, we characterize the first; applications of WSNs. Then we identify the main parameters on which the applications of WSNs are based to detect fires. Finally, to assess the impact of wind on temperature gathered, we present the different stages of the setting of a WSN for detecting a fire, including the experiences and results. Analysis of the results shows that the speed of wind and its direction have both a significant impact on temperatures collected by the WSN. It is therefore important to take in account the wind for detecting fire in time.

De nos jours, le développement des personnages de jeux est devenu une tâche dif- ficile en raison de la complexité toujours grandissante des jeux vidéos actuels. Pour diminuer la complexité liée au développement de ces personnages, certaines approches sont applicables et consistent à utiliser des techniques d'intelligence artificielle. Dans ce travail, nous proposons d'utiliser des diagrammes états-transitions pour activer un personnage de jeu vidéo. Nous étudions les moyens de construire des diagrammes états-transitions et plus spécifiquement comment les structurer à partir des séquences de jeux. Les performances des diagrammes construits sont évaluées et nous analysons les possibilités d'améliorer les rendements obtenus. Dans nos expérimentations, nous utilisons le jeu de poursuite dénommé Pacman. Pacman constitue un banc d'essai idéal car il présente un environnement dynamique et séquentiel et nécessite une prise de décision en temps réel. Dans ce travail nous tentons d'accomplir les tâches suivantes : Acquérir des séquences de jeux à travers l'utilisation de l'apprentissage par la démonstration. Structurer des diagrammes états-transitions à partir des séquences de jeux. Analyser la possibilité d'améliorer les performances des diagrammes états-transitions par l'utilisation des techniques de raisonnement à base de cas et des éléments de la théorie de l'information. / Nowadays, developing game characters has become a difficult task because of the increasing complexity of actual video games. To reduce the complexity of developing those characters, some approaches exist and consist of using artificial intelligence techniques. In this project, we propose using state machines to activate a video game character. We learn the means to build state machines and more specifically how to structure them from game sequences. The performance of those state machines is evaluated and we analyze the possibility of improving the results. In our experimentations, we use the pursuit game called Pacman. Pacman constitute an ideal testbed because it others a dynamic and sequential environment and it calls for real time decision making. In this work we are trying to accomplish the following tasks : Acquire game sequences through usage of learning from demonstration. Structure the state machines from game sequences. Analyze the possibility of improving the performances of the state machines by using case-based reasoning techniques and elements of information theory.