Les travaux présentés dans cette thèse s’inscrivent dans le cadre du développement logiciel des systèmes temps réel embarqués. Nous définissons dans ce travail une méthodologie nommée DRIM. Cette méthodologie permet de guider le déploiement des applications temps réel sur différents RTOS en suivant la ligne de l’IDM et en assurant le respect des contraintes de temps après le déploiement. L’automatisation de la méthodologie DRIM montre sa capacité à détecter les descriptions non-implémentables de l’application, réalisées au niveau conception, pour un RTOS donné, ce qui présente l’avantage de réduire le temps de mise sur le marché d’une part et de guider l’utilisateur pour un choix approprié de l’RTOS cible d’autre part. / The main purpose of this Phd is to contribute to the software development of real-time embedded systems. We define in this work a methodology named DRIM: Design Refinement toward Implementation Methodology. This methodology aims to guide the deployment of a real-time application on to different RTOS while respecting MDE principals and ensuing that the timing properties are still met after deployment. The automation of DRIM shows its ability to detect non-implementable design models describing the real-time application, on aparticular RTOS, which permits to reduce the time-to-market on the one hand and guide the user to the selection of the appropriate RTOS from the other hand.

Ces dernières années, les appareils photos/vidéos numériques grand public sont devenus omniprésents. On peut aujourd'hui trouver des systèmes de captures d'images dans toutes sortes d'appareils numériques comme les téléphones portables, les assistants personnels numériques etc. Malgré une augmentation croissante de la puissance et de la complexité de ces appareils, laqualité de la chaîne de capture d'image, composée du couple système optique/capteur est toujours contrainte à des limitations d'espace et de coût. Les défauts introduits sont nombreuxet dégradent considérablement la qualité des images produites : flou, déformations géométriques, artefacts de couleurs, effets de moire, bruits statiques et dynamiques, etc. Une idée intéressante est de corriger ces défauts de manière algorithmique en utilisant la puissance toujours croissante des architectures de traitements. Dans cette thèse nous nous intéressons particulièrement à deux problèmes issues de l'acquisition de l'image par le capteur : le dématriçage de la matrice de Bayer et la réduction du bruit. Dans la première partie, nous décrivons la structure générale de la chaîne de capture d'image dans les appareils photos/vidéos numériques. Nous présentons le rôle, le fonctionnement et les défauts introduits par chacun de ses éléments. Enfin, nous illustrons comment ces défauts peuvent être corriges par des traitements algorithmiques. Dans la deuxième partie, nous montrons comment l'information de couleur est introduite dans les capteurs numériques. Nous présentons ensuite un état de l'art des algorithmes de dématriçage. Un nouvel algorithme de reconstruction de la matrice de Bayer base sur le principe de l'interpolation directionnelle est propose. Il permet d'associer une qualité d'image produite sans artefacts avec une faible complexité de calculs. Pour mieux comprendre les comportements du bruit dans les capteurs numériques, nous énumérons ses différentes sources et leurs dépendances par rapport aux conditions de prises de vues. Apres avoir présenté l'état de l'art des méthodes de restauration des images bruitées, nous nous intéressons particulièrement aux algorithmes de débruitage à voisinage local et plus précisément au filtre bilatéral. Nous proposons un filtre bilatéral pour la mosaïque de Bayer, adaptatif en fonction de la puissance du bruit dans les images. Dans la troisième partie, nous présentons l'implémentation, l'optimisation et la simulation de l'exécution des algorithmes de dématriçage et de réduction du bruit proposes. La plateforme d'implémentation est le processeur TriMedia TM3270 de NXP semiconductors. Nous montrons que nous arrivons à traiter des images de taille 5 méga-pixels en moins de 0,5 secondes et des images de résolution VGA à une cadence supérieure à 25 images par seconde. Finalement, pour des raisons de standardisation, de rapidité d'exécution et de consommation d'énergie, nous avons conçu une architecture dédiée à l'algorithme de dématriçage propose. Cette architecture permet de multiplier par 10 la rapidité d'exécution obtenue sur le processeur TriMedia TM3270

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cités ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la litérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WTmu. La logique WTmu est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WTmu. Nous identifions un fragment de WTmu appelé WTmu pour le contrôle (C-WTmu). Nous proposons un algorithme qui permet de vérifier si une formule de C-WTmu possède un modèle. Cet algorithme n'a pas besoin de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. En utilisant C-WTmu comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contrôleurs.

