L'annonce de l'essor du chiffrement des données se heurte à celle de l'avènement du "big data". Il n'est maintenant plus suffisant d'envoyer et de recevoir des données, il faut pouvoir les analyser, les exploiter ou encore les partager à grande échelle. Or, les données à protéger sont de plus en plus nombreuses, notamment avec la prise de conscience de l'impact qu'ont les nouvelles technologies (smartphones, internet of things, cloud,...) sur la vie privée des utilisateurs. En rendant ces données inaccessibles, le chiffrement bloque a priori les fonctionnalités auxquelles les utilisateurs et les fournisseurs de service sont habitués. Pour rétablir ces fonctionnalités, il est nécessaire de savoir calculer des fonctions de données chiffrées, et cette thèse explore plusieurs pistes dans ce sens. Dans une première partie, nous nous intéressons au chiffrement totalement homomorphe qui permet de réaliser des calculs arbitraires sur les données chiffrées. Ce type de chiffrement est cependant particulièrement coûteux, notamment à cause de l'appel souvent nécessaire à une procédure très coûteuse : le réamorçage. Nous prouvons ici que minimiser le nombre de réamorçages est un problème NP-complet et donnons une méthode pratique pour approximer ce minimum. Dans une seconde partie, nous étudions des schémas dédiés à une fonctionnalité donnée. Le premier cas d'usage considéré est celui de la déduplication vérifiable de données chiffrées. Il s'agit pour un serveur de stockage externe d'être assuré qu'il ne conserve qu'un seul exemplaire de chaque fichier, même si ceux-ci sont chiffrés, ce qui lui permet d'optimiser l'usage de ses ressources mémoires. Ensuite, nous proposons un schéma de chiffrement cherchable permettant de détecter des intrusions dans un réseau de télécommunications chiffrés. En effet, le travail d'inspection du réseau par des moteurs d'analyse est actuellement entravé par la croissance du trafic chiffré. Les résultats obtenus permettent ainsi d'assurer la confidentialité des échanges tout en garantissant l'absence d'intrusions malveillantes dans le trafic / Nowadays, encryption and services issued of ``big data" are at odds. Indeed, encryption is about protecting users privacy, while big data is about analyzing users data. Being increasingly concerned about security, users tend to encrypt their sensitive data that are subject to be accessed by other parties, including service providers. This hinders the execution of services requiring some kind of computation on users data, which makes users under obligation to choose between these services or their private life. We address this challenge in this thesis by following two directions.In the first part of this thesis, we study fully homomorphic encryption that makes possible to perform arbitrary computation on encrypted data. However, this kind of encryption is still inefficient, and this is due in part to the frequent execution of a costly procedure throughout evaluation, namely the bootstrapping. Thus, efficiency is inversely proportional to the number of bootstrappings needed to evaluate functions on encrypted data. In this thesis, we prove that finding such a minimum is NP-complete. In addition, we design a new method that efficiently finds a good approximation of it. In the second part, we design schemes that allow a precise functionality. The first one is verifiable deduplication on encrypted data, which allows a server to be sure that it keeps only one copy of each file uploaded, even if the files are encrypted, resulting in an optimization of the storage resources. The second one is intrusion detection over encrypted traffic. Current encryption techniques blinds intrusion detection services, putting the final user at risks. Our results permit to reconcile users' right to privacy and their need of keeping their network clear of all intrusion

