Most of our daily activities are carried out over the Internet, from file-sharing and social networking to home banking, online-teaching and online-blogging. Considering file-sharing as one of Internet top activities, different architectures have been proposed, designed and implemented, leading to a wide set of file-sharing networks with different performances and goals. This digital society enables as well users' profiling. As Internet users surf the World Wide Web, every sent or received packet passes through several intermediate nodes until they reach their intended destination. So, an observer will be able to determine where a packet comes from and where it goes to, to monitor and to profile users' online activities by identifying to which server they are connected or how long their sessions last. Meanwhile, anonymous communications have been significantly developed to allow users to carry out their online activities without necessarily revealing their real identity. Our contribution is twofold. On the one hand, we consider hybrid file-sharing environments, with a special focus on widely deployed real-world networks and targeting two defined goals. The first goal is to improve content indexation in the BitTorrent file-sharing environment, enabling BitTorrent content to be indexed in the Kad distributed has table and leading to a more robust BitTorrent system. The second goal is to improve content availability in the I2P file-sharing environment. We allow I2P users to anonymously access public BitTorrent content and we obtain a fully anonymous file-sharing environment, including anonymous content indexation and anonymous content distribution. On the other hand, we focus on the understanding of anonymous environments through extensive monitoring. We characterise the I2P network, targeting the entire anonymous environment and its anonymous services. We consider different aspects of the network, such as the number of users, their characteristics as well as the number of anonymous services available. Through long-term measurements on the network and along with different correlation analyses, we are able to characterise a small group of users using a specific anonymous service, such as the users from a particular city performing anonymous file-sharing.

Les applications des réseaux sociaux (OSN) permettent aux utilisateurs de toutes les âges de partager facilement une large série des contenus confidentiels ou privés avec un nombre théoriquement illimité de partenaires. Cet avantage peut être obtenu au risque des problèmes de sécurité et de l'exposition de la vie privée pour les utilisateurs, puisque dans toutes les OSN existantes, afin de soutenir un modèle d'affaires prometteur, les informations des utilisateurs sont collectées et stockées de façon permanente par le fournisseur de service, qui devient potentiellement un "Big Brother" capable d'exploiter ces informations de plusieurs façons qui peuvent violer la vie privée des utilisateurs individuels ou groupes d'utilisateurs. La thèse propose et valide une nouvelle approche pour ces problèmes de sécurité et de confidentialité. Afin d'assurer la confidentialité des utilisateurs face à les violations potentiels de la vie privée par le fournisseur, ce modèle adopte une architecture distribuée en s'appuyant sur la coopération entre un certain nombre de parties indépendantes qui sont aussi les utilisateurs de l'application de réseau social. Le deuxième point fort de l'approche suggérée est de s'appuyer sur les relations de confiance qui font partie des réseaux sociaux dans la vie réelle afin d'affronter le problème de la création de mécanismes de confiance en préservant la vie privée. Sur la base de ces principes de conception, un nouveau réseau social en ligne distribuée, appelé Safebook, a été proposé: Safebook s'appuie sur la confiance dans la vie réelle et permet aux utilisateurs de maintenir le contrôle sur l'accès et l'utilisation de leurs propres informations.

The scalability of multithreaded applications on current multicore systems is hampered by the performance of lock algorithms, due to the costs of access contention and cache misses. The main contribution presented in this thesis is a new lock algorithm, Remote Core Locking (RCL), that aims to improve the performance of critical sections in legacy applications on multicore architectures. The idea of RCL is to replace lock acquisitions by optimized remote procedure calls to a dedicated hardware thread, which is referred to as the server. RCL limits the performance collapse observed with other lock algorithms when many threads try to acquire a lock concurrently and removes the need to transfer lock-protected shared data to the hardware thread acquiring the lock because such data can typically remain in the server's cache. Other contributions presented in this thesis include a profiler that identifies the locks that are the bottlenecks in multithreaded applications and that can thus benefit from RCL, and a reengineering tool developed with Julia Lawall that transforms POSIX locks into RCL locks. Eighteen applications were used to evaluate RCL: the nine applications of the SPLASH-2 benchmark suite, the seven applications of the Phoenix 2 benchmark suite, Memcached, and Berkeley DB with a TPC-C client. Eight of these applications are unable to scale because of locks and benefit from RCL on an x86 machine with four AMD Opteron processors and 48 hardware threads. Using RCL locks, performance is improved by up to 2.5 times with respect to POSIX locks on Memcached, and up to 11.6 times with respect to Berkeley DB with the TPC-C client. On an SPARC machine with two Sun Ultrasparc T2+ processors and 128 hardware threads, three applications benefit from RCL. In particular, performance is improved by up to 1.3 times with respect to POSIX locks on Memcached, and up to 7.9 times with respect to Berkeley DB with the TPC-C client.

