La quantité croissante des données s’accompagne par l’augmentation du nombre de programmes de transformation de données, généralement des requêtes, et par la nécessité d’analyser et comprendre leurs résultats : (a) pourquoi telle réponse figure dans le résultat ? ou (b) pourquoi telle information n’y figure pas ? La première question demande de trouver l’origine ou la provenance des résultats dans la base, un problème très étudié depuis une 20taine d’années. Par contre, expliquer l’absence de réponses dans le résultat d’une requête est un problème peu exploré jusqu’à présent. Répondre à une question Pourquoi-Pas consiste à fournir des explications quant à l’absence de réponses. Ces explications identifient pourquoi et comment les données pertinentes aux réponses manquantes sont absentes ou éliminées par la requête. Notre travail suppose que la base de données n’est pas source d’erreur et donc cherche à fournir des explications fondées sur (les opérateurs de) la requête qui peut alors être raffinée ultérieurement en modifiant les opérateurs "fautifs". Cette thèse développe des outils formels et algorithmiques destinés au débogage et à la réparation de requêtes SQL afin de traiter des questions de type Pourquoi-Pas. Notre première contribution, inspirée par une étude critique de l’état de l’art, utilise un arbre de requête pour rechercher les opérateurs "fautifs". Elle permet de considérer une classe de requêtes incluant SPJA, l’union et l’agrégation. L’algorithme NedExplain développé dans ce cadre, a été validé formellement et expérimentalement. Il produit des explications de meilleure qualité tout en étant plus efficace que l’état de l’art.L’approche précédente s’avère toutefois sensible au choix de l’arbre de requête utilisé pour rechercher les explications. Notre deuxième contribution réside en la proposition d’une notion plus générale d’explication sous forme de polynôme qui capture toutes les combinaisons de conditions devant être modifiées pour que les réponses manquantes apparaissent dans le résultat. Cette méthode s’applique à la classe des requêtes conjonctives avec inégalités. Sur la base d’un premier algorithme naïf, Ted, ne passant pas à l’échelle, un deuxième algorithme, Ted++, a été soigneusement conçu pour éliminer entre autre les calculs itérés de sous-requêtes incluant des produits cartésien. Comme pour la première approche, une évaluation expérimentale a prouvé la qualité et l’efficacité de Ted++. Concernant la réparation des requêtes, notre contribution réside dans l’exploitation des explications polynômes pour guider les modifications de la requête initiale ce qui permet la génération de raffinements plus pertinents. La réparation des jointures "fautives" est traitée de manière originale par des jointures externes. L’ensemble des techniques de réparation est mis en oeuvre dans FixTed et permet ainsi une étude de performance et une étude comparative. Enfin, Ted++ et FixTed ont été assemblés dans une plate-forme pour le débogage et la réparation de requêtes relationnelles. / With the increasing amount of available data and data transformations, typically specified by queries, the need to understand them also increases. “Why are there medicine books in my sales report?” or “Why are there not any database books?” For the first question we need to find the origins or provenance of the result tuples in the source data. However, reasoning about missing query results, specified by Why-Not questions as the latter previously mentioned, has not till recently receivedthe attention it is worth of. Why-Not questions can be answered by providing explanations for the missing tuples. These explanations identify why and how data pertinent to the missing tuples were not properly combined by the query. Essentially, the causes lie either in the input data (e.g., erroneous or incomplete data) or at the query level (e.g., a query operator like join). Assuming that the source data contain all the necessary relevant information, we can identify the responsible query operators formingquery-based explanations. This information can then be used to propose query refinements modifying the responsible operators of the initial query such that the refined query result contains the expected data. This thesis proposes a framework targeted towards SQL query debugging and fixing to recover missing query results based on query-based explanations and query refinements.Our contribution to query debugging consist in two different approaches. The first one is a tree-based approach. First, we provide the formal framework around Why-Not questions, missing from the state-of-the-art. Then, we review in detail the state-of-the-art, showing how it probably leads to inaccurate explanations or fails to provide an explanation. We further propose the NedExplain algorithm that computes correct explanations for SPJA queries and unions there of, thus considering more operators (aggregation) than the state of the art. Finally, we experimentally show that NedExplain is better than the both in terms of time performance and explanation quality. However, we show that the previous approach leads to explanations that differ for equivalent query trees, thus providing incomplete information about what is wrong with the query. We address this issue by introducing a more general notion of explanations, using polynomials. The polynomial captures all the combinations in which the query conditions should be fixed in order for the missing tuples to appear in the result. This method is targeted towards conjunctive queries with inequalities. We further propose two algorithms, Ted that naively interprets the definitions for polynomial explanations and the optimized Ted++. We show that Ted does not scale well w.r.t. the size of the database. On the other hand, Ted++ is capable ii of efficiently computing the polynomial, relying on schema and data partitioning and advantageous replacement of expensive database evaluations by mathematical calculations. Finally, we experimentally evaluate the quality of the polynomial explanations and the efficiency of Ted++, including a comparative evaluation.For query fixing we propose is a new approach for refining a query by leveraging polynomial explanations. Based on the input data we propose how to change the query conditions pinpointed by the explanations by adjusting the constant values of the selection conditions. In case of joins, we introduce a novel type of query refinements using outer joins. We further devise the techniques to compute query refinements in the FixTed algorithm, and discuss how our method has the potential to be more efficient and effective than the related work.Finally, we have implemented both Ted++ and FixTed in an system prototype. The query debugging and fixing platform, short EFQ allows users to nteractively debug and fix their queries when having Why- Not questions.

