Les systèmes d'énergie électrique embarqués ou semi autonomes connaissent des évolutions marquées. Parmi elles, on peut citer l'introduction massive d'électronique de puissance permettant d'améliorer significativement les performances via leur commande et l'interfaçage de sources de stockage. A contrario, de nombreux problèmes se posent lors du dimensionnement et du choix de l'architecture de commande du système : quelle stratégie de gestion énergétique doit-on mettre en œuvre au préalable pour optimiser les flux et le dimensionnement des sources ? Quelle commande permet d'intégrer à la fois des critères de performances dynamiques, de stabilité et de robustesse vis-à-vis des incertitudes paramétriques inhérentes à un processus de dimensionnement ? Enfin, quels outils et modèles doit-on mettre en œuvre pour garder un lien fort entre paramètres du système et critères de performances tout au long de ce processus ? Les travaux présentés dans ce mémoire proposent des premières réponses à ces questions, via l'utilisation de techniques de commande avancées comme la commande optimale ou la commande robuste. Des outils originaux de modélisation, basés sur les systèmes d'ordre non entier seront également présentés pour la modélisation de dispositifs diffusifs (machines électriques, générateurs électrochimiques) ou modélisés par des équations aux dérivées partielles.

Ces travaux portent sur la validation de modèles de systèmes sur puce (SoC) au niveau transactionnel (TLM). Ces modèles servent notamment au développement du logiciel embarqué. Le matériel est intrinsèquement parallèle mais le simulateur utilise un seul processeur. Les principales entités parallèles du matériel (processeurs, DMA, arbitres de bus, ...) sont représentées en TLM par des processus asynchrones, qui doivent être ordonnancés lors des simulations. Cet ordonnancement est indéterministe afin de mieux représenter le parallélisme physique.<br /><br />Cela pose un problème pour la validation par simulations : il faut couvrir l'espace des ordonnancements en plus de celui des données. En effet, un ordonnanceur déterministe peut cacher des erreurs, car il ne montre qu'un comportement parmi d'autres. Des ordonnancements aléatoires permettent d'observer plus de comportements mais la couverture est incertaine. Un parcours exhaustif de tous les ordonnancements serait beaucoup trop long pour des tests réels.<br /><br />Nous présentons une solution pour couvrir efficacement l'espace des ordonnancements. Celle-ci est basée sur de la réduction d'ordre partiel dynamique. L'idée est d'observer l'influence de l'ordonnancement sur les communications entre processus, pour générer dynamiquement de nouveaux ordonnancements, menant très probablement à des états finaux différents. En itérant sur chaque nouvel ordonnancement, nous obtenons un jeu complet d'ordonnancements, qui garantit la détection, pour un jeu fixé de données, de toutes les erreurs locales et de tous les inter-blocages.<br /><br />Toujours avec l'objectif d'une meilleure représentativité du matériel, les développeurs ont ajouté du temps imprécis à leurs modèles TLM, sous forme de délais bornés. Pour la validation par simulations, cela oblige à couvrir aussi l'espace des temporisations. Nous présentons une extension à la réduction d'ordre partiel dynamique pour résoudre ce problème. Le nouvel algorithme et son prototype retournent un ensemble de jeux de durées, qui garantit de nouveau la détection complète des erreurs locales et inter-blocages pour des données fixées.<br /><br />Enfin, nous étudions comment paralléliser le simulateur SystemC afin de profiter des machines multiprocesseurs, tout en respectant la spécification de SystemC et les particularités des modèles TLM.

Les progrès constants en miniaturisation des transistors et l'augmentation des fréquences des signaux utilisés sont les principales tendances dans l'évolution des circuits électroniques. Avec ces évolutions apparaissent de nombreux effets indésirables qui perturbent le comportement des systèmes électroniques et sont soupçonnés d'être responsables de la majorité des dégradations de signaux dans les systèmes en haute fréquence. Des retards de propagation indésirables sont ainsi introduits par la présence des interconnexions, et la diaphonie, phénomène dû aux couplages entre lignes d'interconnexions, peut éventuellement provoquer des commutations non désirées des transistors. La prise en compte des interconnexions, dès les premières phases de conception d'un système, est par conséquent devenue une nécessité ces dernières années. Mais la simulation temporelle d'un réseau d'interconnexions est très gourmande en temps de calcul, ce qui impacte la durée globale de conception. Le remplacement des modèles électriques, décrivant précisément les interconnexions, par des modèles plus simples est primordial pour limiter les coûts de calcul. Une méthode de réduction d'ordre des modèles peut alors être employée pour effectuer cette opération efficacement. Le modèle final doit en effet décrire assez précisément certains aspects importants du modèle original et conserver les propriétés importantes du réseau d'interconnexions. Cette démarche permettra aux concepteurs d'effectuer des simulations temporelles rapides et d'étudier les paramètres d'intégrité du signal tel que le retard, le temps de montée, le dépassement....L'objectif de cette thèse est d'établir un nouvel outil de réduction de complexité des modèles de réseaux d'interconnexions. Différentes descriptions initiales des systèmes d'interconnexions sont envisagées : modèles circuits (fonctions de transfert) ou mesures fréquentielles. L'approche développée repose sur l'utilisation des fonctions orthogonales de Müntz-Laguerre et de Kautz afin de décrire mathématiquement, de manière précise, le système d'origine. Un opérateur linéaire, lié à ces fonctions de base, est ensuite appliqué pour déterminer un modèle rationnel de moindre complexité. La technique proposée est comparée à d'autres méthodes de la littérature d'abord sur des exemples académiques. Tout le potentiel de la méthode est ensuite illustré par sa mise en œuvre sur des réseaux d'interconnexions.