L'ingénierie des modèles (IDM) a depuis très largement démontré sa pertinence dans les développements logiciels; restait alors à démontrer son applicabilité dans le développement de tout système d'information. Aujourd'hui, de nombreuses expérimentations montrent avec plus ou moins de succès que l'IDM peut parfaitement supporter d'autres domaines comme le domaine du co-design ou celui de l'ingénierie des processus.Dans le domaine du co-design, les activités de conception consiste essentiellement à concevoir et analyser des systèmes implantées sur des plateformes spécifiques (SoC, MPSoC, NoC, etc.): cela nécessite l'utilisation de langages dédiés permettant de représenter : les constituants du système ou de la plateforme, les contraintes non fonctionnelles, les allocations spatio-temporelles des blocs du système sur la plateforme, les analyses qui découlent des choix d'allocation. Le langage de modélisation généraliste UML (Unified Modeling Language) ne pouvait que très difficilement satisfaire de tels besoins. C'est pourquoi l'OMG (Object Management Group) a standardisé une extension d'UML dédiée à la conception et l'analyse de systèmes embarqués temps réel (MARTE). L'objectif premier de cette thèse est de proposer une méthodologie de conception de SoPC (System-on-Programmable-Chip) basée sur l'utilisation de modèles qui fait la synthèse des approches proposées par les communautés de l'ESL et de l'IDM.Aussi avons-nous poussé la réflexion sur les manières de capitaliser au mieux notre méthodologie et sur sa mise en œuvre dans l'élication des processus de co-design. C'est la raison pour laquelle, après avoir fait une étude sur la formalisation des processus de développement, nous avons trouvé opportun de proposer notre propre extension du langage SPEM (Software and System Process Engineering Modeling), standardisé par l'OMG, afin d'y intégrer des concepts manquants, essentiels à notre sens à la représentation des processus IDM de co-design. / The relevancy of the Model Based Approach (MBE) applied in the field of software engineering has been widely demonstrated though several experiments. In the field of co-design, business activities are mainleny design and analysis activities of complex systems implemented into chips (SoC - System-on-Chip) or reprogrammable chip (SoPC) - System-on-Programmable-Chip). Those activities require dedicated languages and tools allowing capture of : system or platform components, non-functional properties, allocation of system blocks onto the platform, either into space or into time, subsequent analysis to allocation choices. The Unified Modeling Language (UML) is a general purpose language that does not fit to such activities. That is why the OMG has standardized a UML profile dedictated to design and analysis of Real-Time Embedded Systems (MARTE). Associated to such language, on of the goal of this thesis is to propose a clear methodology that make benefits of both MBE and Electronic System Level (ESL) techniques. Beneath the simple proposition of an MBE/ESL methodology, another goal of this thesis is to propose a better capitalization of methodology rules allowing a continuous maturity of processes. That is why we found relevant to propose an extension to SPEM in order to introduce missing concepts to acheive our goals.

The need for trustworthy system operation has been acknowledged in many circles. However, establishing that a system is trustworthy is a significant challenge. While trusted computing proposes technical mechanisms towards this end, less attention is directed towards providing a basis for trusting such systems. Consequently, it is not clear: (i) how such mechanisms influence the overall trust in a system; (ii) the properties and assumptions upon which trust is based; and (iii) the evidence necessary to reason about these properties. This can be attributed to a number of factors including: (i) the complexity of modern systems; (ii) a lack of consensus on a definition of trust; and (iii) a lack of a systematic approach for identifying and using evidence to reason about trust-related properties. This dissertation presents research towards addressing these challenges. We argue that an architectural approach provides effective abstractions for making trust properties and assumptions explicit and reasoning about a system's ability to satisfy these properties. We propose a framework for identifying, categorising and mapping trust-properties to aspects of a system that could be used to reason about these properties. Guided by this framework, we propose and develop models for representing knowledge about a particular aspect and using it to reason about trust-properties. A semantic model, based on the semantics of Z, is developed to characterise building blocks of trustworthy systems and to demonstrate how the system's constituents determine its trustworthiness. An abstraction model based on formal verification is developed to reason about the impact of the system's construction and configuration on its trustworthiness. Finally, two complementary models for capturing the runtime aspects of the system are developed. A trace-based model enables analysis of runtime evidence in the form of event logs and a provenance-based model captures operations on the system as a provenance graph. The models are validated on a trusted grid architecture, a password manager and a trustworthy collaborative system.

Le protocole Pastry réalise une table de hachage distribué sur un réseau pair à pair organisé en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implémentations de Pastry, il n'y a pas encore eu de travaux pour décrire formellement l'algorithme ou vérifier son bon fonctionnement. Intégrant des structures de données complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le réseau, ce protocole représente un intérêt certain pour la vérification formelle. La thèse se focalise sur le protocole Join de Pastry qui permet à un noeud de rejoindre le réseau. Les noeuds ayant intégré le réseau doivent avoir une vue du voisinage cohérente entre eux. La propriété principale de correction, appelée CorrectDelivery, assure qu'à tout moment il y a au plus un noeud capable de répondre à une requête pour une clé, et que ce noeud est le noeud le plus proche numériquement à ladite clé. Il n'est pas trivial de maintenir cette propriété en présence de churn. Ce travail nous a permis de découvrir des violations inattendues de la propriété dans les versions publiées de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est conçu et vérifié en utilisant l'assistant interactif à la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypothèses de IdealPastry. Il est montré formellement que LuPastry vérifie CorrectDelivery sous l'hypothèse qu'aucun noeud ne quitte le réseau. Cette hypothèse ne peut être relâchée à cause du risque de perte de connexion du réseau dans le cas où plusieurs noeuds quittent le réseau en même temps / Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network