La migration de données entre des sources aux schémas hétérogènes est un domaine en pleine croissance avec l'augmentation de la quantité de données en accès libre, et le regroupement des données à des fins d'apprentissage automatisé et de fouilles. Cependant, la description du processus de transformation des données d'une instance source vers une instance définie sur un schéma différent est un processus complexe même pour un utilisateur expert dans ce domaine. Cette thèse aborde le problème de la définition de mapping par un utilisateur non expert dans le domaine de la migration de données, ainsi que la vérification du respect par ce mapping des contraintes d'accès ayant été définies sur les données sources. Pour cela, dans un premier temps nous proposons un système dans lequel l'utilisateur fournit un ensemble de petits exemples de ses données, et est amené à répondre à des questions booléennes simples afin de générer un mapping correspondant à ses besoins. Dans un second temps, nous proposons un système permettant de réécrire le mapping produit de manière à assurer qu'il respecte un ensemble de vues de contrôle d'accès définis sur le schéma source du mapping. Plus précisément, le premier grand axe de cette thèse est la formalisation du problème de la définition interactive de mappings, ainsi que la description d'un cadre formel pour la résolution de celui-ci. Cette approche formelle pour la résolution du problème de définition interactive de mappings est accompagnée de preuves de bonnes propriétés. A la suite de cela, basés sur le cadre formel défini précédemment, nous proposons des algorithmes permettant de résoudre efficacement ce problème en pratique. Ces algorithmes visent à réduire le nombre de questions auxquelles l'utilisateur doit répondre afin d'obtenir un mapping correspondant à ces besoins. Pour cela, les mappings possibles sont ordonnés dans des structures de treillis imbriqués, afin de permettre un élagage efficace de l'espace des mappings à explorer. Nous proposons également une extension de cette approche à l'utilisation de contraintes d'intégrité afin d'améliorer l’efficacité de l'élagage. Le second axe majeur vise à proposer un processus de réécriture de mapping qui, étant donné un ensemble de vues de contrôle d'accès de référence, permet d'assurer que le mapping réécrit ne laisse l'accès à aucune information n'étant pas accessible via les vues de contrôle d'accès. Pour cela, nous définissons un protocole de contrôle d'accès permettant de visualiser les informations accessibles ou non à travers un ensemble de vues de contrôle d'accès. Ensuite, nous décrivons un ensemble d'algorithmes permettant la réécriture d'un mapping en un mapping sûr vis-à-vis d'un ensemble de vues de contrôle d'accès. Comme précédemment, cette approche est complétée de preuves de bonnes propriétés. Afin de réduire le nombre d'interactions nécessaires avec l'utilisateur lors de la réécriture d'un mapping, une approche permettant l'apprentissage des préférences de l'utilisateur est proposée, cela afin de permettre le choix entre un processus interactif ou automatique. L'ensemble des algorithmes décrit dans cette thèse ont fait l'objet d'un prototypage et les expériences réalisées sur ceux-ci sont présentées dans cette thèse / Data exchange between sources over heterogeneous schemas is an ever-growing field of study with the increased availability of data, oftentimes available in open access, and the pooling of such data for data mining or learning purposes. However, the description of the data exchange process from a source to a target instance defined over a different schema is a cumbersome task, even for users acquainted with data exchange. In this thesis, we address the problem of allowing a non-expert user to spec- ify a source-to-target mapping, and the problem of ensuring that the specified mapping does not leak information forbidden by the security policies defined over the source. To do so, we first provide an interactive process in which users provide small examples of their data, and answer simple boolean questions in order to specify their intended mapping. Then, we provide another process to rewrite this mapping in order to ensure its safety with respect to the source policy views. As such, the first main contribution of this thesis is to provide a formal definition of the problem of interactive mapping specification, as well as a formal resolution process for which desirable properties are proved. Then, based on this formal resolution process, practical algorithms are provided. The approach behind these algorithms aims at reducing the number of boolean questions users have to answers by making use of quasi-lattice structures to order the set of possible mappings to explore, allowing an efficient pruning of the space of explored mappings. In order to improve this pruning, an extension of this approach to the use of integrity constraints is also provided. The second main contribution is a repairing process allowing to ensure that a mapping is “safe” with respect to a set of policy views defined on its source schema, i.e., that it does not leak sensitive information. A privacy-preservation protocol is provided to visualize the information leaks of a mapping, as well as a process to rewrite an input mapping into a safe one with respect to a set of policy views. As in the first contribution, this process comes with proofs of desirable properties. In order to reduce the number of interactions needed with the user, the interactive part of the repairing process is also enriched with the possibility of learning which rewriting is preferred by users, in order to obtain a completely automatic process. Last but not least, we present extensive experiments over the open source prototypes built from two contributions of this thesis