.

Cette thèse s'intéresse à l'allocation de ressources des réseaux WMAN (Wireless Metropolitan Area Networks) utilisant l'OFDMA (Orthogonal Frequency Division Multiple Access). Les applications récentes destinées aux réseaux sans fils requièrent des débits importants. L'OFDMA, technique d'accès multiple basée sur l'OFDM(Orthogonal Frequency Division Multiplexing), permet d'obtenir des débits élevés en tirant avantage de la diversité multiutilisateur. Dans une première partie, l'allocation de ressources est considérée au niveau de la couche physique (affectation des fréquences et de la puissance). Dans un contexte monocellulaire, un algorithme est proposé afin de maximiser le débit de la cellule tout en assurant des débits individuels aux utilisateurs (problème RA, Rate Adaptive optimization). L'impact de la sous canalisation sur le débit global est analysé. Puis, un algorithme est proposé dans un contexte multicellulaire pour adapter dynamiquement le facteur de réutilisation fréquentiel. Dans une deuxième partie, l'ordonnancement est traité. L'objectif est de garantir les délais du trafic temps réel, de maximiser le débit du trafic non temps réel tout en assurant une équité proportionnelle entre les flux. Pour cela, les extensions du GPS (Global Processor Sharing) sont étudiées. Deux algorithmes, extensions du WFS (Wireless Fair Service) pour l'OFDMA, sont proposés. Leurs performances sont comparées au WFS et aux algorithmes existants en OFDMA. L'une des propositions, l'OWFS (Opportunist Wireless Fair Service) est particulièrement adaptée pour maximiser le débit du trafic non temps réel et comporte un paramètre, le poids de délai, qui permet de maintenir un taux de pertes acceptable pour le trafic temps réel.

L'étude réalisée dans cette thèse s'est portée sur un concept original de microréseau et son<br />utilisation pour faciliter l'intégration des systèmes à base d'énergies renouvelables (EnR)<br />dans le réseau. Ce microréseau est constitué des générateurs à base d'EnR ainsi que de<br />systèmes de soutien qui incorporent des fonctionnalités additionnelles de façon à en améliorer<br />l'intégration. Sur la base de ce concept proposé, deux différentes applications types de<br />microréseaux on été étudiées en détail : un microréseau résidentiel ilôtable et un parc éolien<br />muni de systèmes DFACTS (STATCOM et DVR). Dans les deux applications, des structures<br />de contrôle/commande à différents niveaux et appliquées aux différents composants du<br />microréseau ont été développées, analysées en simulation off line et finalement validées sur<br />un banc expérimental hybride temps réel avec des prototypes à échelle réduite.

Les systèmes embarqués temps réel critiques intègrent des architectures complexes qui évoluent constamment a n d'intégrer des nouvelles fonctionnalités requises par les utilisateurs naux des systèmes (automobile, avionique, ferroviaire, etc.). Ces nouvelles architectures ont un impact direct sur la variabilité du comportement temporel des systèmes temps réel. Cette variabilité entraîne un sur-approvisionnement important si la conception du système est uniquement basée sur le raisonnement pire cas. Approches probabilistes proposent des solutions basées sur la probabilité d'occurrence des valeurs les plus défavorables a n d'éviter le sur-approvisionnement, tout en satisfaisant les contraintes temps réel. Les principaux objectifs de ce travail sont de proposer des nouvelles techniques d'analyse des systèmes temps réel probabilistes et des moyens de diminuer la complexité de ces analyses, ainsi que de proposer des algorithmes optimaux d'ordonnancement á priorité xe pour les systèmes avec des temps d'exécution décrits par des variables aléatoires. Les résultats que nous présentons dans ce travail ont été prouvés surs et á utiliser pour les systèmes temps réel durs, qui sont l'objet principal de notre travail. Notre analyse des systèmes avec plusieurs paramètres probabilistes a été démontrée considérablement moins pessimiste que d'autres types d'analyses. Cette analyse combinée avec des algorithmes d'ordonnancement optimaux appropriées pour les systèmes temps réel probabilistes peut aider les concepteurs de systèmes á mieux apprécier la faisabilité d'un systéme, en particulier de ceux qui sont jugé irréalisable par des analyses/algorithmes d'ordonnancement déterministes.

