Dans cette thèse, nous proposons d'étudier le débogage interactif d'applications pour les systèmes embarqués MPSoC (Multi-Processor System on Chip). Une étude de l'art a montrée que la conception et le développement de ces applications reposent de plus en plus souvent sur des modèles de programmation et des frameworks de développement. Ces environnements définissent les bonnes pratiques, tant au niveau algorithmique qu'au niveau des techniques de programmation. Ils améliorent ainsi le cycle de développement des applications destinées aux processeurs MPSoC. L'utilisation de modèles de programmation ne garantit cependant pas que les codes pourront etre exécutés sans erreur, en particulier dans le cas de la programmation dynamique, oú ils offrent très peu d'aide à la vérification. Notre contribution pour résoudre ces challenges consiste en une nouvelle approche pour le débogage interactif, appelée Programming Model-Centric Debugging, ainsi qu'une implémentation d'un prototype de débogueur. Le débogage centré sur les modèles rapproche le débogage interactif du niveau d'abstraction fourni par les modèles de programmation, en capturant et interprétant les événements générés pendant l'exécution de l'application. Nous avons appliqué cette approche sur trois modèles de programmation, basés sur les composants logiciels, le dataflow et la programmation d'accélérateur par kernels. Ensuite, nous détaillons comment nous avons développé notre prototype de débogueur, basé sur GDB, pour la programmation de la plate-forme STHORM de STMicroelectronics. Nous montrons aussi comment aborder le débogage basé sur les modèles avec quatre études de cas~: un code de réalité augmentée construit à l'aide de composants, une implémentation dataflow d'un décodeur vidéo H.264 and deux applications de calcul scientifique.

L’approche synchrone aux systèmes réactifs, où le temps global est une séquence d’instants discrets, a été proposée afin de faciliter la conception des systèmes embarqués critiques. Des systèmes synchrones sont souvent réalisés sur des architectures asynchrones pour des raisons de performance ou de contraintes physiques de l’application. Une répartition d’un système synchrone sur une architecture asynchrone nécessite des protocoles de communication et de synchronisation pour préserver la sémantique synchrone. En pratique, les protocoles peut avoir un coût important qui peut entrer en conflit avec les contraintes de l’application comme, par exemple, la taille de mémoire disponible, le temps de réaction, ou le débit global.L’approche quasi-synchrone utilise des composants synchrones avec des horloges indépendantes. Les composants communiquent par échantillonnage de mémoire partagée ou par des tampons FIFO. On peut exécuter un tel système de façon synchrone, où toutes les horloges avancent simultanément, ou de façon asynchrone avec moins de contraintes sur les horloges, sans ajouter des protocoles .Plus les contraintes sont relâchées, plus de comportements se rajoutent en fonction de l’entrelacement des tics des horloges. Dans le cas de systèmes flots de données, un comportement est différent d’un autre si les valeurs ou le cadencement ont changé. Pour certaines classes de systèmes l’occurrence des déviations est acceptable, tant que la fréquence de ces événements reste bornée.Nous considérons des limites dures sur la fréquence des déviations avec ce que nous appelons les exigences faiblement dures, par exemple, le nombre maximal d’éléments divergents d’un flot par un nombre d’éléments consécutifs.Nous introduisons des limites de dérive sur les apparitions relatives des paires d’événements récurrents comme les tics d’une horloge, l’occurrence d’une différence,ou l’arrivée d’un message. Les limites de dérive expriment des contraintes entre les horloges, par exemple, une borne supérieure de deux tics d’une horloge entre trois tics consécutifs d’une autre horloge. Les limites permettent également de caractériser les exigences faiblement dures. Cette thèse présente des analyses pour la vérification et l’inférence des exigences faiblement dures pour des programmes de flots de données synchrones étendu avec de la communication asynchrone par l’échantillonnage de mémoire partagée où les horloges sont décrites par des limites de dérive. Nous proposons aussi une analyse de performance des systèmes répartis avec de la communication par tampons FIFO, en utilisant les limites de dérive comme abstraction. / The synchronous approach to reactive systems, where time evolves by globally synchronized discrete steps, has proven successful for the design of safetycriticalembedded systems. Synchronous systems are often distributed overasynchronous architectures for reasons of performance or physical constraintsof the application. Such distributions typically require communication and synchronizationprotocols to preserve the synchronous semantics. In practice, protocolsoften have a significant overhead that may conflict with design constraintssuch as maximum available buffer space, minimum reaction time, and robustness.The quasi-synchronous approach considers independently clocked, synchronouscomponents that interact via communication-by-sampling or FIFO channels. Insuch systems we can move from total synchrony, where all clocks tick simultaneously,to global asynchrony by relaxing constraints on the clocks and withoutadditional protocols. Relaxing the constraints adds different behaviors dependingon the interleavings of clock ticks. In the case of data-flow systems, onebehavior is different from another when the values and timing of items in a flowof one behavior differ from the values and timing of items in the same flow ofthe other behavior. In many systems, such as distributed control systems, theoccasional difference is acceptable as long as the frequency of such differencesis bounded. We suppose hard bounds on the frequency of deviating items in aflow with, what we call, weakly-hard requirements, e.g., the maximum numberdeviations out of a given number of consecutive items.We define relative drift bounds on pairs of recurring events such as clockticks, the occurrence of a difference or the arrival of a message. Drift boundsexpress constraints on the stability of clocks, e.g., at least two ticks of one perthree consecutive ticks of the other. Drift bounds also describe weakly-hardrequirements. This thesis presents analyses to verify weakly-hard requirementsand infer weakly-hard properties of basic synchronous data-flow programs withasynchronous communication-by-sampling when executed with clocks describedby drift bounds. Moreover, we use drift bounds as an abstraction in a performanceanalysis of stream processing systems based on FIFO-channels.