Dans cette thèse, nous étudions le problème de l’analyse de signatures de pannes dans le domaine de la maintenance avionique, afin d’identifier les défaillances au sein d’équipements en panne et suggérer des actions correctives permettant de les réparer. La thèse a été réalisée dans le cadre d’une convention CIFRE entre Thales Research & Technology et l’Université Paris-Sud. Les motivations sont donc à la fois théoriques et industrielles. Une signature de panne devrait fournir toutes les informations nécessaires pour identifier, comprendre et réparer la panne. Pour comprendre le mécanisme la panne son identification doit donc être explicable. Nous proposons une approche à base d’ontologies pour modéliser le domaine d’étude, permettant une interprétation automatisée des tests techniques réalisés afin d’identifier les pannes et obtenir les actions correctives associées. Il s’agit d’une approche d’apprentissage de concepts permettant de découvrir des concepts représentant les signatures de pannes tout en fournissant des explications sur les choix de propositions de réparations. Comme les signatures ne sont pas connues a priori, un algorithme d’apprentissage automatique non supervisé approxime les définitions des concepts. Les signatures apprises sont fournies sous forme de définitions de la logique de description (DL) et ces définitions servent d’explications. Contrairement aux techniques courantes d’apprentissage de concepts conçues pour faire de l’apprentissage supervisé ou basées sur l’analyse de patterns fréquents au sein de gros volumes de données, l’approche proposée adopte une perspective différente. Elle repose sur une construction bottom-up de l’ontologie. Le processus d’apprentissage est réalisé via un opérateur de raffinement appliqué sur l’espace des expressions de concepts et le processus est guidé par les données, c’est-à-dire les individus de l’ontologie. Ainsi, les notions de justifications, de concepts plus spécifiques et de raffinement de concepts ont été révisées et adaptées pour correspondre à nos besoins. L’approche a ensuite été appliquée au problème de la maintenance avionique. Un prototype a été implémenté et mis en œuvre au sein de Thales Avionics à titre de preuve de concept. / In this thesis we explore the problem of signature analysis in avionics maintenance, to identify failures in faulty equipment and suggest corrective actions to resolve the failure. The thesis takes place in the context of a CIFRE convention between Thales R&T and the Université Paris-Sud, thus it has both a theoretical and an industrial motivation. The signature of a failure provides all the information necessary to understand, identify and ultimately repair a failure. Thus when identifying the signature of a failure it is important to make it explainable. We propose an ontology based approach to model the domain, that provides a level of automatic interpretation of the highly technical tests performed in the equipment. Once the tests can be interpreted, corrective actions are associated to them. The approach is rooted on concept learning, used to approximate description logic concepts that represent the failure signatures. Since these signatures are not known in advance, we require an unsupervised learning algorithm to compute the approximations. In our approach the learned signatures are provided as description logics (DL) definitions which in turn are associated to a minimal set of axioms in the A-Box. These serve as explanations for the discovered signatures. Thus providing a glass-box approach to trace the reasons on how and why a signature was obtained. Current concept learning techniques are either designed for supervised learning problems, or rely on frequent patterns and large amounts of data. We use a different perspective, and rely on a bottom-up construction of the ontology. Similarly to other approaches, the learning process is achieved through a refinement operator that traverses the space of concept expressions, but an important difference is that in our algorithms this search is guided by the information of the individuals in the ontology. To this end the notions of justifications in ontologies, most specific concepts and concept refinements, are revised and adapted to our needs. The approach is then adapted to the specific avionics maintenance case in Thales Avionics, where a prototype has been implemented to test and evaluate the approach as a proof of concept.

