Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique

Au cours de la dernière décennie, l'informatique en nuage (Cloud Computing) suscita un important changement de paradigme dans de nombreux systèmes d'information. Ce nouveau paradigme s'illustre principalement par la délocalisation de l'infrastructure informatique hors du parc des entreprises, permettant ainsi une utilisation des ressources à la demande. La prise en charge de serveurs locaux s'est donc vue peu à peu remplacée par la location de serveurs distants, auprès de fournisseurs spécialisés tels que Google, Amazon, Microsoft. Afin d'assurer la pérennité d'un tel modèle économique, il apparaît nécessaire de fournir aux utilisateurs diverses garanties relatives à la sécurité, la disponibilité, ou encore la fiabilité des ressources mises à disposition. Ces facteurs de qualité de service (QoS pour Quality of Service) permettent aux fournisseurs et aux utilisateurs de s'accorder sur le niveau de prestation escompté. En pratique, les serveurs mis à disposition des utilisateurs doivent épisodiquement faire face à des fautes arbitraires (ou byzantines). Il s'agit par exemple de ruptures temporaires du réseau, du traitement de messages corrompus, ou encore d’arrêts inopinés. Le contexte d'informatique en nuage s'est vu néanmoins propice à l'émergence de technologies telles que la virtualisation ou la réplication de machines à états. De telles technologies permettent de pallier efficacement à l’occurrence de pannes via l'implémentation de protocoles de tolérance aux pannes.La tolérance aux fautes byzantines (BFT pour Byzantine Fault Tolerance) est un domaine de recherche implémentant les concepts de réplication de machines à états, qui vise à assurer la continuité et la fiabilité des services en présence de comportements arbitraires. Afin de répondre à cette problématique, de nombreux protocoles furent proposés. Ceux-ci se doivent d'être efficaces afin de masquer le surcoût lié à la réplication, mais également robustes afin de maintenir un niveau de performance élevé en présence de fautes. Nous constatons d'abord qu'il est délicat de relever ces deux défis à la fois: les protocoles actuels sont soit conçus pour être efficaces au détriment de leur robustesse, soit pour être robustes au détriment de leur efficacité. Cette thèse se focalise autour de cette problématique, l'objectif étant de fournir les instruments nécessaires à la conception de protocoles à la fois robustes et efficaces.Notre intérêt se porte principalement vers deux types de dénis de service liés à la gestion des requêtes. Le premier de ces dénis de service est causé par la corruption partielle d'une requête lors de son émission par un client. Le deuxième est causé par l'abandon intentionnel d'une requête lors de sa réception par un réplica. Afin de faire face efficacement à ces deux comportements byzantins, plusieurs mécanismes dédiés furent implémentés dans les protocoles de BFT robustes. En pratique, ces mécanismes engendrent d'importants surcoûts, ce qui nous permet d'introduire notre première contribution: la définition de plusieurs principes de conception génériques destinés à réduire ces surcoûts tout en assurant un niveau de robustesse équivalent.La seconde contribution de cette thèse illustre ER-PBFT, un nouveau protocole implémentant ces principes de conception sur PBFT, la référence en matière de tolérance aux fautes byzantines. Nous démontrons l'efficacité de notre nouvelle politique de robustesse, à la fois en présence de comportements byzantins mais également lors de scénarios sans faute.La troisième contribution illustre ER-COP, un nouveau protocole orienté à la fois vers l’efficacité et la robustesse, implémentant nos principes de conception sur COP, le protocole de BFT fournissant les meilleures performances à l'heure actuelle dans un environnement sans faute. Nous évaluons le surcoût engendré par l'intégration de notre politique de robustesse, et nous démontrons la capacité de ER-COP à tolérer l'occurrence de comportements byzantins. / Over the last decade, Cloud computing instigated an important switch of paradigm in numerous information systems. This new paradigm is mainly illustrated by the re-location of the whole IT infrastructures out of companies’ warehouses. The use of local servers has thus being replaced by remote ones, rented from dedicated providers such as Google, Amazon, Microsoft.In order to ensure the sustainability of this economic model, it appears necessary to provide several guarantees to users, related to the security, availability, or even reliability of the proposed resources. Such quality of service (QoS) factors allow providers and users to reach an agreement on the expected level of dependability. Practically, the proposed servers must episodically cope with arbitrary faults (also called byzantine faults), such as incorrect/corrupted messages, servers crashes, or even network failures. Nevertheless, the Cloud computing environment encouraged the emergence of technologies such as virtualization or state machine replication. These technologies allow cloud providers to efficiently face the occurrences of faults through the implementation of fault tolerance protocols.Byzantine Fault Tolerance (BFT) is a research area involving state machine replication concepts, and aiming at ensuring continuity and reliability of hosted services in presence of any kind of arbitrary behaviors. In order to handle such threat, numerous protocols were proposed. These protocols must be efficient in order to counterbalance the extra cost of replication, and robust in order to lower the impact of byzantine behaviors on the system performance. We first noticed that tackling both these concerns at the same time is difficult: current protocols are either designed to be efficient at the expense of their robustness, or robust at the expense of their efficiency. We tackle this specific problem in this thesis, our goal being to provide the required tools to design both efficient and robust BFT protocols.Our focus is mainly dedicated to two types of denial-of-service attacks involving requests management. The first one is caused by the partial corruption of a request transmitted by a client. The second one is caused by the intentional drop of a request upon receipt. In order to face efficiently both these byzantine behaviors, several mechanisms were integrated in robust BFT protocols. In practice, these mecanisms involve high overheads, and thus lead to the significant performance drop of robust protocols compared to efficien ones. This assessment allows us to introduce our first contribution: the definition of several generic design principles, applicable to numerous existing BFT protocols, and aiming at reducing these overheads while maintaining the same level of robustness.The second contribution introduces ER-PBFT, a new protocol implementing these design principles on PBFT, the reference in terms of byzantine fault tolerance. We demonstrate the efficiency of our new robustness policy, both in fault-free scenarios and in presence of byzantine behaviors.The third contribution highlights ER-COP, a new BFT protocol dedicated to both efficiency and robustness, implementing our design principles on COP, the BFT protocol providing for now the best performances in a fault-free environment. We evaluate the additional cost introduced by our robustness policy, and we demonstrate ER-COP's ability to handle byzantine behaviors.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

