De nombreux protocoles Total Order Broadcast uniformes ont été conçus au cours des 30 dernières années. Ils peuvent être classés en deux catégories: ceux qui visent une faible latence, et ceux qui visent à haut débit. Latence mesure le temps nécessaire pour effectuer un seul message diffusé sans prétention, alors que le débit mesure le nombre d'émissions que les processus peuvent compléter par unité de temps quand il y a discorde. Tous les protocoles qui ont été conçus pour autant faire l'hypothèse que le réseau sous-jacent ne sont pas partagées par d'autres applications en cours d'exécution. Ceci est une préoccupation majeure à condition que dans les centres de données modernes (aka Clouds), l'infrastructure de mise en réseau est partagée par plusieurs applications. La conséquence est que, dans de tels environnements, le total des protocoles afin de diffusion uniformes présentent des comportements instables.Dans cette thèse, j'ai conçu et mis en œuvre un nouveau protocole pour la Total Order Broadcast uniforme qui optimise la performance lorsqu'il est exécuté dans des environnements multi-Data Centers et le comparer avec plusieurs algorithmes de l'état de l'art.Dans cette thèse, je présente deux contributions. La première contribution est MDC-Cast un nouveau protocole pour Total Order Broadcast dans lesquelles il optimise les performances des systèmes distribués lorsqu'ils sont exécutés dans des environnements multi-centres de données. MDC-Cast combine les avantages de la multidiffusion IP dans les environnements de cluster et unicast TCP/IP pour obtenir un algorithme hybride qui fonctionne parfaitement entre les centres de données.La deuxième contribution est un algorithme conçu pour déboguer les performances dans les systèmes distribués en boîte noire. L'algorithme n'est pas encore publié car il nécessite plus de tests pour une meilleure généralisation. / Many uniform total order broadcast protocols have been designed in the last 30 years. They can be classified into two categories: those targeting low latency, and those targeting high throughput. Latency measures the time required to complete a single message broadcast without contention, whereas throughput measures the number of broadcasts that the processes can complete per time unit when there is contention. All the protocols that have been designed so far make the assumption that the underlying network is not shared by other applications running. This is a major concern provided that in modern data centers (aka Clouds), the networking infrastructure is shared by several applications. The consequence is that, in such environments, uniform total order broadcast protocols exhibit unstable behaviors.In this thesis, I provide two contributions. The first contribution is MDC-Cast a new protocol for total order broadcasts in which it optimizes the performance of distributed systems when executed in multi-data center environments. MDC-Cast combines the benefits of IP-multicast in cluster environments and TCP/IP unicast to get a hybrid algorithm that works perfectly in between datacenters.The second contribution is an algorithm designed for debugging performance in black-box distributed systems. The algorithm is not published yet due to the fact that it needs more tests for a better generalization.