Dans cette thèse, nous nous intéressons à la résolution des équations SPN du transport de neutrons au sein des cœurs de réacteurs nucléaires à eau pressurisée. Ces équations forment un problème aux valeurs propres généralisé. Dans notre étude nous commençons par le problème source associé et ensuite nous étudions le problème aux valeurs propres. Un cœur de réacteur est composé de différents milieux: le combustible, le fluide caloporteur, le modérateur... à cause de ces hétérogénéités de la géométrie, le flux solution du problème source peut être peu régulier. Nous proposons l’analyse numérique de l’approximation de la solution par la méthode des éléments finis du problème source dans le cas où la solution est peu régulière. Pour le problème aux valeurs propres, dans le cas mixte, les théories déjà développées ne s’appliquent pas. Nous proposons ici une nouvelle méthode pour étudier la convergence de la méthode des éléments finis mixtes pour les problèmes aux valeurs propres. Pour les solutions peu régulières, la montée en ordre de la méthode des éléments finis n’améliore pas l’approximation du problème, il faut raffiner le maillage aux alentours des singularités de la solution. La géométrie des cœurs de réacteur se prête bien aux maillages cartésiens, mais leur raffinement augmente vite leur nombre de degrés de liberté. Pour palier à cette augmentation, nous proposons ici une méthode de décomposition de domaine qui permet d’utiliser des maillages globalement non-conformes. / In this thesis, we investigate the resolution of the SPN neutron transport equations in pressurized water nuclear reactor. These equations are a generalized eigenvalue problem. In our study, we first considerate the associated source problem and after we concentrate on the eigenvalue problem. A nuclear reactor core is composed of different media: the fuel, the coolant, the neutron moderator... Due to these heterogeneities of the geometry, the solution flux can have a low-regularity. We propose the numerical analysis of its approximation with finite element method for the low regular case. For the eigenvalue problem under its mixed form, we can not rely on the theories already developed. We propose here a new method for studying the convergence of the SPN neutron transport eigenvalue problem approximation with mixed finite element. When the solution has low-regularity, increasing the order of the method does not improve the approximation, the triangulation need to be refined near the singularities of the solution. Nuclear reactor cores are well-suited for Cartesian grids, but the refinement of these sort of triangulations increases rapidly their number of degrees of freedom. To avoid this drawback, we propose domain decomposition method which can handle globally non-conforming triangulations.

