On identifie simultanément les coefficients d'emmagasinement et de transmissivité hydraulique dans un écoulement souterrain gouvernent par une équation parabolique linéaire. Ces deux paramètres sont supposés être des fonctions constantes par morceaux en espace. Les inconnues du problème sont non seulement les valeurs de ces coefficients mais aussi la géométrie des zones dans lesquelles ces coefficients sont constants. Le problème est formule comme la minimisation d'une fonction de moindres carres calculant la différence entre les mesures et les quantités correspondantes évaluées avec la valeur courante des paramètres. L'objectif principal de ce travail est la construction d'une technique de paramétrisation adaptative guidée par des indicateurs de raffinement. L'utilisation d'indicateurs de raffinement, nous permet de construisons la paramétrisation de façon itérative, on allant d'une paramétrisation à une seule zone à une paramétrisation avec m zones où m est une valeur optimale à identifier. Nous distinguons les cas ou les deux paramètres ont la même paramétrisation et le cas où les deux paramètres ont des paramétrisations différentes. Pour améliorer la résolution du problème inverse d'estimation de paramètres, nous incorporons des estimateurs d'erreurs a posteriori. / We identify simultaneously storage and hydraulic transmissivity coefficients in groundwater flow governed by a linear parabolic equation. Both parameters are assumed to be functions piecewise constant in space. The unknowns are the coefficient values as well as the geometry of the zones where these coefficients are constant. This problem is formulated as minimizing a least-square function calculating the difference between measurements and the corresponding quantities computed with the current parameters values. The main point of this work is to construct an adaptative parameterization technique guided by refinement indicators. Using refinement indicators, we build the parameterization iteratively, going from a one zone parametrization to a parametrization with $m$ zones where $m$ is an optimal value to identify. We distinguish the cases where the two parameters have the same parameterization and different parameterizations.\\ To improve the resolution of the inverse problem, we incorporate a posteriori error estimations.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

La recherche de la sûreté de fonctionnement des systèmes complexes impose une démarche de conception rigoureuse. Les travaux de cette thèse s’inscrivent dans le cadre la modélisation formelle des systèmes de contrôle autonomes tolérants aux fautes. Le premier objectif a été de proposer une formalisation d’une architecture générique en couches fonctionnelles qui couvre toutes les activités essentielles du système de contrôle et qui intègre des mécanismes de sécurité. Le second objectif a été de fournir une méthode et des outils pour évaluer qualitativement les exigences de sécurité. Le cadre formel de modélisation et d’évaluation repose sur le formalisme Event-B. La modélisation Event-B proposée tire son originalité d’une prise en compte par raffinements successifs des échanges et des relations entre les couches de l’architecture étudiée. Par ailleurs, les exigences de sécurité sont spécifiées à l’aide d’invariants et de théorèmes. Le respect de ces exigences dépend de propriétés intrinsèques au système décrites sous forme d’axiomes. Les preuves que le principe d’architecture proposé satisfait bien les exigences de sécurité attendue ont été réalisées avec les outils de preuve de la plateforme Rodin. L’ensemble des propriétés fonctionnelles et des propriétés relatives aux mécanismes de tolérance aux fautes, ainsi modélisées en Event-B, renforce la pertinence de la modélisation adoptée pour une analyse de sécurité. Cette approche est par la suite mise en œuvre sur un cas d’étude d’un drone ONERA. / The study of complex system safety requires a rigorous design process. The context of this work is the formal modeling of fault tolerant autonomous control systems. The first objective has been to provide a formal specification of a generic layered architecture that covers all the main activities of control system and implement safety mechanisms. The second objective has been to provide tools and a method to qualitatively assess safety requirements. The formal framework of modeling and assessment relies on Event-B formalism. The proposed Event-B modeling is original because it takes into account exchanges and relations betweenarchitecture layers by means of refinement. Safety requirements are first specified with invariants and theorems. The meeting of these requirements depends on intrinsic properties described with axioms. The proofs that the concept of the proposed architecture meets the specified safety requirements were discharged with the proof tools of the Rodin platform. All the functional properties and the properties relating to fault tolerant mechanisms improve the relevance of the adopted Event-B modeling for safety analysis. Then, this approach isimplemented on a study case of ONERA UAV.