Les techniques formelles de la famille « vérification de modèles » (« model checking ») se heurtent au problème de l’explosion combinatoire. Ceci limite les perspectives d’exploitation dans des projets industriels. Ce problème est provoqué par la combinatoire dans la construction de l’espace des états possibles durant l’exécution des systèmes modélisés. Le nombre d’états pour des modèles de systèmes industriels réalistes dépasse régulièrement les capacités des ressources disponibles en calcul et stockage. Cette thèse défend l’idée qu’il est possible de réduire cette combinatoire en spécialisant les outils pour des familles de propriétés. Elle propose puis valide expérimentalement un ensemble de méthodes pour le développement de ce type d’outils en suivant une approche guidée par les propriétés appliquée au contexte temps réel. Il s’agit donc de construire des outils d’analyse performants pour des propriétés temps réel qui soient exploitables pour des modèles industriels de taille réaliste. Les langages considérés sont, d’une part UML étendu par le profil MARTE pour la modélisation par les utilisateurs, et d’autre part les réseaux de Petri temporisés comme support pour la vérification. Les propositions sont validées sur un cas d’étude industriel réaliste issu du monde avionique : l’étude de la latence et la fraicheur des données dans un système de gestion des alarmes exploitant les technologies d’Avionique Modulaire Intégrée. Ces propositions ont été mise en oeuvre comme une boite à outils qui intègre les cinq contributions suivantes: la définition de la sémantique d’exécution spécifiques aux propriétés temps réel pour les modèles d’architecture et de comportement spécifiés en UML/MARTE; la spécification des exigences temps réel en s’appuyant sur un ensemble de patrons de vérification atomiques dédiés aux propriété temps réel; une méthode itérative d’analyse à base d’observateurs pour des réseaux de Petri temporisés; des techniques de réduction de l’espace d’états spécifiques aux propriétés temps réel pour des Réseaux de Petri temporisés; une approche pour l’analyse des erreurs détectées par « vérification des modèles » en s’appuyant sur des idées inspirées de la « fouille de données » (« data mining »). / Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Ces dernières années, les appareils photos/vidéos numériques grand public sont devenus omniprésents. On peut aujourd’hui trouver des systèmes de captures d’images dans toutes sortes d’appareils numériques comme les téléphones portables, les assistants personnels numériques etc. Malgré une augmentation croissante de la puissance et de la complexité de ces appareils, laqualité de la chaîne de capture d’image, composée du couple système optique/capteur est toujours contrainte à des limitations d’espace et de coût. Les défauts introduits sont nombreuxet dégradent considérablement la qualité des images produites : flou, déformations géométriques, artefacts de couleurs, effets de moire, bruits statiques et dynamiques, etc. Une idée intéressante est de corriger ces défauts de manière algorithmique en utilisant la puissance toujours croissante des architectures de traitements. Dans cette thèse nous nous intéressons particulièrement à deux problèmes issues de l’acquisition de l’image par le capteur : le dématriçage de la matrice de Bayer et la réduction du bruit. Dans la première partie, nous décrivons la structure générale de la chaîne de capture d’image dans les appareils photos/vidéos numériques. Nous présentons le rôle, le fonctionnement et les défauts introduits par chacun de ses éléments. Enfin, nous illustrons comment ces défauts peuvent être corriges par des traitements algorithmiques. Dans la deuxième partie, nous montrons comment l’information de couleur est introduite dans les capteurs numériques. Nous présentons ensuite un état de l’art des algorithmes de dématriçage. Un nouvel algorithme de reconstruction de la matrice de Bayer base sur le principe de l’interpolation directionnelle est propose. Il permet d’associer une qualité d’image produite sans artefacts avec une faible complexité de calculs. Pour mieux comprendre les comportements du bruit dans les capteurs numériques, nous énumérons ses différentes sources et leurs dépendances par rapport aux conditions de prises de vues. Apres avoir présenté l’état de l’art des méthodes de restauration des images bruitées, nous nous intéressons particulièrement aux algorithmes de débruitage à voisinage local et plus précisément au filtre bilatéral. Nous proposons un filtre bilatéral pour la mosaïque de Bayer, adaptatif en fonction de la puissance du bruit dans les images. Dans la troisième partie, nous présentons l’implémentation, l’optimisation et la simulation de l’exécution des algorithmes de dématriçage et de réduction du bruit proposes. La plateforme d’implémentation est le processeur TriMedia TM3270 de NXP semiconductors. Nous montrons que nous arrivons à traiter des images de taille 5 méga-pixels en moins de 0,5 secondes et des images de résolution VGA à une cadence supérieure à 25 images par seconde. Finalement, pour des raisons de standardisation, de rapidité d’exécution et de consommation d’énergie, nous avons conçu une architecture dédiée à l’algorithme de dématriçage propose. Cette architecture permet de multiplier par 10 la rapidité d’exécution obtenue sur le processeur TriMedia TM3270 / Digital cameras are now present everywhere. They are commonly included in portable digital devices such as mobile phones and personal digital assistants. In spite of constant improvements in terms of computing power and complexity, the digital imaging chain quality, including sensor and lenses system, is still limited by space and cost constraints. An important number of degradations are introduced by this chain that significantly decrease overall image quality : including blurring effects, geometric distortions, color artefacts, moiré effects, static and dynamic noise. Correcting these defects in an algorithmic way, using the increasing power of embedded processing architecture present in mobile phones and PDAs may appear like an interesting solution. In this thesis we are especially interested in reducing two major defects of the sensor acquisition chain : Bayer matrix demosaicing artefacts and photon noise. In the first part, we describe the general imaging chain commonly used in digital cameras and video devices. We show the function, the inner working and the defects introduced by each of its elements. Finally we exhibit possible ways to correct these defects using algorithmic solutions. In the second part, we introduce the principle of Bayer demosaicing. We present the state of the art and we propose a new method based on a directed interpolation principle. Our method yields a good image quality while retaining a low computational complexity. We then enumerate several noise sources present in imaging digital sensors and their dependencies with imaging conditions. We are particularly interested in local algorithms and more specifically in the bilateral filter. After presenting the state of the art in denoising algorithm, we propose a new adaptive bilateral filter for sensor colour mosaic denoising. In the third part, we present the implementation, the optimization and the execution simulation of the proposed demosaicing and denoising algorithms. The implementation target is the TM3270 TriMedia processor from NXP Semiconductors. We show that it is possible to process 5 megapixels images in less than 0.5 seconds and more than 25 images per second at VGA resolution. Finally, for standardization, execution speed and power consumption reasons, we describe a dedicated architecture for our proposed demosaicing algorithm. This architecture improves the execution speed by a factor of 10 compared to the TriMedia TM3270 processor