L’objectif de ce travail est d’étudier les capacités de la méthode de Boltzmann sur réseau (LBM) dans un cadre numériquement contraignant : celui de la simulation aéroacoustique en maillage non-uniforme, à très haut nombre de Reynolds et à nombre de Mach non négligeable (Ma > 0.1), appliquée à l’automobile. La problématique industrielle est celle du calcul du bruit intérieur d’origine aérodynamique, dont le calcul du champ de pression pariétal instationnaire sur le vitrage conducteur est la première étape décisive. Il a été constaté qu’un manque de précision sur la faible part acoustique du champ de pression total sur le vitrage, provenant très probablement d’erreurs au niveau des transitions de résolution du maillage, était la cause d’une surestimation du bruit intérieur. Nous présentons d’abord une construction cohérente et unifiée de la méthode de Boltzmann sur réseau à partir de l’équation de Boltzmann, dans un cadre athermal faiblement compressible. Nous étudions ensuite en détail les propriétés aéroacoustiques de la LBM, en parcourant toutes les grandes familles d’opérateurs de collision de la littérature. Une variante de modèle à temps de relaxation multiples, utilisable pour l’aéroacoustique, est présentée et testée. Un modèle alternatif simplifié de filtrage sélectif, rapide et compact, est développé et validé. La problématique des maillages non-uniformes est abordée. Un recensement exhaustif des études LBM menées dans ce cadre dans la littérature montre qu’aucune ne correspond à nos contraintes. Des algorithmes alternatifs aux transitions sont développés. Enfin, des applications industrielles sont réalisées à l’aide des modèles développés dans le mémoire. / The main goal of this work is to study the capacities of the Lattice Boltzmann Method in a constrained numerical framework : that of numerical simulation in automotive aeroacoustics with non-uniform meshes, at high Reynolds number and non egligible Mach number (Ma > 0.1). The industrial problem is the computation of the interior aerodynamic noise, which includes as its first decisive step the computation of the unsteady wall pressure field on the car windows. It was observed that a lack of precision on the weak acoustic part of the total pressure field on the driver-side window, which is most probably due to errors at mesh refinement interfaces, caused an overestimation of the interior noise. We first present a coherent and unified construction of the Lattice BoltzmannMethod from the Boltzmann equation, in an athermal weakly compressible framework. Then, we study in details the aeroacoustic properties of the LBM by reviewingall the main families of collisional operators that exist in the literature. A variant of multiple relaxation time operator that can be used for aeroacoustics is presented and tested. A simplified alternative selective filter, fast and compact, is developped and numerically validated. The problem of non-uniform meshes is discussed. An exhaustive review of the LBM studies that have been carried out within that framework shows that none of them corresponds to our constraints. Alternative transition nodes algorithms are developed. Finally, all the developed models of this work are applied to industrial cases.

Lors de simulations numériques d'ordre élevé, la discrétisation sous-paramétrique du domaine de calcul peut générer des erreurs dominant l'erreur liée à la discrétisation des variables. De nombreux travaux proposent d'utiliser l'analyse isogéométrique afin de mieux représenter les géométries et de résoudre ce problème. Nous présenterons dans ce travail le couplage du schéma aux résidus distribués limité et stabilisé de Lax-Frieirichs avec l'analyse isogéométrique. En particulier, nous construirons une famille de fonctions de base permettant de représenter exactement les coniques et définies tant sur les éléments triangulaires que quadrangulaires : les fonctions de base de Bernstein rationnelles. Nous nous intéresserons ensuite à la génération de maillages précis pour l'analyse isogéométrique. Notre méthode consiste à créer un maillage courbe à partir d'un maillage linéaire par morceaux de la géométrie. Le maillage obtenu en sortie de notre procédure est non-structuré, conforme et assure la continuité de nos fonctions de base sur tout le domaine. Pour finir, nous décrirons les différentes méthodes d'adaptation de maillages développées : l'élévation d'ordre et le raffinement isotrope. Bien évidemment, la géométrie exacte du maillage courbe d'entrée est préservée au cours des processus d'adaptation.

