Aujourd'hui, les systèmes embarqués sont de plus en plus utilisés pour contrôler les systèmes complexes. Dans ce travail de thèse, nous nous intéressons aux systèmes embarqués critiques utilisés pour la commande de systèmes de transport comme les systèmes ferroviaires. Le but de ce travail est de permettre la conception de systèmes tolérants aux fautes pour le contrôle-commande des systèmes de transport. Nous proposons une nouvelle approche de modélisation des systèmes embarqués temporisés pour le diagnostic de leurs fautes. Elle est basée sur une décomposition structurelle du système et sur une extension de la diagnosticabilité modulaire au contexte des systèmes temporisés. On distingue deux approches de base pour le diagnostic de fautes des SED, une approche basée sur les diagnostiqueurs et une approche basée sur les signatures temporelles causales (STC). La principale limite de l’approche diagnostiqueur réside dans la gestion de l’explosion combinatoire. Dans ce travail, notre verrou principal est de combattre cette limite. Nous proposons une nouvelle méthode basée sur l’ingénierie par les modèles pour le diagnostic des systèmes embarqués critiques. D’autre part, la limite majeure de l’approche STC est la garantie de la cohérence d’une base de STC. Un deuxième niveau de difficulté réside dans l’interprétation des événements en entrée du système de diagnostic dans le cadre de l’hypothèse de défaillances multiples. Dans ce travail, nous proposons deux méthodes différentes pour la vérification de la cohérence d’une base de STC et nous proposons un algorithme d’interprétation basé sur le concept de monde qui garantit la correction du diagnostic / Today, embedded systems are increasingly used to control complex systems. In this thesis, we are interested in critical embedded systems used for the control of transport systems such as railway systems. The aim of this work is to enable the design of fault-tolerant systems for the control of transport systems. We propose a new timed embedded systems modeling approach to diagnose their faults. It is based on decomposition of the system and structural extension of diagnosability context of modular timed systems. In DES, there are two basic approaches for diagnosis: diagnoser based approach and chronicles (Causal Temporal Signature (CTS)) based approach. The major limitation of diagnoser approaches rely in the management of the combinatorial explosion related to the formalism of automata. In this work, our main lock is to combat this limit. We propose new engineering models based method for the diagnosis of critical embedded systems. On the other hand, the major limitation of chronicles approach is first to be able to guaranty the consistency of a database. A second level of difficulty is in interpreting some sequences of events at the input of the diagnostic system under the hypothesis of multiple failures. In this work, we propose two different methods to verify the consistency of a set of CTS and we propose an interpretation algorithm based on a concept of worlds which guarantees the correct diagnosis

Aujourd'hui, les systèmes embarqués sont de plus en plus utilisés pour contrôler les systèmes complexes. Dans ce travail de thèse, nous nous intéressons aux systèmes embarqués critiques utilisés pour la commande de systèmes de transport comme les systèmes ferroviaires. Le but de ce travail est de permettre la conception de systèmes tolérants aux fautes pour le contrôle-commande des systèmes de transport. Nous proposons une nouvelle approche de modélisation des systèmes embarqués temporisés pour le diagnostic de leurs fautes. Elle est basée sur une décomposition structurelle du système et sur une extension de la diagnosticabilité modulaire au contexte des systèmes temporisés. On distingue deux approches de base pour le diagnostic de fautes des SED, une approche basée sur les diagnostiqueurs et une approche basée sur les signatures temporelles causales (STC). La principale limite de l'approche diagnostiqueur réside dans la gestion de l'explosion combinatoire. Dans ce travail, notre verrou principal est de combattre cette limite. Nous proposons une nouvelle méthode basée sur l'ingénierie par les modèles pour le diagnostic des systèmes embarqués critiques. D'autre part, la limite majeure de l'approche STC est la garantie de la cohérence d'une base de STC. Un deuxième niveau de difficulté réside dans l'interprétation des événements en entrée du système de diagnostic dans le cadre de l'hypothèse de défaillances multiples. Dans ce travail, nous proposons deux méthodes différentes pour la vérification de la cohérence d'une base de STC et nous proposons un algorithme d'interprétation basé sur le concept de monde qui garantit la correction du diagnostic

Les travaux de cette thèse contribuent au développement de méthodes automatiques de vérification et de valida-tion de systèmes informatiques, à partir de modèles. Ils sont divisés en deux parties : vérification et générationde tests.Dans la partie vérification, pour le problème du model-checking régulier indécidable en général, deux nouvellestechniques d’approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces. Des sur-approximations de l’ensemble des états accessibles sont calculées, avec l’objectif d’assurer la terminaison del’exploration de l’espace d’états. Les états accessibles (ou des sur-approximations de cet ensemble d’états)sont représentés par des langages réguliers, ou automates d’états finis. La première technique consiste à sur-approximer l’ensemble des états atteignables en fusionnant des états des automates, en fonction de critèressyntaxiques simples, ou d’une combinaison de ces critères. La seconde technique d’approximation consisteaussi à fusionner des états des automates, mais à l’aide de transducteurs. De plus, pour cette seconde technique,nous développons une nouvelle approche pour raffiner les approximations, qui s’inspire du paradigme CEGAR(CounterExample-Guided Abstraction Refinement). Ces propositions ont été expérimentées sur des exemplesde protocoles d’exclusion mutuelle.Dans la partie génération de tests, une technique qui permet de combiner la génération aléatoire avec un critèrede couverture, à partir de modèles algébriques (des grammaires algébriques, des automates à pile) est définie.Générer les tests à partir de ces modèles algébriques (au lieu de le faire à partir de graphes) permet de réduirele degré d’abstraction du modèle et donc de générer moins de tests qui ne sont pas exécutables dans le systèmeréel. Ces propositions ont été expérimentées sur la grammaire de JSON (JAvaScript Object Notation), ainsi quesur des automates à pile correspondant à des appels de fonctions mutuellement récursives, à une requête XPath,et à l’algorithme Shunting-Yard. / The thesis contributes to development of automatic methods for model-based verification and validation ofcomputer systems. It is divided into two parts: verification and test generation.In the verification part, for the problem of regular model checking undecidable in general, two new approxi-mation techniques are defined in order to provide efficient (semi-)algorithms. Over-approximations of the setof reachable states are computed, with the objective of ensuring the termination of the exploration of the statespace. Reachable states (or over-approximations of this set of states) are represented by regular languages or,equivalently, by finite-state automata. The first technique consists in over-approximating the set of reachablestates by merging states of automata, based on simple syntactic criteria, or on a combination of these criteria.The second approximation technique also merges automata states, by using transducers. For the second tech-nique, we develop a new approach to refine approximations, inspired by the CEGAR paradigm (for Counter-Example-Guided Abstraction Refinement). These proposals have been tested on examples of mutual exclusionprotocols.In the test generation part, a technique that combines the random generation with coverage criteria, fromcontext-free models (context-free grammars, pushdown automata) is defined. Generate tests from these mo-dels (instead of doing from graphs) reduces the model abstraction level, and therefore allows having moretests executable in the real system. These proposals have been tested on the JSON grammar (JavaScript ObjectNotation), as well as on pushdown automata of mutually recursive functions, of an XPath query, and of theShunting-Yard algorithm.