Validation temporelle de réseaux embarqués critiques et fiables pour l\u27automobile

Dans le domaine de l\u27automobile, la tendance actuelle pour les constructeurs est de remplacer certains systèmes hydrauliques et mécaniques par des systèmes x-by-wire : composants électroniques communicants grâce à un réseau. Deus aspects particuliers de la fiabilité de ces architectures sont traités dans ces travaux : l\u27aspect temporel et sa tolérance aux fautes. Afin de garantir la fiabilité de ces systèmes critiques, il est nécessaire de vérifier le respect de leurs contraintes strictes par validation. Les travaux de cette thèse sont consacrés à la validation temporelle en présence de fautes d\u27une architecture dédiées à ces systèmes : TTA (Time-Triggered Architecture), et en proposent une méthodologie de validation. Pour cela, il a été nécessaire de choisir un formalisme de modélisation adapté aux différentes caractéristiques de l\u27architecture et à ces contraintes, en particulier sur le plan temporel. Une étude comparative théorique et expérimentale de plusieurs formalismes a permis de choisir les TSA (Times Safety Automata), extension des automates temporisés implémentée dans l\u27outil UPPAAL. Le modèle obtenu est ensuite analysé par model-checking. Cette méthodologie a permis la validation des bornes temporelles des différents services de TTA, c\u27est à dire leur pire temps d\u27exécution, sous certaines hypothèses de fautes. Elle complète les processus de validation de TTA existants, d\u27une part les approches de tests, de simulations et d\u27injections de fautes qui ne sont pas exhaustives, et d\u27autre part des approches formelles (preuve de théorème) qui ne permettaient pas de prendre en compte les bornes temporelles ou l\u27interaction des algorithmes