Dans la conception basée sur des modèles on construit un modèle mathématique du système que l'on utilise pour concevoir le système de sorte qu'il présente les propriétés souhaitées. Pour les systèmes de sûreté critique, il peut être d'une importance capitale de vérifier ces propriétés de sûreté sur le modèle, par exemple, pour tenir compte des variations des paramètres. Le calcul d'un nombre fini de comportements du système par le biais de simulation ne suffit pas à garantir des propriétés de sécurité. Avec une analyse d'atteignabilité on peut calculer une couverture de tous les comportements possibles du système, possiblement infinis. Cette analyse peut prendre en compte de non-déterminisme dans le modèle et peut garantir des propriétés de sécurité. Les systèmes d'intérêt présentent souvent à la fois un comportement continu et discret et de tels systèmes sont appelés systèmes hybrides. Le calcul d'atteignabilité est considéré comme difficile pour les systèmes continus et hybrides. Ce n'est que récemment que des méthodes pour le calcul d'accessibilité ont été développées qui peuvent être mis à l'échèlle. Ils sont basés sur des représentations implicites d'ensembles continus à l'aide du concepte mathématique de la fonction de support. Dans cette thèse, nous développons un outil extensible appelé SpaceEx pour le calcul d'atteignabilité des systèmes hybrides. Deux algorithmes d'atteignabilité ont été mis en œuvre dans SpaceEx, l'un basé sur l'outil PHAVer pour les automates linéaires hybrides et l'autre basé sur les fonctions de support pour les dynamiques affines par morceaux. L'algorithme de fonction support a été mis au point et sa mise à l'échelle a été amélioré en basculant entre différentes représentations d'ensembles continus. Nous proposons un algorithme de calcul d'image des transition discrètes amélioré qui réduit l'erreur de sur-approximation et nous illustrons sa précision et son efficacité avec plusieurs études de cas.