La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

L'étude des réseaux sur puces (NoC) est un domaine de recherche qui traite principalement la communication globale dans les systèmes sur puce (SoC). La topologie choisie et l'algorithme de routage jouent un rôle essentiel durant la phase de conception des architectures NoC. La modélisation des structures répétitives telles que les topologies des réseaux sur puce sous des formes graphiques pose un défi particulier. Cet aspect peut être rencontré dans les applications orienté contrôle/données intensif tel que le codeur vidéo H.264. Model Driven Engineering est une méthodologie de développement logiciel où le système complet est modélisé à un niveau d'abstraction élevé en utilisant un langage de modélisation unifié comme l’UML/MARTE. Le profil UML pour la modélisation et l'analyse des systèmes embarqués en temps réel (MARTE) est la norme actuelle pour la modélisation des SoCs.Cette thèse décrit une méthodologie adéquate pour la modélisation des NoCs en utilisant le profil MARTE. L'étude proposée a montré que le paquetage RSM (Repetitive Structure Modeling) du profil MARTE est assez puissant pour modéliser différent types de topologies. En utilisant cette méthodologie, plusieurs aspects tels que l’algorithme de routage sont modélisés en se basant sur les machines d'état. Ceci permet au profil MARTE à être assez complet pour la modélisation d'un grand nombre d’architectures de NoCs. Certains travaux sont en cours pour synthétiser ces réseaux, en VHDL à partir de ces modèles. Pour la validation de la méthodologie proposée, une approche de co-design a été étudiée par l’implémentation d'un système de codage vidéo H.264 sur un NoC de type Diagonal Mesh en utilisant model en « Y » de l’outil Gaspard2. Avant de passer à l'association de l'application/architecture, une optimisation architecturale ciblant la réduction de la puissance consommée du module le plus critique (Estimateur de Mouvement) de l'application a été effectué. Ainsi, une architecture VLSI flexible d’un estimateur de mouvement à blocks variables (FSVBSME) a été proposée. / The study of Networks on Chips (NoCs) is a research field that primarily addresses the global communication in Systems-on-Chip (SoCs). The selected topology and the routing algorithm play a prime role during the design of NoC architectures.The modeling of repetitive structures such as network on chip topologies in graphics forms poses a particular challenge. This aspect may be encountered in intensive data/control oriented applications such as H.264 video coder. Model driven engineering is a software development methodology where the complete system is modeled at a high abstraction level using a modeling language as UML/MARTE. The UML profile for Modeling and Analysis of Real-Time Embedded systems (MARTE) is the current standard for the SoCs modeling. This thesis describes an adequate methodology for modeling NoCs by using the MARTE standard profile. The proposed study has shown that the Repetitive Structure Modeling (RSM) package of MARTE profile is powerful enough for modeling different topologies. By using this methodology, several aspects such as routing algorithm are modeled based finite state machines. This allows to the MARTE profile to be complete enough for modeling a large number of NoCs architectures. Some work is on-going to synthesize such networks in VHDL from such models. While validating the proposed methodology, a co-design approach has been studied by mapping a H264 video coding system onto a Diagonal Mesh NoC by using the Y Chart of Gaspard2 tool. Before allowing the association of the application/architecture, an architectural optimization targeting power minimization of the most critical module of the application has been performed. So, a flexible VLSI architecture for full-search VBSME (FSVBSME) has been proposed.