Le langage UML est devenu un standard de fait, y compris pour le développement de systèmes critiques. Néanmoins, les outils actuels apportent peu d'aide pour exploiter et vérifier les modèles proposés, surtout en cours de développement. Cette thèse se concentre sur l'aide à la construction d'architectures en UML durant les phases d'analyse et de conception de systèmes réactifs. Elle vise à développer un cadre théorique et pragmatique pour mettre en œuvre une approche incrémentale. Ce cadre fournit un outil permettant de vérifier les architectures durant leur modélisation. Les architectures sont modélisées par des diagrammes UML de structures composites alors que les composants primitifs sont présentés par une combinaison de diagrammes de machines d'états et de diagramme d'activités. Ce travail offre les moyens de vérifier d'une part si une nouvelle architecture est un raffinement, une extension ou un incrément de celle définie durant les étapes précédentes, et d'autre part si un composant est compatible avec un environnement ou s'il est substituable par un autre. L'analyse des architectures impose de leur donner une sémantique formelle. Concernant les composants primitifs, nous leur associons une sémantique en LTS (Labelled Transition Systems) ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états et diagrammes d'activités en LTS. Concernant les composants composites, nous leur associons un LTS en transformant un diagramme de structure composite en une spécification Exp.Open, puis en générant la fusion des LTS grâce à la boîte à outils CADP. Dans un second temps, nous avons mis en œuvre des techniques de vérifications de relations de conformité de LTS que sont les préordres de raffinement, d'extension, et d'incrément. Nous avons également défini et implanté une relation de compatibilité et de substituabilité. L'ensemble de ces techniques de construction incrémentale se positionne selon deux axes. L'axe vertical représente le niveau d'abstraction. L'évolution d'une architecture peut se faire sur cet axe dans deux sens : i) par des techniques de raffinement dans le sens descendant et ii) par des techniques d'abstraction dans le sens ascendant. L'axe horizontal représente le niveau de couverture des exigences. L'évolution d'une architecture peut se faire sur cet axe selon deux sens : i) par des techniques d'extension et ii) par des techniques de restriction. Ces travaux ont été réalisés de façon théorique et pratique : ils ont donné lieu au développement d'un outil dédié à la construction incrémentale de modèles UML, appelé IDCM (Incremental Development of Conforming Models), regroupant la transformation de modèles et la mise en œuvre de l'ensemble des relations incrémentales. Ceci a été validé sur diverses études de cas. / UML is becoming a de facto standard, including for development of dependable systems. However, current tools offer little help to take benefit of proposed models and to verify them, especially during development phases. This thesis focuses on supporting construction of UML architectures of reactive systems. It aims at developing a theoretic and pragmatic framework to implement the incremental approach. The framework provides tools to verify the coherenceof architectures during the modelling phase. Architectures are modelled by UML diagram of composite structures while primitive components are represented by a combination of state machine diagram and activity diagram. This work provides a means to verify in one hand if a new architecture is a refinement, an extension or an increment of those defined in the previous steps, and in another hand, if a component is compatible with an environment or if it is substitutableby another.In order to analyse UML architectures, we must give them a formal semantics. We associated primitive components with LTS (Labelled Transition Systems) which led us to define a procedure for automatic transformation of state machines and activities diagrams into LTS. We associated composite components with LTS by transforming a diagram of composite structure into Exp.Open specification, then by generating LTS fusion with the toolbox CADP. We have implemented verification techniques of conformance relations on LTS such as the preorders: refinement, extension, and increment. We also defined and implemented compatibility relation and substitutability relation. All these incremental construction techniques are positioned along two axes. The vertical axis represents the level of bstraction.The development of an architecture following this axis in two directions: i) refinement techniques in the downward direction and ii) abstraction techniques in the upward direction. The horizontal axis represents the coverage level of requirements. The development of architectures can be realized following this axis in two directions : i) extension direction and ii) restrictiondirection.This work has been carried out in theory and practice : it has led to the development of a dedicated tool for incremental construction of UML models, called IDCM (Incremental Development of Conforming Models), grouping the transformation of models and the implementation of a set of incremental relations. This has been validated on various case studies.

La validation fonctionnelle d'un système matériel consiste a vérifier le système vis-a-vis de son fonctionnement attendu. Il existe deux façons de spécifier ce fonctionnement attendu. D'une part, la spécification peut être donnée sous forme d'une description fonctionnelle complète. D'autre part, l'expression de cette spécification peut être donnée sous forme d'un ensemble de propriétés temporelles critiques. Ces deux façons de spécifier les systèmes matériels ont donne lieu a deux problèmes de vérification. Notre domaine d'étude concerne les systèmes matériels numériques séquentiels synchrones. Le travail présente dans ce document développe une approche de vérification unifiée, fondée sur le modèle de machines d'états finis, pour résoudre les deux problèmes de vérification sur ces systèmes. Dans cette approche, tout probleme de vérification se ramène a définir une machine d'états finis sur laquelle la vérification sera réalisée. L'application du langage lustre et de l'outil de vérification Lesar associe a été étudiée dans le but de valider cette approche. Dans cette application, la resolution des deux problèmes de vérification se ramène a définir un programme lustre ayant une seule sortie. La vérification consiste a vérifier que cette sortie est la constante booléenne 1. Cette vérification est réalisée automatiquement par l'outil de vérification Lesar