Validation temporelle de réseaux embarqués critiques et fiables pour l'automobiles
Institution:
Lyon, INSADisciplines:
Directors:
Abstract EN:
In the automotive domain, the current tendency for the manufacturers is to replace hydraulic and mechanical systems by x-by-wire systems : electronic components communicating through a network. Two particular aspects of the reliability of this architectures are studied in this work: the temporal aspect and its fault tolerance. In order to guarantee the reliability of this critical systems, it is necessary to verify the respect of their constraints by validation. Works of this thesis is devoted to the temporal validation in presence of faults of a specific architecture dedicated to these systems: TTA (Time-Triggered Structure), and propose a methodology of validation for this architecture. For that, it was necessary to choose a modelling formalism which fits well to the characteristics of the architecture and its constraints, in particular on the temporal domain. A theoretical and experimental comparative study of several formalisms led us to choose the TSA (Time Safety Automata), extension of the timed automata implemented in the UPPAAL tool. The obtained model is then analysed by model-checking. This methodology allowed the validation of the temporal bounds of the TTA services, i. E. Their worst execution time, under different faults hypotheses. It completes the existent validation processes for TTA, on the one hand the approaches such as test, simulation and fault injection which are not exhaustive, and on the other hand formal approaches (proof of theorems) which did not allow to take into account the temporal bounds or the interaction of the algorithms.
Abstract FR:
Dans le domaine de l’automobile, 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’aspect 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’une 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’architecture 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’outil 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’est à dire leur pire temps d’exécution, sous certaines hypothèses de fautes. Elle complète les processus de validation de TTA existants, d’une part les approches de tests, de simulations et d’injections de fautes qui ne sont pas exhaustives, et d’autre part des approches formelles (preuve de théorème) qui ne permettaient pas de prendre en compte les bornes temporelles ou l’interaction des algorithmes.