Dans la conception basée sur des modèles on construit un modèle mathématique du système que l'on utilise pour concevoir le système de sorte qu'il présente les propriétés souhaitées. Pour les systèmes de sûreté critique, il peut être d'une importance capitale de vérifier ces propriétés de sûreté sur le modèle, par exemple, pour tenir compte des variations des paramètres. Le calcul d'un nombre fini de comportements du système par le biais de simulation ne suffit pas à garantir des propriétés de sécurité. Avec une analyse d'atteignabilité on peut calculer une couverture de tous les comportements possibles du système, possiblement infinis. Cette analyse peut prendre en compte de non-déterminisme dans le modèle et peut garantir des propriétés de sécurité. Les systèmes d'intérêt présentent souvent à la fois un comportement continu et discret et de tels systèmes sont appelés systèmes hybrides. Le calcul d'atteignabilité est considéré comme difficile pour les systèmes continus et hybrides. Ce n'est que récemment que des méthodes pour le calcul d'accessibilité ont été développées qui peuvent être mis à l'échèlle. Ils sont basés sur des représentations implicites d'ensembles continus à l'aide du concepte mathématique de la fonction de support. Dans cette thèse, nous développons un outil extensible appelé SpaceEx pour le calcul d'atteignabilité des systèmes hybrides. Deux algorithmes d'atteignabilité ont été mis en œuvre dans SpaceEx, l'un basé sur l'outil PHAVer pour les automates linéaires hybrides et l'autre basé sur les fonctions de support pour les dynamiques affines par morceaux. L'algorithme de fonction support a été mis au point et sa mise à l'échelle a été amélioré en basculant entre différentes représentations d'ensembles continus. Nous proposons un algorithme de calcul d'image des transition discrètes amélioré qui réduit l'erreur de sur-approximation et nous illustrons sa précision et son efficacité avec plusieurs études de cas. / In model based design, one constructs a mathematical model of the system and uses it to design the system so that it exhibits the desired properties. For safety critical systems, it can be of utmost importance to verify these safety properties on the model, e.g., to account for parameter variations. Computing a finite number of system behaviors via simulation is not sufficient to guarantee safety properties. With a reachability analysis one can compute a cover of all possible system behaviors, potentially infinite, accounting for any non-determinism in the model, and with which one can guarantee safety properties. Systems of interest often exhibit both continuous and discrete behavior and such systems are called hybrid systems. Reachability computation is considered hard for continuous and hybrid systems. Only recently, scalable methods for reachability computation have been developed based on implicit set representations using the mathematical construct of support functions. In this thesis, we develop an extendable tool called SpaceEx for reachability of hybrid systems. Two reachability algorithms have been implemented in SpaceEx, one based on the PHAVer tool for linear hybrid automata and the other based on support functions for piecewise affine dynamics. The support function based algorithm has been tuned and its scalability has been improved by switching set representations. We propose an improved image computation algorithm for discrete transition that further reduces the over-approximation error and illustrate its accuracy and efficiency with several case studies.

Les applications temps réel durs sont celles qui doivent exécuter en respectant des contraintes temporelles. L'ordonnancement temps réel a bien été étudié sur mono-processeurs depuis plusieurs années. Récemment, l'utilisation d'architectures multiprocesseurs a augmenté dans les applications industrielles et des architectures parallèles sont proposées pour que le logiciel devienne compatible avec ces plateformes. L'ordonnancement multiprocesseurs de tâches parallèles dépendantes n'est pas une simple généralisation du cas mono-processeur et la problématique d'ordonnancement devient plus complexe et difficile.
Dans cette thèse, nous étudions le problème d'ordonnancement temps réel de graphes de tâches parallèles acycliques sur des plateformes multiprocesseurs. Dans ce modèle, un graphe est composé d'un ensemble de sous-tâches dépendantes sous contraintes de précédence qui expriment les relations de précédences entre les sous-tâches. L'ordre d'exécution des sous-tâches est dynamique, c'est-à-dire que les sous-tâches peuvent s'exécuter en parallèle ou séquentiellement par rapport aux décisions de l'ordonnanceur temps réel. Pour traiter les contraintes de précédence, nous proposons deux méthodes pour l'ordonnancement des graphes : par transformation du modèle de graphe de sous tâches parallèles en un modèle de tâches séquentielles indépendantes, plus simple à ordonnancer et par ordonnancement direct des graphes en prenant en compte les relations de dépendance entre les sous-tâches. Nous proposons un ordonnancement des graphes en prenant directement en compte les paramètres temporels des graphes et un ordonnancement au niveau des sous-tâches, par rapport à des paramètres temporels attribués aux sous-tâches par un algorithme spécifique.
Enfin, nous prouvons que les deux méthodes d'ordonnancement de graphes ne sont pas comparables. Nous fournissons alors des résultats de simulation pour comparer ces méthodes en utilisant les algorithmes d'ordonnancement globaux EDF et DM. Nous avons développé un logiciel nommé YARTISS pour générer des graphes aléatoires et réaliser les simulations / The interest for multiprocessor systems has recently been increased in industrial applications, and parallel programming API's have been introduced to benefit from new processing capabilities. The use of multiprocessors for real-time systems, whose execution is performed based on certain temporal constraints is now investigated by the industry. Real-time scheduling problem becomes more complex and challenging in that context. In multiprocessor systems, a hard real-time scheduler is responsible for allocating ready jobs to available processors of the systems while respecting their timing parameters.
In this thesis, we study the problem of real-time scheduling of parallel Directed Acyclic Graph (DAG) tasks on homogeneous multiprocessor systems. In this model, a DAG task consists of a set of subtasks that execute under precedence constraints. At all times, the real-time scheduler is responsible for determining how subtasks execute, either sequentially or in parallel, based on the available processors of the system. We propose two DAG scheduling approaches to determine the execution form of DAG tasks. The first approach is the DAG Stretching algorithm, from the Model Transformation approach, which forces DAG tasks to execute as sequentially as possible. The second approach is the Direct Scheduling, which aims at scheduling DAG tasks while respecting their internal dependencies. We provide real-time schedulability analyses for Direct Scheduling at DAG-Level and at Subtask-Level.
Due to the incomparability of DAG scheduling approaches, we use extensive simulations to compare performance of global EDF with global DM scheduling using our simulation tool YARTISS

