Divers domaines d'application des systèmes électroniques, comme par exemple les implants médicaux ou les puces cryptographiques pour appareils portables, exigent à la fois une très faible puissance dissipée et un niveau de fiabilité très élevé. De plus, comme la miniaturisation des technologies CMOS approche ses limites ultimes, ces exigences deviennent nécessaires pour l'ensemble de l'industrie de microélectronique. En effet, en approchant ces limites les problèmes de la dissipation de puissance, du rendement de fabrication et de la fiabilité des composants empirent, rendant la poursuite de miniaturisation nanometric de plus en plus difficile. Ainsi, avant que ces problèmes bloquent le progrès technologique, des nouvelles solutions au niveau du processus de fabrication et du design sont exigées pour maintenir la puissance dissipée, le rendement de fabrication et la fiabilité à des niveaux acceptables. Le projet de thèse visé le développant des architectures tolérant aux fautes capables de répondre à ces défis pour les technologies de fabrication CMOS présentes et à venir. Ces architectures devraient permettre d'améliorer le rendement de fabrication et la fiabilité et réduire en même temps la puissance dissipée des composants électroniques. Elles conduiraient en une innovation majeure, puisque les architectures tolérant aux fautes traditionnelles permettraient d'améliorer le rendement de fabrication et la fiabilité des composants électroniques aux dépens d'une pénalité significative en puissance consommée.

La recherche de la sûreté de fonctionnement des systèmes complexes impose une démarche de conception rigoureuse. Les travaux de cette thèse s’inscrivent dans le cadre la modélisation formelle des systèmes de contrôle autonomes tolérants aux fautes. Le premier objectif a été de proposer une formalisation d’une architecture générique en couches fonctionnelles qui couvre toutes les activités essentielles du système de contrôle et qui intègre des mécanismes de sécurité. Le second objectif a été de fournir une méthode et des outils pour évaluer qualitativement les exigences de sécurité. Le cadre formel de modélisation et d’évaluation repose sur le formalisme Event-B. La modélisation Event-B proposée tire son originalité d’une prise en compte par raffinements successifs des échanges et des relations entre les couches de l’architecture étudiée. Par ailleurs, les exigences de sécurité sont spécifiées à l’aide d’invariants et de théorèmes. Le respect de ces exigences dépend de propriétés intrinsèques au système décrites sous forme d’axiomes. Les preuves que le principe d’architecture proposé satisfait bien les exigences de sécurité attendue ont été réalisées avec les outils de preuve de la plateforme Rodin. L’ensemble des propriétés fonctionnelles et des propriétés relatives aux mécanismes de tolérance aux fautes, ainsi modélisées en Event-B, renforce la pertinence de la modélisation adoptée pour une analyse de sécurité. Cette approche est par la suite mise en œuvre sur un cas d’étude d’un drone ONERA. / The study of complex system safety requires a rigorous design process. The context of this work is the formal modeling of fault tolerant autonomous control systems. The first objective has been to provide a formal specification of a generic layered architecture that covers all the main activities of control system and implement safety mechanisms. The second objective has been to provide tools and a method to qualitatively assess safety requirements. The formal framework of modeling and assessment relies on Event-B formalism. The proposed Event-B modeling is original because it takes into account exchanges and relations betweenarchitecture layers by means of refinement. Safety requirements are first specified with invariants and theorems. The meeting of these requirements depends on intrinsic properties described with axioms. The proofs that the concept of the proposed architecture meets the specified safety requirements were discharged with the proof tools of the Rodin platform. All the functional properties and the properties relating to fault tolerant mechanisms improve the relevance of the adopted Event-B modeling for safety analysis. Then, this approach isimplemented on a study case of ONERA UAV.