Lors de simulations numériques d’ordre élevé, la discrétisation sous-paramétrique du domaine de calcul peut générer des erreurs dominant l’erreur liée à la discrétisation des variables. De nombreux travaux proposent d’utiliser l’analyse isogéométrique afin de mieux représenter les géométries et de résoudre ce problème.Nous présenterons dans ce travail le couplage du schéma aux résidus distribués limité et stabilisé de Lax-Frieirichs avec l’analyse isogéométrique. En particulier, nous construirons une famille de fonctions de base permettant de représenter exactement les coniques et définies tant sur les éléments triangulaires que quadrangulaires : les fonctions de base de Bernstein rationnelles. Nous nous intéresserons ensuite à la génération de maillages précis pour l’analyse isogéométrique. Notre méthode consiste à créer un maillage courbe à partir d’un maillage linéaire par morceaux de la géométrie. Le maillage obtenu en sortie de notre procédure est non-structuré, conforme et assure la continuité de nos fonctions de base sur tout le domaine. Pour finir, nous décrirons les différentes méthodes d’adaptation de maillages développées : l’élévation d’ordre et le raffinement isotrope. Bien évidemment, la géométrie exacte du maillage courbe d’entrée est préservée au cours des processus d’adaptation. / During high order simulations, the approximation error may be dominated by the errors linked to the sub-parametric discretization used for the geometry representation. Many works propose to use an isogeometric analysis approach to better represent the geometry and hence solve this problem. In this work, we will present the coupling between the limited stabilized Lax-Friedrichs residual distributed scheme and the isogeometric analysis. Especially, we will build a family of basis functions defined on both triangular and quadrangular elements and allowing the exact representation of conics : the rational Bernstein basis functions. We will then focus in how to generate accurate meshes for isogeometric analysis. Our idea is to create a curved mesh from a classical piecewise-linear mesh of the geometry. We obtain a conforming unstructured mesh which ensures the continuity of the basis functions over the entire mesh. Last, we will detail the curved mesh adaptation methods developed : the order elevation and the isotropic mesh refinement. Of course, the adaptation processes preserve the exact geometry of the initial curved mesh.

Dans ce travail de thèse, on s'est intéressé à la simulation d'écoulements incompressibles multi-échelles et multiphasiques. L'une des principales difficultés numériques est l'introduction d'une diffusion numérique due aux schémas utilisés. Celle-ci étant indépendante du maillage, une possibilité est de simuler ce type d'écoulement avec un très grand nombre points. Cependant, les besoins en ressources informatiques et en temps deviennent rapidement importants. On a donc développé une méthode de raffinement de maillage adaptatif (AMR) dans le but de suivre, soit des interfaces dans un écoulement diphasique, soit des fronts de concentration dans un écoulement monophasique avec transport d'une espèce inerte, de manière précise tout en optimisant le temps CPU et<br />la taille mémoire. On montre au travers de cas d'étude 2D et 3D, judicieusement choisis, l'efficacité de cette méthode.