Les nouveaux enjeux environnementaux motivent la recherche par les acteurs de l'industrie aéronautique de méthodes de calcul de trajectoires optimales. Les contributions de cette thèse se déclinent selon trois axes. Dans un premier temps, plusieurs techniques d'optimisation de trajectoire avion sont comparées sur un cas simple traité dans la bibliographie universitaire. Puis, un modèle réduit pour prendre en compte le niveau des nuisances sonores dans un algorithme d'optimisation de trajectoire est proposé.Enfin, un problème d'optimisation de trajectoire de montée d'un avion civil est résolu par une approche directe. Les spécificités du problème consistent en la présence de plusieurs phases au sein de la trajectoire, la formulation de contraintes égalités à vérifier par des composantes du vecteur d'état sur des intervalles de temps et enfin la difficulté d'intégration numérique du modèle de bruit. / Forthcoming environmental challenges stimulate the development of trajectory optimization methods by aeronautical actors. This contribution consists in three parts. First, several trajectory optimization techniques are compared. The comparison is based on a simple academic problem. After that, a model is proposed for considering noise nuisance level in the framework of trajectory optimization. Finally, the optimization problem of an ascent phase of a civil aircraft is solved using a direct approach. The specific issues of the problem are tackled with a general formulation. They consist in the presence of several phases along the trajectory, running state equality constraints and tough numerical integration of the noise model.

Cet ouvrage aborde la génération de grilles de Voronoï sous contrainte pour réduire les erreurs liées à la géométrie des cellules lors de la simulation réservoir. Les points de Voronoï sont optimisés en minimisant des fonctions objectif correspondant à différentes contraintes géométriques. L'originalité de cette approche est de pouvoir combiner les contraintes simultanément : - la qualité des cellules, en plaçant les points de Voronoï aux barycentres des cellules ; - le raffinement local, en fonction d'un champ de densité [rho], correspondant à la perméabilité, la vitesse ou la vorticité ; - l'anisotropie des cellules, en fonction d'un champ de matrice M contenant les trois vecteurs principaux de l'anisotropie, dont l'un est défini par le vecteur vitesse ou par le gradient stratigraphique ; - l'orientation des faces des cellules, en fonction d'un champ de matrice M contenant les trois vecteurs orthogonaux aux faces, dont l'un est défini par le vecteur vitesse ; - la conformité aux surfaces du modèle structural, failles et horizons ; - l'alignement des points de Voronoï le long des puits. La qualité des grilles générées est appréciée à partir de critères géométriques et de résultats de simulation comparés à des grilles fines de référence. Les résultats indiquent une amélioration de la géométrie, qui n'est pas systématiquement suivie d'une amélioration des résultats de simulation / Voronoi grids are generated under constraints to reduce the errors due to cells geometry during flow simulation in reservoirs. The Voronoi points are optimized by minimizing objective functions relevant to various geometrical constraints. An original feature of this approach is to combine simultaneously the constraints: - Cell quality, by placing the Voronoi points at the cell barycenters. - Local refinement according to a density field rho, relevant to permeability, velocity or vorticity. - Cell anisotropy according to a matrix field M built with the three principal vectors of the anisotropy, which one is defined by the velocity vector or by the stratigraphic gradient. - Faces orientation according to a matrix field M built with the three vectors orthogonal to the faces, which one is defined by the velocity vector. - Conformity to structural features, faults and horizons. - Voronoï points alignment along well path. The quality of the generated grids is assessed from geometrical criteria and from comparisons of flow simulation results with reference fine grids. Results show geometrical improvements, that are not necessarily followed by flow simulation results improvements

