Thèse : Mécanique : Faculté des Sciences de Paris : 1837. / Titre provenant de l'écran-titre.

Th. doct.-ing.--Paris--École nationale supérieure de mécanique, 1984. / Bibliogr. p. 114-120.

Thèse : Mécanique : Université, Faculté des sciences de Paris : 1839. / Titre provenant de l'écran-titre.

Reproduction de : Thèse de doctorat : Mécanique : Faculté des sciences de Paris : 1866. Reproduction de : Thèse de doctorat : Algèbre : Faculté des sciences de Paris : 1866. / Titre provenant de la page de titre du document numérisé.

L'objectif général de cette thèse est d'étudier les mécanismes de transport des déchets marins flottants ainsi queleur accumulation potentielle en Méditerranée, en s'appuyant sur la modélisation numérique de leur dérive ainsique sur des observations in-situ de leur distribution. La dynamique du transport des déchets marins y estnotamment analysée en terme d'échelles caractéristiques du bassin, en partant de la grande échelle jusqu'auxéchelles côtière et littorale.Dans un premier temps, l'examen d'un ensemble d'expériences Lagrangiennes numériques a permis d'identifierdans le bassin des zones probables d'accumulation non permanentes à grande échelle (Mansui et al., 2015a).L'impact à l'échelle côtière d'un courant de bord (Courant Nord) et des forçages atmosphériques sur ladistribution locale et l'échouage des déchets marins flottants a ensuite pu être estimé en utilisant notammentdes données originales recueillies en mer et à terre (Mansui et al., 2015b, en révision). / The main objective of this work is to study the floating marine debris transport mechanisms and their potentialaccumulation in the Mediterranean Sea, using numerical modelling and in-situ observations of debris. Thetransport dynamics is analysed in terms of typical scales in the basin, from the large scale to the coastal andlocal scales.First, the analysis of a Lagrangian experience data set show the potential existence of non-permanent and largeretention areas (Mansui et al., 2015a). In a second stage, the coastal impact of a boundary current (the NorthernCurrent) and atmospheric forcings on the local distribution and stranding of floating marine litter has beenestimated (Mansui et al., 2015b, under revision), using an original set of data combining offshore sightings andbeaching surveys.

La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues.<br /><br />Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse Simulation Abstraite. L'objectif de la Simulation Abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La Simulation Abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel.<br /><br />Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par une méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation du domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.

Ce mémoire reprend quelques résultats obtenus entre 2000 et 2007 au sein du projet Arénaire du LIP. La problématique centrale est l'évaluation de fonctions numériques : étant donnée une fonction réelle, par exemple un polynôme, un sinus, une exponentielle ou toute autre fonction utile, il s'agit de construire un opérateur pour l'évaluer. Pour cela, on dispose de quelques règles du jeu et de quelques briques de bases: pour le matériel, on peut utiliser, avec un parallélisme arbitraire, des additions et multiplications entières et des tables précalculées. Pour le logiciel, on dispose en plus d'opérateurs de calcul en virgule flottante, mais avec un modèle d'exécution séquentiel. Dans les deux cas, on est contraint à des approximations dont on cherche à minimiser l'erreur. La question de la précision, notamment des calculs intermédiaires, est ici intimement liée à celle de la performance. Pour gérer tous ces paramètres et obtenir des implémentations de qualité, il faut de plus en plus d'automatisation. De plus, pour que cette qualité soit garantie, il faut se rapprocher du monde de la preuve formelle. Ces différents aspects sont évoqués, ainsi que des applications de ces travaux aux accélérateurs de calcul reconfigurables et à la normalisation de la virgule flottante.

Ce travail s'inscrit dans le cadre de la simulation numérique de procédé de forgeage des métaux. Il s'articule autour de deux thèmes principaux que sont l'adaptation du logiciel Forge3® au procédé de roulage d'anneaux à mi-chaud d'une part, et la réduction des temps de calcul d'autre part. Après un premier chapitre décrivant le cadre d'étude, est présentée dans une deuxième partie l'étude du procédé de roulage. Grâce à l'introduction d'un nouveau formalisme des outils flottants dans le logiciel, on arrive à reproduire fidèlement la cinématique particulière de l'outillage. Ces développements sont validés par une confrontation directe avec des résultats expérimentaux. Vient ensuite un travail d'identification des paramètres thermiques de la simulation. Ces paramètres sont validés par l'étude de deux types de bagues sensiblement différentes. Les résultats sont très encourageants, la simulation se montrant prédictive sur la trajectoire de l'outillage, ainsi que sur l'évolution de la température de la matrice tout au long d'un cycle, et ce sur les deux symboles différents. On présente enfin dans une troisième partie une nouvelle méthode de résolution de systèmes linéaires basée sur un algorithme multigrilles trois niveaux. Le solveur multigrille, construit à partir de la librairie PETSc, est fondé sur une technique de déraffinement automatique de maillage qui permet d'obtenir des maillages grossiers emboîtés par noeuds. Après une étude paramétrique permettant la bonne configuration du solveur, on vérifie numériquement sa convergence asymptotique linéaire. Les performances obtenues sur différents cas de forgeage sont édifiantes, avec une division du temps de résolution d'un système linéaire par un facteur 6, pour une division du temps de calcul total de la simulation par un facteur 3 pour des maillages d'environ 60000 noeuds.