Nous présentons dans cette thèse nos travaux sur la réduction d'ordre appliquée à des simulations d'aérothermie. Nous considérons le couplage entre les équations de Navier-Stokes et une équations d'énergie de type advection-diffusion. Les paramètres physiques considérés nous obligent à considéré l'introduction d'opérateurs de stabilisation de type SUPG ou GLS. Le but étant d'ajouter une diffusion numérique dans la direction du champs de convection, afin de supprimer les oscillations non-phyisques. Nous présentons également notre stratégie de résolution basée sur la méthode des bases réduite (RBM). Afin de retrouver une décomposition affine, essentielle pour l'application de la RBM, nous avons implémenté une version discrète de la méthode d'interpolation empirique (EIM). Cette variante permet de la construction d'approximation affine pour des opérateurs complexes. Nous utilisons notamment cette méthode pour la réduction des opérateurs de stabilisations. Cependant, la construction des bases EIM pour des problèmes non-linéaires implique un grand nombre de résolution éléments finis. Pour pallier à ce problème, nous mettons en oeuvre les récents développement de l'algorithme de coconstruction entre EIM et RBM (SER). / We present in this thesis our work on model order reduction for aerothermal simulations. We consider the coupling between the incompressible Navier-Stokes equations and an advection-diffusion equation for the temperature. Since the physical parameters induce high Reynolds and Peclet numbers, we have to introduce stabilization operators in the formulation to deal with the well known numerical stability issue. The chosen stabilization, applied to both fluid and heat equations, is the usual Streamline-Upwind/Petrov-Galerkin (SUPG) which add artificial diffusivity in the direction of the convection field. We also introduce our order reduction strategy for this model, based on the Reduced Basis Method (RBM). To recover an affine decomposition for this complex model, we implemented a discrete variation of the Empirical Interpolation Method (EIM) which is a discrete version of the original EIM. This variant allows building an approximated affine decomposition for complex operators such as in the case of SUPG. We also use this method for the non-linear operators induced by the shock capturing method. The construction of an EIM basis for non-linear operators involves a potentially huge number of non-linear FEM resolutions - depending on the size of the sampling. Even if this basis is built during an offline phase, we usually can not afford such expensive computational cost. We took advantage of the recent development of the Simultaneous EIM Reduced basis algorithm (SER) to tackle this issue.

La vérification des systèmes d'états finis, qu'ils soient distribués ou concurrents, est confrontée en pratique au problème d'explosion d'états (taille prohibitive de l'espace d'états sous-jacent) qui survient pour des systèmes de taille réaliste, contenant de nombreux processus en parallèle et des structures de données complexes. Différentes techniques ont été proposées pour combattre l'explosion d'états, telles que la vérification à la volée, la réduction d'ordre partiel, ou encore la vérification distribuée. Cependant, l'expérience pratique a montré qu'aucune de ces techniques, à elle seule, n'est toujours suffisante pour maîtriser des systèmes à grande échelle. Cette thèse propose une combinaison de ces approches dans le but de faire passer à l'échelle leurs capacités de vérification. Notre approche est basée sur les Systèmes d'Equations Booléennes (SEBs), qui fournissent une représentation intermédiaire élégante des problèmes de vérification définis sur des Systèmes de Transitions Etiquetées, comme la comparaison par équivalence, la réduction par tau-confluence, l'évaluation de formules de mu-calcul modal sans alternance, ou encore la génération de cas de tests de conformité. Nous proposons DSolve et MB-DSolve, deux nouveaux algorithmes pour la résolution distribuée à la volée de SEBs (contenant un, resp. plusieurs blocs d'équations), et nous les employons comme moteurs de calcul pour quatre outils de vérification à la volée développés au sein de la boîte à outils CADP en utilisant l'environnement OPEN/CAESAR : le comparateur par équivalence BISIMULATOR, le réducteur TAU_CONFLUENCE, l'évaluateur de propriétés temporelles EVALUATOR, et le générateur de cas de tests de conformité EXTRACTOR. Les mesures expérimentales effectuées sur des grappes de machines montrent des accélérations quasi-linéaires et un bon passage à l'échelle des versions distribuées de ces outils par rapport à leurs équivalents séquentiels.