Cette thèse s'intéresse à la conception et à l'analyse de méthodes de discrétisation hybrides pour les inégalités variationnelles non linéaires apparaissant en mécanique des fluides et des solides. Les principaux avantages de ces méthodes sont la conservation locale au niveau des mailles, la robustesse par rapport à différents régimes de paramètres et la possibilité d’utiliser des maillages polygonaux / polyédriques avec des nœuds non coïncidants, ce qui est très intéressant dans le contexte de l’adaptation de maillage. Les méthodes de discrétisation hybrides sont basées sur des inconnues discrètes attachées aux faces du maillage. Des inconnues discrètes attachées aux mailles sont également utilisées, mais elles peuvent être éliminées localement par condensation statique. Deux applications principales des discrétisations hybrides sont abordées dans cette thèse. La première est le traitement par la méthode de Nitsche du problème de contact de Signorini (dans le cas scalaire) avec une non-linéarité dans les conditions aux limites. Nous prouvons des estimations d'erreur optimales conduisant à des taux de convergence d'erreur d'énergie d'ordre (k + 1), si des polynômes de face de degré k >= 0 sont utilisés. La deuxième application principale concerne les fluides à seuil viscoplastiques. Nous concevons une méthode de Lagrangien augmenté discrète appliquée à la discrétisation hybride. Nous exploitons la capacité des méthodes hybrides d’utiliser des maillages polygonaux avec des nœuds non coïncidants afin d'effectuer l’adaptation de maillage local et mieux capturer la surface limite. La précision et la performance des schémas sont évaluées sur des cas tests bidimensionnels, y compris par des comparaisons avec la littérature / This thesis is concerned with the devising and the analysis of hybrid discretization methods for nonlinear variational inequalities arising in computational mechanics. Salient advantages of such methods are local conservation at the cell level, robustness in different regimes and the possibility to use polygonal/polyhedral meshes with hanging nodes, which is very attractive in the context of mesh adaptation. Hybrid discretizations methods are based on discrete unknowns attached to the mesh faces. Discrete unknowns attached to the mesh cells are also used, but they can be eliminated locally by static condensation. Two main applications of hybrid discretizations methods are addressed in this thesis. The first one is the treatment using Nitsche's method of Signorini's contact problem (in the scalar-valued case) with a nonlinearity in the boundary conditions. We prove optimal error estimates leading to energy-error convergence rates of order (k+1) if face polynomials of degree k >= 0 are used. The second main application is on viscoplastic yield flows. We devise a discrete augmented Lagrangian method applied to the present hybrid discretization. We exploit the capability of hybrid methods to use polygonal meshes with hanging nodes to perform local mesh adaptation and better capture the yield surface. The accuracy and performance of the present schemes is assessed on bi-dimensional test cases including comparisons with the literature

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

Le raffinement de nuage de points et la reconstruction de surface sont deux problèmes fondamentaux dans le traitement de la géométrie. La plupart des méthodes existantes ont été ciblées sur les données de capteur de distance et se sont avérées être mal adaptées aux données multi-vues. Dans cette thèse, deux nouvelles méthodes sont proposées respectivement pour les deux problèmes avec une attention particulière aux données multi-vues. La première méthode permet de lisser les nuages de points provenant de la reconstruction multi-vue sans endommager les données. Le problème est formulé comme une optimisation non-linéaire sous contrainte et ensuite résolu par une série de problèmes d’optimisation sans contrainte au moyen d’une méthode de barrière. La seconde méthode effectue une triangulation du nuage de points d’entrée pour générer un maillage en utilisant une stratégie de l’avancement du front pilotée par un critère de l’empilement compact de sphères. L’algorithme est simple et permet de produire efficacement des maillages de haute qualité. Les expérimentations sur des données synthétiques et du monde réel démontrent la robustesse et l’efficacité des méthodes proposées. Notre méthodes sont adaptées aux applications qui nécessitent des informations de position précises et cohérentes telles que la photogrammétrie et le suivi des objets en vision par ordinateur / Point cloud refinement and surface reconstruction are two fundamental problems in geometry processing. Most of the existing methods have been targeted at range sensor data and turned out be ill-adapted to multi-view data. In this thesis, two novel methods are proposed respectively for the two problems with special attention to multi-view data. The first method smooths point clouds originating from multi-view reconstruction without impairing the data. The problem is formulated as a nonlinear constrained optimization and addressed as a series of unconstrained optimization problems by means of a barrier method. The second method triangulates point clouds into meshes using an advancing front strategy directed by a sphere packing criterion. The method is algorithmically simple and can produce high-quality meshes efficiently. The experiments on synthetic and real-world data have been conducted as well, which demonstrates the robustness and the efficiency of the methods. The developed methods are suitable for applications which require accurate and consistent position information such photogrammetry and tracking in computer vision

Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée / This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V

