Les travaux présentés dans ce mémoire proposent une méthode originale de génération automatique de tests à partir de modèles SysML pour la validation de systèmes embarqués. Un sous-ensemble du langage SysML (appelé SysML4MBT) regroupant les éléments de modélisation pris en compte dans notre approche a été défini et une stratégie de génération de tests dédiée (intitulée ComCover) a été créée. Cette stratégie, basée sur les principes du critère de couverture de modèles bien connu Def-Use, s'intéresse à la couverture des communications (envois / réceptions) au sein du système et entre le système et son environnement.La mise en œuvre opérationnelle d'un prototype, basé sur un générateur de tests à partir de modèle UML, a nécessité la définition de règles de réécriture permettant la transformation du modèle SysML4MBT vers le format d'entrée natif du générateur de tests tout en conservant l'expressivité de SysML4MBT. Finalement, les étapes de concrétisation des tests en scripts exécutables et l'établissement automatique du verdict lors de l'exécution sur banc de test définis durant le projet VETESS permettent l'établissement d'une chaîne outillée opérationnelle de génération et d'exécution automatique de tests à partir de spécifications SysML. Cette chaîne outillée a été étrennée sur plusieurs cas d'étude automobile tels que l'éclairage avant, les essuie-glaces ou la colonne de direction de véhicule. Sur ce dernier exemple, nous avons eu l'opportunité d'exécuter les tests sur un banc de test physique. Ces cas d'étude ont permis de valider chacune des étapes de l'approche proposée. / The work introduced in this thesis is in line with an original SysML Model-Based Testing approach to validate automotive mechatronic systems. A subset of SysML notation (called SysML4MBT) supported to express the test model is defined and a dedicated test generation strategy (called ComCover) is created. This strategy, based on the well-known Def-Use criteria, deals with the coverage of communications (sends / receives) inside the system and between the system and its environment.The development of an operational prototype, based on a UML-based test generator, has required the definition of rewriting rules to derive the input model of the UML test generator from the SysML4MBT model, by preserving the SysML4MBT expressivity.Finally, the concretization of tests in executable scripts and the assignment of a verdict by executing tests on test bench defined during the VETESS project, complete the operational toolchain that allows tests generation and execution from SysML models.This toolchain has been tried out on several automotive case studies as front lightings, wiper or steering column. Concerning this last experimentation, we have had the opportunity to execute test on a physical test bench. These case studies allow validating each step of the proposed approach.

Les travaux présentés dans ce mémoire proposent une méthode originale de génération automatique de tests à partir de modèles SysML pour la validation de systèmes embarqués. Un sous-ensemble du langage SysML (appelé SysML4MBT) regroupant les éléments de modélisation pris en compte dans notre approche a été défini et une stratégie de génération de tests dédiée (intitulée ComCover) a été créée. Cette stratégie, basée sur les principes du critère de couverture de modèles bien connu Def-Use, s'intéresse à la couverture des communications (envois / réceptions) au sein du système et entre le système et son environnement.La mise en œuvre opérationnelle d'un prototype, basé sur un générateur de tests à partir de modèle UML, a nécessité la définition de règles de réécriture permettant la transformation du modèle SysML4MBT vers le format d'entrée natif du générateur de tests tout en conservant l'expressivité de SysML4MBT. Finalement, les étapes de concrétisation des tests en scripts exécutables et l'établissement automatique du verdict lors de l'exécution sur banc de test définis durant le projet VETESS permettent l'établissement d'une chaîne outillée opérationnelle de génération et d'exécution automatique de tests à partir de spécifications SysML. Cette chaîne outillée a été étrennée sur plusieurs cas d'étude automobile tels que l'éclairage avant, les essuie-glaces ou la colonne de direction de véhicule. Sur ce dernier exemple, nous avons eu l'opportunité d'exécuter les tests sur un banc de test physique. Ces cas d'étude ont permis de valider chacune des étapes de l'approche proposée.

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.