Automated planning is a field of artificial intelligence that aims at proposing methods to chose and order sets of actions with the objective of reaching a given goal. A sequence of actions solving a planning problem is usually called a plan. In many cases, one does not only have to find a plan but an optimal one. This notion of optimality can be defined by assigning costs to actions. An optimal plan is then a plan minimizing the sum of the costs of its actions. Planning problems are standardly solved using algorithms such as A* that search for minimum cost paths in graphs. In this thesis we focus on a particular approach to planning called factored planning or modular planning. The idea is to consider a decomposition of a planning problem into almost independent sub-problems (or components). One then searches for plans into each component and try to assemble these local plans into a global plan for the original planning problem. The main interest of this approach is that, for some classes of planning problems, the components considered can be planning problems much simpler to solve than the original one. First, we present a study of the use of some message passing algorithms for factored planning. In this case the components of a problem are represented by weighted automata. This allows to handle all plans of a sub-problems, and permits to perform factored cost-optimal planning. Achieving cost-optimality of plans was not possible with previous factored planning methods. This approach is then extended by using approximate resolution techniques ("turbo" algorithms) and by proposing another representation of components for handling actions which read-only in some components. Then we describe another approach to factored planning: a distributed version of the famous A* algorithm. Each component is managed by an agent which is responsible for finding a local plan in it. For that, she uses information about her own component, but also information about the rest of the problem, transmitted by the other agents. The main difference between this approach and the previous one is that it is not only modular but also distributed.

This work focuses on the study of concurrent and timed games. These two classes of games have been useful models in controller synthesis. In situations where several agents interact, the notion of winning strategies used so far is not adapted and it is necessary to adopt concepts from game theory. The main concept considered in this area is that of Nash equilibrium. For concurrent games, we propose a transformation which draw a parallel between equilibria and winning strategies. Many works have focused on the computation of winning strategies and we can take advantage of the available algorithms. To compute equilibria in timed games we show that it is possible to reduce them to concurrent games. We propose algorithms for the computation of equilibria, first with classical objectives. Then, we propose a more general framework, in which more quantitative preferences can be described. We also study the theoretical complexity of the associated decision problems. Finally, we present a tool that implements one of the algorithms that we developed.

Trees are said to be unordered if the order between successor nodes of a given node is not important. Unranked trees are trees which do not have a priori bound on the number of successors of each node of the tree. Unranked and unordered trees are a possible model for semistructured data. The advantage of this model is that it is less dependant on the representation of semistructured data as XML documents, and the drowback is that formalisms (tree automata, logics) for manipulating this kind of trees are generally related with worse complexity results compared with similar formalisms for unranked and ordered trees. Our aim is a theoretical study of some logics for unranked and unordered trees, espetially from the point of view of using it as query languages for semistructured data. Thus, we are interested in the model checking problem and its complexity, in the satisfiability problem and in caracterising the expressive power of these logics. The model checking problem is, given a tree and a logic formula, to decide whether the trees satisfies the formula; model checking is the mecanism used for query evaluation. The satisfiability problem is, given a logic formula, to decide whether this formula admits some models; satisfiability can be used for query optimisation. Finally, caracterisation of the expressive power of a logic is a caracterisation of the kind of properties it can express. We start from a spatial logic which has been introduced as the basis of a query language for semistructured data. This logic is quite expressive and has several kinds of operators. We consider different fragments of this logic. We identify several interesting fragments of the logic for which the satisfiability problem is decidable, when this problem is known to be undecidable for other fragments. We compare fragments of the logic with monadic second order logic on trees and extensions of it. Finally, studying the model checking problem and its complexity allowed us to propose a model checking algorithm and to establish several results on theoretic complexity of model checking for several fragments of the spatial logic.

Les systèmes embarqués temps réel nécessitent une analyse temporelle pour valider leur comportement temporel.Afin de réduire le coût de développement, l'analyse doit être effectuée à une phase précoce au moment de la modélisationpour détecter les anomalies de conception. L'analyse d'ordonnançabilité est une des analyses temporelles qui permettentde s'assurer du bon fonctionnement du système conçu. Elle est issue de la théorie de l'ordonnancement temps réel.Plusieurs méthodes et tests analytiques ont été proposés par la communauté académique mais peu sont les tests adoptéspar les industriels. En effet, l'utilisation des tests d'analyse exige une large connaissance des travaux de recherches - misà jour régulièrement - afin de choisir la méthode la plus adaptée aux systèmes conçus pour les valider ou les dimensionnerpour le cas des systèmes qui sont en cours de conception.Cette thèse s'intéresse à cette utilisation minimaliste de la théorie de l'ordonnancement dans l'industrie, et propose dessolutions d'aide à la décision basées sur l'ingénierie dirigée par les modèles. Nos solutions visent à augmenter l'applicabilitéde la théorie de l'ordonnancement, à faciliter le choix des tests appropriés et à réduire le surdimensionnement qui peutêtre généré au moment de la conception. Ces solutions sont implémentées dans un Framework appelé MoSaRT offrantdes fonctionnalités pour les concepteurs (modeleurs et analystes) afin d'améliorer le processus de conception des systèmestemps réel en vue de leur ordonnançabilité.