Le présent mémoire porte sur l'animation passive de phénomènes naturels. L'animation est dite passive lorsque qu'elle [i.e. lorsqu'elle] est directe et sans contrôle ou sans dynamique inverse. En particulier, le type de phénomènes naturels traités est celui des phénomènes gazeux et plus précisément, ceux modélisés par un fluide à phase unique. Tout d'abord, le domaine de l'animation de fluide synthétisé par la simulation d'un modèle physique sera introduit ainsi que la problématique abordée.Le document comprend trois contributions abordant la problématique à différents niveaux. Dans le premier ouvrage, on retrouve une méthode permettant de résoudre les équations de Navier-Stokes en une seule itération sur le GPU (Graphical Processing Unit). La méthode est si simple qu'elle a pu être implémentée en moins d'une journée de travail dans Fx-Composer (vidéo : http: //www.youtube.com/watch?v=PScfTOKbSpU). En plus d'être extrêmement rapide sur le GPU, cette méthode rend l'animation de fluide beaucoup plus accessible et peut être utilisée à différentes fins : l'initiation à l'animation de fluide à l'aide d'une méthode simple à implémenter ou l'ajout rapide d'effets visuels dans un jeu vidéo ou autre application interactive. La deuxième contribution aborde le problème au niveau de la visualisation du fluide. On y retrouve l'élaboration d'une méthode explicite et inconditionnellement stable pour la résolution numérique de l'équation de convection-diffusion utilisée pour simuler la densité d'un gaz qui à la fois est diffusé et transporté dans le domaine par un champ de vecteurs-vitesse, qui dans notre cas représente le mouvement d'un fluide.Le troisième article aborde le problème au niveau de la complexité calculatoire et réduit l'animation 3D de feu à une utilisation 2D strictement en espace-écran. La complexité d'une animation en espace-écran est constante pour une résolution d'image donnée puisque les calculs se font uniquement sur les pixels de l'écran (ou une sur une sous-résolution de ceux-ci).