Nous nous intéressons aux approches formelles pour le développement de systèmes réactifs critiques. Le langage synchrone Lustre pour la spécification de tels systèmes a subit des évolutions majeurs au cours des dernières années en intégrant dans sa sémantique à base flots de données synchrones des constructions de plus haut-niveau appelées automates de modes (dans le langage Scade 6). Ceux-ci mettent en œuvre l’activation de modes de calculs en fonction des états et des transitions de l’automate, et reposent pour cela sur la sémantique des horloges du langage Lustre. En particulier, nous étudiions la prise en compte des horloges et des automates de modes dans l’outil de génération de tests GATeL dédié à l’origine au langage Lustre mono-horloge (flots de données purs). GATeL génère automatiquement des séquences de tests pour un modèle à partir d’un objectif de test décrit en Lustre à travers une exploration en arrière des dépendances entre flots et selon des teniques de résolution de contraintes. Nous présentons ces différents domaines et la mise en oeuvre des modifications apportées à l’outil pour prendre en compte les automates de modes. Enfin, nous définissons des critères de couverture structurelle pour les automates de modes et montrons alors comment, en les traduisant de manière automatique sous forme d’objectifs de tests, GATeL permet de générer des séquences couvrant ces critères. / Lustre is a synchronous dataflow-oriented language for the specification of reactive systems. Since its definition, it has been extended to support mode automata, a formalism in which computation modes are activated according to an extended state-machine. The semantics of mode-automata is heavily based on an appropriate use of the clock sampling features of Lustre. We present the modifications made in GATeL, an automatic test sequences generator originally designed for a mono-rate subset of Lustre. GATeL performs a lazy goal-oriented test sequences generation, based on constraint logic programming. We modify it so that it can handle the temporal constraints of clocks internally and efficiently generate tests sequences from state-maines specifications. We also present some existing structural test criteria for state-machines and adapt them to the specific case of mode-automata.

Les travaux présentés dans cette thèse sont effectuées dans le cadre des Systèmes sur puce (SoC, Systemon Chip) et la conception de systèmes embarqués en temps réel, notamment dédiés au domaine de la reconfiguration dynamique, liés à ces systèmes complexes. Dans ce travail, nous présentons un nouveau flot de conception basé sur l'Ingénierie Dirigée par les Modèles (IDM/MDE) et le profilMARTE pour la conception conjointe du SoC, la spécification et la mise en oeuvre de ces systèmes sur puce reconfigurables, afin d'élever les niveaux d'abstraction et de réduire la complexité du système. La première contribution relative à cette thèse est l'identification des parties de systèmes sur puce reconfigurable dynamiquement qui peuvent être modélisées au niveau d'abstraction élevé. Cette thèse adapte une approche dirigée par l'application et cible les modèles d'application de haut niveau pour être traités comme des régions dynamiques des SoCs reconfigurables. Nous proposons aussi des modèles de contrôle générique pour la gestion de ces régions au cours de l'exécution en temps réel. Bien que cette sémantique puisse être introduite à différents niveaux d'abstraction d'un environnent pour la conception conjointe du SoC, nous insistons tout particulièrement sur sa fusion au niveau du déploiement, qui relie la propriété intellectuelle avec les éléments modélisés à haut niveau de conception. En outre, ces concepts ont été intégrés dans le méta-modèleMARTE et le profil correspondant afin de fournir une extension adéquate pour exprimer les caractéristiques de reconfiguration à la modélisation de haut niveau. La seconde contribution est la proposition d'un méta-modèle intermédiaire, qui isole les concepts présents au niveau transfert de registre (RTL-Register Transfer Level). Ce méta-modèle intègre les concepts chargés de l'exécution matérielle des applications modélisées, tout en enrichissant la sémantique de contrôle, provoquant la création d'un accélérateur matériel reconfigurable dynamiquement avec plusieurs implémentations disponibles. Enfin, en utilisant les transformations de modèlesMDE et les principes correspondants, nous sommes en mesure de générer des codeHDL équivalents à différentes implémentations de l'accélérateur reconfigurable ainsi que différents codes source en langage C/C++ liés au contrôleur de reconfiguration, qui est finalement responsable de la commutation entre les différentes mplémentations. Enfin, notre flot de conception a été vérifié avec succès dans une étude de cas liée à un système anti-radar de détection de collision. Une composante clé intégrante de ce système a été modélisée en utilisant les spécifications MARTE étendu et le code généré a été utilisé dans la conception et la mise en oeuvre d'un SoC sur un FPGA reconfigurable dynamiquement.