La Sûreté de Fonctionnement (SdF) est un domaine étudié de façon de plus en plus rigoureuse par les concepteurs. Si la SdF relative aux organes bénéficie de retours d'expériences sur lesquels le développement de solutions physiques peut s'appuyer, tel n'est pas le cas lorsqu'il s'agit de concevoir les architectures fonctionnelles d'un produit. L'architecte Système conceptualise et conçoit un système qui doit fournir un service selon certaines performances ; son cadre de référence, à savoir l'Ingénierie Système étant lacunaire en matière de SdF. De la sorte, l’ingénieur expert en SdF intervient après l'architecte, réalise ses propres analyses fonctionnelles, perturbant le travail réalisé et obligeant à des boucles qui pourraient être évitées. Il convient de ce fait, pour les industriels, de s'intéresser de près à l'alignement entre la SdF et l'IS. Nous avons obtenu quatre résultats. Le premier est un modèle conceptuel de l’Ingénierie de Systèmes Sûrs de Fonctionnement. Ce modèle conceptuel permet de définir les concepts et les liens entre le domaine de l'IS et celui de la SdF. Le macroprocessus présenté permet de définir l’architecture d’un système sûr. Plusieurs activités spécifiques sont présentes dans le macroprocessus. Ainsi, nous avons développé une méthode qui concerne l’analyse des risques en vue externe. Nous avons proposé une nouvelle méthode qui permet de définir les Safety Goals associé pour les scénarios critiques et une autre permettant l’analyse des architectures fonctionnelles d’un point de vue dysfonctionnel pour définir les Functional Safety Requirements. Cette méthode repose sur des mécanismes de propagation de défaillance / Safety is an area which is increasingly stringent by designers. If Safety on components benefits from experience feedback on which the development of physical solutions can support, this is not the case when it comes to designing functional architecture of a product. The System Architect conceptualizes and designs a system that must provide service according to a defined level of performance; its framework, namely the System Engineering is incomplete for safety. In this way, the safety expert comes after architects, performs his/her own functional analyzes, disrupting the work and forcing loops that could be avoided. It should therefore, for industry to pay close attention to the alignment between the SE and safety. We got four results. The first one is a conceptual model of the Safe Systems Engineering. This conceptual model, divided into three views defines the concepts and relationships between the field of SE and that of safety. The assembly has a strong semantic consistency. The proposed macroprocess permits to define the architecture of a safe system. For this, we have divided into three design phases and four views. Thus, we developed a methodology on risk analysis in external view. Given the limitations of methods like Preliminary Hazard Analysis regarding the deliverables required by the ISO 26262:2011 (Hazard Analysis and Risk Assessment), we proposed a new method for defining the Safety Goals associated for critical scenarios and another method for analyzing the functional architecture with a dysfunctional point of view to define the Functional Safety Requirements

Society is challenging systems engineers by demanding increasingly complex and integrated IT systems (Northrop et al., 2006; RAE, 2004) e.g. integrated enterprise resource planning systems, integrated healthcare systems and business critical services provisioned using cloud based resources. These types of IT system are often systems-of-systems (SoS). That is to say they are composed of multiple systems that are operated and managed by independent parties and are distributed across multiple organisational boundaries, geographies or legal jurisdictions (Maier, 1998). SoS are notorious for becoming problematic due to interconnected technical and social issues. Practitioners claim that they are ill equipped to deal with the sociotechnical challenges posed by system-of-systems. One of these challenges is to identify the socio-technical threats associated with building, operating and managing systems whose parts are distributed across organisational boundaries. Another is how to troubleshoot these systems when they exhibit undesirable behaviour. This thesis aims to provide a modelling abstraction and an extensible technique that enables practitioners to identify socio-technical threats prior to implementation and troubleshoot SoS post-implementation. This thesis evaluates existing modelling abstractions for their suitability to represent SoS and suggests that an agent-responsibility based modelling abstraction may provide a practical and scalable way of representing SoS for socio-technical threat identification and troubleshooting. The practicality and scalability of the abstraction is explored through the use of case studies that motivate the extension of existing responsibility-based techniques so that new classes of system (coalitions-of-systems) and new classes of threat (agent-related threats) may be analysed. This thesis concludes that the notion of ‘responsibility' is a promising abstraction for representing and analysing systems that are composed of parts that are independently managed and maintained by agents spanning multiple organisational boundaries e.g. systems-of-systems, enterprise-scale systems.