This thesis studies logics which express properties on programs. These logics were originally intended for the formal verification of programs with pointers. Overall, no automated verification method will be proved tractable here- rather, we give a new insight on separation logic. The complexity and decidability of some essential fragments of this logic for Hoare triples were not known before this work. Also, its combination with some other verification methods was little studied. Firstly, in this work we isolate the operator of separation logic which makes it undecidable. We describe the expressive power of this logic, comparing it to second-order logics. Secondly, we try to extend decidable subsets of separation logic with a temporal logic, and with the ability to describe data. This allows us to give boundaries to the use of separation logic. In particular, we give boundaries to the creation of decidable logics using this logic combined with a temporal logic or with the ability to describe data.

Se basant sur les avancées techniques et scientifiques dans les domaines des systèmes d'information géographique et des indicateurs sociaux et environnementaux, l'objectif de cette thèse est de contribuer au développement d'un outil informatique d'aide à l'identification et à l'évaluation de variantes de tracés routiers. Le rôle du bureau d'étude en aménagement dans la conduite des projets routiers, ses besoins en matière de développement d'outil et les méthodes d'évaluation préexistantes sont d'abord présentés. On étudie ensuite les possibilités d'automatisation du traitement des données géographiques de l'aire d'étude d'un projet, permettant de faire ressortir les zones les plus propices à l'insertion de tronçons routiers (sur la base des fonctionnalités du logiciel ArcGIS). Afin d'améliorer et approfondir l'évaluation des variantes et d'aider à la sélection entre tracés, des indicateurs nouveaux relatifs aux effets globaux et locaux des tronçons routiers, sont proposés. Ils concernent les impacts environnementaux de type d'analyse de cycle de vie, la fragmentation des écosystèmes, la sécurité des transports, le patrimoine, les nuisances sonores, la co-visibilité et le rayonnement. Leur applicabilité et leur pertinence sont testées dans la comparaison de variantes d'un projet réel. Afin de répondre aux besoins du processus de concertation, une méthode interactive de combinaison des indicateurs est proposée. Enfin, les potentialités de développement de ces fonctions sous forme d'outil opérationnel pour le bureau d'étude, sont discutées.

In this thesis, we are interested in designing schedulers for hybrid systems. We consider two specific subclasses of hybrid systems, real-time systems where tasks are competing for the access to common resources, and sampled switched systems where a choice has to be made on dynamics of the system to reach goals. Scheduling consists in defining the order in which the tasks will be run on the processors in order to complete all the tasks before a given deadline. In the first part of this thesis, we are interested in the scheduling of periodic tasks on multiprocessor architectures. We are especially interested in the robustness of schedulers, i.e., to prove that some values of the system parameters can be modified, and until what value they can be extended while preserving the scheduling order and meeting the deadlines. The Inverse Method can be used to prove the robustness of parametric timed systems. In this thesis, we introduce a state space reduction technique which allows us to treat challenging case studies such as one provided by Astrium EADS for the launcher Ariane 6. We also present how an extension of the Inverse Method, the Behavioral Cartography, can solve the problem of schedulability, i.e., finding the area in the parametric space in which there exists a scheduler that satisfies all the deadlines. We compare this approach to an analytic method to illustrate the interest of our approach In the second part of this thesis, we are interested in the control of affine switched systems. These systems are governed by a finite family of affine differential equations. At each time step, a controller can choose which dynamics will govern the system for the next time step. Controlling in this sense can be seen as a scheduling on the order of dynamics the system will have to use. The objective for the controller can be to make the system stay in a given area of the state space (stability) or to reach a given region of the state space (reachability). In this thesis, we propose a novel approach that computes a scheduler where the strategy is uniform for dense subsets of the state space. Moreover, our approach only uses forward computation, which is better suited than backward computation for contractive systems. We show that our designed controllers, systems evolve to a limit cyclic behavior. We apply our method to several case studies from the literature and on a real-life prototype of a multilevel voltage converter. Moreover, we show that our approach can be extended to systems with perturbations and non-linear dynamics.