L'analyse isométrique s'est révélée être un outil très prometteur pour la conception et l'analyse. Une tâche difficile consiste toujours à faire passer l'IGA de concept à un outil de conception pratique pour l'industrie et ce travail contribue à cet effort. Ce travail porte sur l'implémentation de l'IGA dans le solveur explicite Altair Radioss afin de répondre aux applications de simulation de crash et d'emboutissage. Pour cela, les ingrédients nécessaires à une intégration native de l'IGA dans un code éléments finis traditionnel ont été identifiés et adaptés à l'architecture de code existante. Un élément solide B-Spline et NURBS a été développé dans Altair Radioss. Les estimations heuristiques des pas de temps élémentaires ou nodaux sont explorées pour améliorer l'efficacité des simulations et garantir leur stabilité. Une interface de contact existante a été étendue afin de fonctionner de manière transparente avec les éléments finis NURBS et de Lagrange. Un raffinement local est souvent nécessaire pour la bonne représentation de champs non linéaires tels que les champs de déformations plastiques. Une analyse est faite en termes de compatibilité pour l'analyse et de mise en oeuvre pour plusieurs bases de fonctions Spline telles que les Hierarchical B-Splines, les Truncated Hierarchical B-Splines, les T-Splines et les Locally Refined B-Splines (LR B-Splines). Les LR B-Splines sont implémentés. Un schéma de raffinement est proposé et définit un sous-ensemble de raffinements adapté à leur utilisation au sein de Radioss. Le processus de raffinement d’un maillage initialement grossier et régulier est développé au sein du solveur. Il permet à l’utilisateur d’établir du raffinement local par un ensemble d’instructions à fournir dans le jeu de donnée de la simulation. La solution globale est validée sur des cas tests industriels, pour des cas de validation classiquement utilisés pour les codes industriels comme l'emboutissage et les tests de chute. / IsoGeometric Analysis has shown to be a very promising tool for an integrated design and analysis process. A challenging task is still to move IGA from a proof of concept to a convenient design tool for industry and this work contributes to this endeavor. This work deals with the implementation of the IGA into Altair Radioss explicit finite element solver in order to address crash and stamping simulation applications. To this end, the necessary ingredients to a smooth integration of IGA in a traditional finite element code have been identified and adapted to the existing code architecture. A solid B-Spline element has been developed in Altair Radioss. The estimations of heuristic element and nodal stable time increment are explored to improve the accuracy of simulations and guarantee their stability. An existing contact interface has been extended in order to work seamlessly with both NURBS and Lagrange finite elements. As local refinement is needed for solution approximation, an analysis is made in terms of analysis suitability and implementation aspects for several Spline basis functions as Hierarchical B-Splines (HB-Splines), Truncated Hierarchical B-Splines (THB-Splines), T-Splines and Locally Refined B-Splines (LR B-Splines). The LR B-Spline basis is implemented. An improved refinement scheme is introduced and defines a set of analysis-suitable refinements to be used in Radioss. The refinement process of a regular coarse mesh is developed inside the solver. It allows the user to define a local refinement giving a set of instructions in the input file. The global solution is validated on industrial benchmarks, for validation cases conventionally used for industrial codes like stamping and drop test.