Le travail décrit dans cette thèse fait partie d'un effort de recherche au laboratoire VERIMAG pour créer une chaîne d'outils basée sur modèles (model-based) pour la conception et l'implantation des systèmes embarquées. Nous utilisons une approche en trois couches, qui séparent le niveau d'application du niveau implantation/architecture. L'application est décrite dans un langage de haut niveau qui est indépendante des détails d'implantation. L'application est ensuite transférée à l'architecture d'exécution en utilisant des techniques spécifiques pour que les propriétés demandées soient bien préservées.<br />Dans cette thèse, l'application est décrite en Simulink/Stateflow, un langage de modélisation très répandu dans le milieu de l'industrie, comme celui de l'automobile. Au niveau de l'architecture, nous considérons des implantation sur une plate-forme "mono-processeur" et "multi-tâches". Multi-tâches signifie que l'application est répartie en un nombre des tâches qui sont ordonnées par un système d'exploitation temps-réel (RTOS) en fonction d'une politique d'ordonnancement préemptive comme par exemple la priorité statique (static-priority SP) ou la date-limite la plus proche en priorité (earliest deadline first EDF).<br />Entre ces deux couches, on rajoute une couche de représentation intermédiaire basée sur le langage de programmation synchrone Lustre, développé à VERIMAG durant les 25 dernières années. Cette représentation intermédiaire permet de profiter des nombreux outils également développés à VERIMAG tels que des simulateurs, des générateurs de tests, des outils de vérification et des générateurs de code.<br />Dans la première partie de cette thèse, on étudie comment réaliser une traduction automatique de modèle Simulink/Stateflow en modèles Lustre. Coté Simulink, le problème est relativement simple mais nécessite néanmoins l'utilisation d'algorithmes sophistiqués pour inférer correctement les informations de temps et de types (de signaux) avant de générer les variables correspondantes dans le programme Lustre. La traduction de Stateflow est plus difficile à cause d'un certain nombre de raisons ; d'abord Stateflow présent un certain nombre de comportements "non-sûr" tels que la non-terminaison d'un cycle synchrone ou des sémantiques qui dépendent de la disposition graphique des composants sur un modèle. De plus Stateflow est un langage impératif, tandis que Lustre un langage de flots de données. Pour le premier problème nous proposons un ensemble de conditions vérifiables statiquement servant à définir un sous-ensemble "sûr" de Stateflow. Pour le deuxième type de problèmes nous proposons un ensemble de techniques pour encoder des automates et du code séquentiel en équations de flots de données.<br />Dans la deuxième partie de la thèse, on étudie le problème de l'implantation de programmes synchrones dans l'architecture mono-processeur et multi-tâche décrite plus haut. Ici, l'aspect le plus important est comment implanter les communications entre tâches de manière à ce que la sémantique synchrone du système soit préservée. Des implantations standards, utilisant des buffers de taille un, protégés par des sémaphores pour assurer l'atomicité, ou d'autres protocoles "lock-free" proposés dans la littérature ne préservent pas la sémantique synchrone. Nous proposons un nouveau schéma de buffers, qui préserve la sémantique synchrone tout en étant également "lock-free". Nous montrons de plus que ce schéma est optimal en terme d'utilisation des buffers.