L'étude des circuits asynchrones est un secteur dans lequel de nombreuses recherches ont été effectuées ces dernières années. Les circuits asynchrones ont démontré plusieurs caractéristiques intéressantes comme la robustesse, l'extensibilité, la faible consommation ou le faible rayonnement électromagnétique. Parmi les différentes classes de circuits asynchrones, les circuits quasi-insensibles aux délais (QDI) ont montré des caractéristiques extrêmement intéressantes en termes de faible consommation et de robustesse aux variations PVT (Process, Voltage, Temperature). L'usage de ces circuits est notamment bien adapté aux applications fonctionnant dans un environnement sévère et pour lesquelles la consommation est un critère primordial. Les travaux de cette thèse s'inscrivent dans ce cadre et visent la conception et la synthèse de machines à états asynchrones (QDI) faiblement consommantes. Une méthode de synthèse dédiée à des contrôleurs asynchrones à faible consommation a donc été développée. Cette technique s'est montrée particulièrement efficace pour synthétiser les contrôleurs de grande taille. La méthode s'appuie sur une modélisation appropriée des contrôleurs et une technique de synthèse dirigée par la syntaxe utilisant des composants spécifiques appelés séquenceurs. Les circuits obtenus ont été vérifiés formellement afin de s'assurer de leurs propriétés en termes de robustesse et de correction fonctionnelle. A cette occasion, une méthode de vérification formelle a été mise en place pour valider les contrôleurs d'une part, et plus généralement, n'importe quel circuit asynchrone d'autre part. Cette technique fait appel à une modélisation hiérarchique des circuits asynchrones en PSL et à un outil de vérification formelle (RAT).

Des développements technologiques récents concernant les photodiodes à effet avalanche (PDA) ont mené à la conception et la fabrication d'un tout nouveau module de détection de radiation TEP (tomographie d'émission par positrons) destiné à l'imagerie moléculaire préclinique. Il est basé sur une matrice de 8 par 8 scintillateurs LYSO (ortho-silicate de lutétium dopé au cérium, cerium-doped lutetium yttrium orthosilicate ) individuellement couplés aux pixels de deux matrices monolithiques de 4 par 8 PDA. Cette avancée, pouvant amener la résolution spatiale d'un scanner à passer sous la barrière du mm, exige la conception d'un tout nouveau système d'acquisition de données. En effet, il faut adapter le système de lecture individuelle de chacun des pixels du bloc de détection de façon à satisfaire la multiplication par ~8, relativement à une version antérieure (le LabPET[indice supérieur TM] I), de la densité de pixels du futur scanner LabPET[indice supérieur TM] II. Conséquemment, le traitement de signal numérique ne peut être exclusivement embarqué dans les matrices de portes logiques programmable (field-programmable gate array , FPGA) du système d'acquisition, en considérant les aspects monétaires, d'espace occupé et de puissance consommée de l'ensemble du projet LabPET[indice supérieur TM] II. De façon à s'adapter à cette nouvelle réalité, un nouveau circuit intégré à application spécifique (application specific integrated circuit, ASIC) à signaux mixtes avec 64 canaux d'acquisition, fabriqué avec la technologie TSMC CMOS 0,18 [micromètre], a été conçu. L'ASIC utilise la méthode de temps au-dessus d'un seuil (time over threshold , ToT), déjà implantée dans des applications de physique des hautes-énergies, de manière à extraire numériquement l'information relative à un rayonnement interagissant avec la matrice de détection (l'énergie, le temps et le numéro de pixel de l'événement). Dans le cadre de ce projet, une architecture complexe de machines à états-finis, cadencée par une horloge de 100 MHz, a été implantée et elle permet à l'ASIC d'identifier le taux anticipé de 3 000 événements par seconde par canal. Ceci est réalisé en calculant en temps réel le paramètre ToT tout en assurant la calibration adéquate de chacune des chaînes d'acquisition. Le circuit intégré peut caractériser jusqu'à 2 Mévénements/s malgré son unique lien différentiel à bas voltage (low-voltage differential signaling, LVDS) de transfert de données et consomme environ 600 mW. L'ASIC a été développé en suivant un processus de conception de circuits intégrés à signaux mixtes. Il permet notamment de minimiser et de vérifier l'impact des indésirables effets parasites sur la circuiterie analogique et numérique de l'ensemble avant que les dessins de masques ne soient envoyés vers la fonderie pour fabriquer le circuit désiré.