Avec la plupart des méthodes formelles, un premier modèle peut être raffiné formellement en plusieurs étapes, jusqu'à ce que le raffinement final contienne assez de détails pour une implémentation. Ce premier modèle est généralement construit à partir de la description des besoins obtenue dans la phase d'analyse des exigences. Cette transition de la phase des exigences à la phase de spécification formelle est l'une des étapes les plus délicates dans la chaîne de développement formel. En fait, la construction de ce modèle initial exige un niveau élevé de compétence et beaucoup de pratique, d'autant qu'il n'existe pas de processus bien défini pour aider les concepteurs. Parallèlement à ce problème, il s'avère également que les exigences non-fonctionnelles sont largement marginalisées dans le processus de développement logiciel. Les pratiques industrielles actuelles consistent généralement à spécifier seulement les exigences fonctionnelles durant les premières phases de ce processus et à laisser la prise en compte des exigences non-fonctionnelles au niveau de l'implémentation. Pour surmonter ces problèmes, la thèse vise à définir un couplage entre un modèle d'exigences exprimé en SysML/KAOS et des spécifications formelles abstraites, tout en garantissant une distinction entre les exigences fonctionnelles et non-fonctionnelles dès la phase d'analyse des exigences. Pour cela, la thèse propose tout d'abord deux approches différentes (l'une dédiée au B classique et l'autre à Event-B) dans lesquelles des modèles formels abstraits sont construits progressivement à partir du modèle de buts fonctionnels SysML/KAOS. La thèse se focalise par la suite sur l'approche dédiée à Event-B afin de la compléter et l'enrichir en se servant de deux autres modèles SysML/KAOS qui décrivent les buts non-fonctionnels et leurs impacts sur les buts fonctionnels. Nous présentons différentes manières permettant d'injecter ces buts non-fonctionnels et leurs impacts dans les modèles abstraits Event-B déjà obtenus. Des liens de correspondance entre les buts non-fonctionnels et les différents éléments Event-B sont également établis afin de faciliter la gestion de l'évolution de ces buts. Les différentes approches proposées dans cette thèse ont été appliquées pour la spécification du composant de localisation qui est une partie critique d'un système de transport terrestre. L'approche dédiée à Event-B est implémentée dans l'outil SysKAOS2EventB, permettant ainsi de générer une architecture de raffinement Event-B à partir d'un modèle de buts fonctionnels SysML/KAOS. Cette mise en œuvre s'appuie principalement sur les technologies de transformation de modèles à modèles / With most of formal methods, an initial formal model can be refined in multiple steps, until the final refinement contains enough details for an implementation. Most of the time, this initial model is built from the description obtained by the requirements analysis. Unfortunately, this transition from the requirements phase to the formal specification phase is one of the most painful steps in the formal development chain. In fact, building this initial model requires a high level of competence and a lot of practice, especially as there is no well-defined process to assist designers. Parallel to this problem, it appears that non-functional requirements are largely marginalized in the software development process. The current industrial practices consist generally in specifying only functional requirements during the first levels of this process and in leaving the consideration of non-functional requirements in the implementation level. To overcome these problems, this thesis aims to define a coupling between a requirement model expressed in SysML/KAOS and an abstract formal specification, while ensuring a distinction between functional and non-functional requirements from the requirements analysis phase. For that purpose, this thesis proposes firstly two different approaches (one dedicated to the classical B and the other to Event-B) in which abstract formal models are built incrementally from the SysML/KAOS functional goal model. Afterwards, the thesis focuses on the approach dedicated to Event-B in order to complete it and enrich it by using the two other SysML/KAOS models describing the non-functional goals and their impact on functional goals. We present different ways to inject these non-functional goals and their impact into the obtained abstract Event-B models. Links of correspondance between the non-functional goals and the different Event-B elements are also defined in order to improve the management of the evolution of these goals. The different approaches proposed in this thesis have been applied to the specification of a localization component which is a critical part of a land transportation system. The approach dedicated to Event-B is implemented in the SysKAOS2EventB tool, allowing hence the generation of an Event-B refinement architecture from a SysML/KAOS functional goal model. This implementation is mainly based on the model-to-model transformation technologies

Dans cette thèse, nous avons étudié et développé un environnement de preuve pour les algorithmes distribués. Nous avons choisi de combiner d’une part l’approche "correct-par-construction" basée sur la méthode "B évènementielle" et d’autre part les calculs locaux comme un outil de codage et de preuve d’algorithmes distribués. Ainsi, nous avons proposé un patron et une approche qui caractérisent d’une façon incrémentale une démarche générale de preuve de plusieurs classes d’algorithmes distribués. Les solutions proposées sont validées et implémentées par un outil de preuve appelé B2Visidia. / In this thesis, we have studied and developed a proof environment for distributed algorithms. We have chosen to combine the “correct-by-construction” approach based on the “Event-B” method and the local computations models. These models define abstract computing processes for solving problems by distributed algorithms. Thus, we have proposed a pattern and an approach to characterize a general approach to prove several classes of distributed algorithms. The proposed solutions are implemented by a tool called B2Visidia.