La vérification des programmes est un enjeu majeur pour les applications critiques comme l'aviation, l'aérospatiale ou les systèmes embarqués. Les approches Bounded model checking (e.g., CBMC) et de programmation par contraintes (e.g., CPBPV, …) reposent sur la recherche de contre-exemples qui violent une propriété du programme à vérifier. La recherche de tels contre-exemples peut être très longue et coûteuse lorsque les programmes à vérifier contiennent des calculs en virgule flottante. Ceci est dû en grande partie au fait que les stratégies de recherche existantes ont été conçues pour des domaines finis et, dans une moindre mesure, pour des domaines continus. Dans cette thèse, nous proposons un ensemble de stratégie de recherche dédié à la vérification de programme avec du calcul sur les flottants. Les stratégies proposées pour les choix de variables et de choix de valeur se basent sur des propriétés propres aux flottants. Ces propriétés utilisent des caractéristiques des domaines des variables, ou de la structure des contraintes. Certaines propriétés qui portent sur les domaines des variables sont classiques comme la taille et la cardinalité et d'autres beaucoup plus spécifiques comme la densité. Les notions de taille et cardinalité sont équivalentes sur les entiers, mais ne le sont pas sur les flottants. Ainsi la densité capture une variabilité qui est très spécifique aux flottants dont la moitié se trouve entre [-1,1]. De manière similaire les propriétés qui portent sur la structure des contraintes sont, pour certaines tels que le degré ou le nombre d’occurrences, issues des domaines finis, et pour d’autres beaucoup plus spécifiques, comme l’absorption, et la cancellation; ces deux propriétés capturent des phénomènes qui sont généralement la cause de fortes déviations du programme flottant vis-à-vis son interprétation sur les réels et donc de l’existence même de beaucoup de contre-exemples. Pour chaque propriété, deux stratégies de choix de variables sont proposées. La première choisit la variable qui minimise la propriété, alors que la seconde choisit la variable qui la maximise. Les stratégies de choix de valeurs essaient quant à elles de tirer profit des phénomènes d'absorption et de cancellation. L'évaluation de ces stratégies sur un ensemble de programmes réalistes est très encourageante : ces stratégies sont plus efficaces que les stratégies standards. / Program verification is a major issue for critical applications such as aviation, aerospace or embedded systems. Bounded model checking (e.g., CBMC) and constraint programming (e.g., CPBPV,...) approaches are based on the search for counter-examples that violate a property of the program to verify. The search for such counter-examples can be very time-consuming and costly when the programs to be verified contain floating point calculations. This is largely due to the fact that existing research strategies have been designed for finite domains and, to a lesser extent, for continuous domains. In this thesis, we propose a set of search strategies dedicated to program verification with floating point computation. The proposed strategies for variable and value selection are based on specific floating properties. These properties use characteristics of the variable domains, or the constraint structure. Some properties that focus on the domains of the variables are classic such as size and cardinality and others much more specific like density. The notions of size and cardinality are equivalent on the integers, but not on the floats. Density captures a variability that is very specific to the floats, half of which are between[-1.1]. Similarly, the properties that concern the structure of constraints are, for some such as the degree or number of occurrences, derived from finite domains, and for others much more specific, such as absorption, and cancellation; these two properties capture phenomena that are generally the cause of strong deviations of the floating point program from its interpretation on the reals and hence the existence of many counterexamples. For each property, two variable selection strategies are proposed. The first one chooses the variable that minimizes the property, while the second one chooses the variable that maximizes it. Value choice strategies try to take advantage of the phenomena of absorption and cancellation.

Les nouveaux systèmes développés par le secteur automobile font de plus en plus appel à l'électronique et nécessiteront bientôt plus de puissance que ce que peuvent fournir les batteries 12 et 24 Volts actuelles. C'est dans ce cadre que de nouvelles batteries 42 Volts vont être introduites. Dans un premier temps, nous avons montré que les solutions "classiques", permettant de diminuer la résistance à l'état passant des composants unipolaires conventionnels, n'étaient plus satisfaisantes car elles se heurtaient à une limitation fondamentale, dite "limite du silicium". C'est pour cette raison que nos travaux de recherche se sont orientés vers de nouveaux transistors MOS de puissance (FLYMOS") adaptés au 42 Volts. Le travail présenté dans ce mémoire est basé sur le concept des îlots flottants (FLi-Diode) et de son application aux composants MOS (FLYMOS"), afin d'améliorer le compromis "tenue en tension/ résistance à l'état passant". Ce concept consiste en l'introduction d'une région flottante P dans une zone N- afin d'étaler le champ électrique dans le volume : la tenue en tension peut ainsi être augmentée sans pour autant dégrader la résistance à l'état passant. Dans un deuxième temps, les paramètres technologiques ont été optimisés à l'aide de la simulation physique bidimensionnelle pour concevoir un transistor FLYMOS" (cellules de bord et centrale) présentant un compromis optimal entre tenue en tension et résistance à l'état passant. Le concept des îlots flottants a ensuite été validé par la réalisation technologique de FLi-Diodes et de FLYMOS" basse tension (BVdss < 100V). Les meilleurs transistors FLYMOS" ainsi réalisés présentent une tenue en tension supérieure à la tenue en tension de la jonction plane et une résistance à l'état passant fortement améliorée puisqu'elle est proche de la limite conventionnelle du silicium.