Dans cette thèse, nous proposons une méthodologie de co-conception des systèmes dynamiquement reconfigurables basés sur FPGA. Notre méthodologie s’appuie sur l’Ingénierie Dirigée par les Modèles (IDM) dont la spécification des modèles est décrite avec le profil MARTE. Les travaux présentés visent à garantir la flexibilité, la réutilisabilité et l’automatisation afin de faciliter le travail du concepteur et d’améliorer sa productivité. La première contribution réside dans la modélisation à haut-niveau d’abstraction permettant de cacher un grand nombre de détails d’implémentation. Un flot de conception est défini pour la modélisation des FPGAs, basé sur l’IDM afin d’assurer l’automatisation de la génération de code. Suivant ce flot, plusieurs modèles sont créés moyennant principalement les concepts de MARTE. Cependant,la modélisation de certains concepts de la reconfiguration dynamique a nécessité des extensions dans MARTE que nous avons identifiées et intégrées dans un nouveau profil qui étend MARTE baptisé RecoMARTE. La seconde contribution est l’automatisation de la chaîne de transformations et la validation expérimentale. Afin d’assurer l’automatisation de notre flot de conception vers la génération du code, une chaîne de transformations a été utilisée. Nous passons ainsi d’un modèle MARTE/RecoMARTE vers une description intermédiaire selon le standard IP-XACT afin de générer des fichiers utilisés dans l’environnement XPS de Xilinx. Cette automatisation permet d’accélérer la phase de conception et éviter les erreurs dues à la manipulation directe des détails. Enfin, un exemple d’application de traitement d’image a été élaboré afin de démontrer et valider notre méthodologie. / The works presented in this dissertation propose a co-design methodology of dynamically reconfigurable systems based on FPGA. Our methodology is based on the Engineering Model Driven approach (MDE). The models specification is done in MARTE profile.It aims to ensure flexibility, reusability and automation to facilitate the work of designer and improve his productivity. The first contribution related to this thesis is identifying parts of dynamically reconfigurable FPGA that can be modeled at high abstraction levels. So, we defined a design flow based on the MDE to ensure the automation of code generation. Using this flow, several models are created mainly through MARTE profile concepts. However, the modeling concepts of dynamic reconfiguration on FPGAs required extensions in MARTE. Thus, we identified the missing concepts to be integrated in a new profile that extends MARTE : RecoMARTE. The second contribution allows the chain automation and experimental validation. To integrate our design flow and to automate code generation, a processing chain was used. The final model resulting from the proposed MARTE-based design flow is given as input to this chain. We thereby move from MARTE/RecoMARTE models to an intermediate description according to the IP-XACT standard to finally generate files describing the complete system in the Xilinx XPS environment. This automation allows to accelerate the design phase and avoid errors due to the direct manipulation of these details. Finally, the proposed MARTE-based design flow and transformation chain were used for an image processing system design, which showed the benefits of our contributions in terms of design reusability and automation.

Depuis plusieurs décennies, la congestion urbaine est de plus en plus répandue et dégrade la qualité de vie des habitants des villes. Plusieurs méthodes sont utilisées pour diminuer la congestion urbaine, notamment la régulation du trafic et la valorisation des transports en commun. Depuis les années 1990 l'utilisation d‘outils issus de l'intelligence artificielle, et en particulier des méthodes distribuées et les systèmes multi-agents, a permis de concevoir de nouvelles méthodes de régulation du trafic. Parallèlement, l'amélioration des capacités de communication des véhicules et des conducteurs et l'arrivée de voitures autonomes permettent d'envisager de nouvelles approches en matière de régulation. Le travail de recherche proposé dans le cadre de cette thèse est structuré en deux volets. Nous proposons d'abord une méthode de régulation du trafic à une intersection s'appuyant sur la négociation automatique. Notre méthode se fonde sur un système d'argumentation décrivant l'état du trafic et les préférences de chacun, appuyé par des méthodes de raisonnement pour les véhicules et les infrastructures. Dans le deuxième volet de cette thèse, nous proposons une méthode de coordination des bus avec le reste du trafic. Celle-ci permet à un bus de se coordonner de manière anticipative avec les prochaines intersections qu'il prévoit de traverser, afin de mettre en place une politique commune de régulation qui permet au bus d'atteindre son prochain arrêt en subissant le minimum de congestions potentielles / Since several decades, urban congestion is more and more widespread and deteriorate the quality of life of citizens who live in cities. Several methods are used to reduce urban congestion, notably traffic regulation and promotion of public transportation. Since the 1990's, the usage of tools from artificial intelligence, particularly distributed systems and multi-agent systems, allowed to design new methods for traffic regulation. Indeed, these methods ease to take into account the complexity of traffic-related problems with distribution. Moreover, the improvement of the communication abilities of the vehicles and the coming of autonomous vehicles allow to consider new approaches for regulation.The research work presented in this work is twofold. First we propose a method for traffic regulation at an intersection based on automatic negotiation. Our method is based on an argumentation system describing the state of the traffic and the preferences of each vehicle, relying on reasonning methods for vehicles and infrastructures. In the second part of this thesis, we propose a coordination method for buses for the rest of the traffic. This method allows a bus to coordinate in an anticipatory way with the next intersections on its trajectory, in order to define a common regulation policy allowing the bus to reach its next stop without suffering from potential congestions