Vérification Formelle et Incrémentale de Spécifications SysML pour la Conception de Systèmes à Base de ComposantsLe travail présenté dans cette thèse est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisé avec le langage SysML. Les SBC sont largement utilisés dans le domaine industrielet ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l'utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en {\oe}uvre d'approches plus rigoureuses.Pour faciliter la communication entre les différentes parties impliquées dans le développement d'un SBC, un des langages largement utilisé est SysML, qui permet de modéliser, en plus de la structure et le comportement du système, aussi ses exigences. Il offre un standard de modélisation, spécification et documentation de systèmes, dans lequel il est possible de développer un système, partant d'un niveau abstrait, vers des niveaux plus détaillés pouvant aboutir à une implémentation. %Généralement ces systèmes sont faits plus grands parce qu'ils sont développés avec des cadres logiciels.Dans ce contexte nous avons traité principalement deux problématiques.La première est liée au développement par raffinement d'un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu'une composition d'un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d'un SBC. Dans cette contribution, nous exploitons les outils: Ptolemy pour la vérification de la compatibilité des composants assemblés, et l'outil MIO Workbench pour la vérification du raffinementLa deuxième problématique traitée concerne la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante: comment spécifier une architecture SBC qui satisfait toutes les exigences du système? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d'interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le model-checker SPIN et la LTL pour spécifier et vérifier les exigences.Mots clés: {Modélisation, Spécifications SysML, Architecture SBC, Raffinement, Compatibilité, Exigences, Propriétés LTL, Promela/SPIN, Ptolemy, MIO Workbench} / Formal and Incremental Verification of SysML Specifications for the Design of Component-Based SystemsThe work presented in this thesis is a contribution to the specification and verification of Component-Based Systems (CBS) modeled in SysML. CBS are widely used on the industrial field, and they are built by assembling various reusable components, allowing developing complex systems at lower cost.Despite the success of the use of CBS, their design is an increasingly complex step that requires the implementation of more rigorous approaches.To ease the communication between the various stakeholders in a CBS development project, one of the widely used modeling languages is SysML, which besides allowing modeling of structure and behavior, it has capabilities to model requirements. It offers a standard for modeling, specifying and documenting systems, wherein it is possible to develop a system, starting from an abstract level, to more detailed levels that may lead to an implementation.In this context, we have dealt mainly two issues. The first one concerns the development by refinement of a CBS, which is described only by its SysML interfaces and behavior protocols. Our contribution allows the designer of CBS to formally ensure that a composition of a set of elementary and reusable components refines an abstract specification of a CBS. In this contribution, we use the tools: Ptolemy for the verification of compatibility of the assembled components and MIO Workbench for refinement verification.The second one concerns the difficulty to decide what to build and how to build it, considering only system requirements and reusable components. Therefore, the question that arises is: how to specify a CBS architecture, which satisfies all system requirements? We propose a formal and incremental verification approach based on SysML models and interface automata to guide, by the requirements, the CBS designer to define a coherent system architecture that satisfies all proposed SysML requirements. In this approach we use the SPIN model-checker and LTL properties to specify and verify requirements.Keywords: {Modeling, SysML specifications, CBS architecture, Refinement, Compatibility, Requirements, LTL properties, Promela/SPIN, Ptolemy, MIO Workbench}

Le calcul d'écoulements dans les générateurs de vapeur des réacteurs à eau pressurisée est un problème complexe, faisant intervenir différents régimes d'écoulement et plusieurs échelles de temps et d'espace. Un scénario accidentel peut être caractérisé par des variations très rapides pour un nombre de Mach de l'ordre de l'unité. A l'inverse en régime nominal l'écoulement peut être stationnaire, à bas nombre de Mach. De plus quelque soit le régime considéré, la complexité de la géométrie d'un générateur de vapeur conduit à modéliser le faisceau de tubes par un milieu poreux, d'où le problème de couplage à l'interface avec le milieu fluide.Un schéma de correction de pression tout-Mach en volumes finis colocalisés a été introduit pour les équations d'Euler et de Navier-Stokes. L'existence d'une solution discrète, la consistance du schéma au sens de Lax et la positivité de l'énergie interne ont été démontrées. Le schéma a été ensuite étendu aux modèles diphasiques homogènes du code GENEPI développé au CEA. Enfin un algorithme Multigrille-AMR a été adaptée pour permettre de mettre en oeuvre notre schéma sur des maillages adaptatifs.Concernant la seconde problématique, une extension de la loi de Beavers-Joseph a été proposée pour le régime convectif. En introduisant un saut d'énergie cinétique à l'interface, on retrouve une loi de type Beavers-Joseph mais avec un coefficient de glissement non-linéaire, qui dépend de la vitesse fluide à l'interface et de la vitesse Darcy. La validité de cette nouvelle condition d'interface a été évaluée en réalisant des calculs de simulation numérique directe à différents nombres de Reynolds. / The numerical simulation of steam generators of pressurized water reactors is a complex problem, involving different flow regimes and a wide range of length and time scales. An accidental scenario may be associated with very fast variations of the flow with an important Mach number. In contrast in the nominal regime the flow may be stationary, at low Mach number. Moreover whatever the regime under consideration, the array of U-tubes is modelled by a porous medium in order to avoid taking into account the complex geometry of the steam generator, which entails the issue of the coupling conditions at the interface with the free-fluid.We propose a new pressure-correction scheme for cell-centered finite volumes for solving the compressible Navier-Stokes and Euler equations at all Mach number. The existence of a discrete solution, the consistency of the scheme in the Lax sense and the positivity of the internal energy were proved. Then the scheme was extended to the homogeneous two-phase flow models of the GENEPI code developed at CEA. Lastly a multigrid-AMR algorithm was adapted for using our pressure-correction scheme on adaptive grids.Regarding the second issue addressed in this work, an extension to the Beavers-Joseph law was proposed for the convective regime. By introducing a jump in the kinetic energy at the interface, we recover an interface condition close to the Beavers-Joseph law but with a non-linear slip coefficient, which depends on the free-fluid velocity at the interface and on the Darcy velocity. The validity of this new transmission condition was assessed with direct numerical simulations at different Reynolds numbers.

<P align="justify">Model-checking is an automated technique which aims at verifying properties of computer systems. A model-checker is fed with a model of the system (which capture all its possible behaviors) and a property to verify on this model. Both are given by a convenient mathematical formalism like, for instance, a transition system for the model and a temporal logic formula for the property.</P><p><p><P align="justify">For several reasons (the model-checking is undecidable for this class of model or the model-checking needs too much resources for this model) model-checking may not be applicable. For safety properties (which basically says "nothing bad happen"), a solution to this problem uses a simpler model for which model-checkers might terminate without too much resources. This simpler model, called the abstract model, over-approximates the behaviors of the concrete model. However the abstract model might be too imprecise. In fact, if the property is true on the abstract model, the same holds on the concrete. On the contrary, when the abstract model violates the property, either the violation is reproducible on the concrete model and so we found an error; or it is not reproducible and so the model-checker is said to be inconclusive. Inconclusiveness stems from the over-approximation of the concrete model by the abstract model. So a precise model yields the model-checker to conclude, but precision comes generally with an increased computational cost.</P><p><p><P align="justify">Recently, a lot of work has been done to define abstraction refinement algorithms. Those algorithms compute automatically abstract models which are refined as long as the model-checker is inconclusive. In the thesis, we give a new abstraction refinement algorithm which applies for safety properties. We compare our algorithm with previous attempts to build abstract models automatically and show, using formal proofs that our approach has several advantages. We also give several extensions of our algorithm which allow to integrate existing techniques used in model-checking such as acceleration techniques.</P><p><p><P align="justify">Following a rigorous methodology we then instantiate our algorithm for a variety of models ranging from finite state transition systems to infinite state transition systems. For each of those models we prove the instantiated algorithm terminates and provide encouraging preliminary experimental results.</P><p><br><p><br><p><P align="justify">Le model-checking est une technique automatisée qui vise à vérifier des propriétés sur des systèmes informatiques. Les données passées au model-checker sont le modèle du système (qui en capture tous les comportements possibles) et la propriété à vérifier. Les deux sont donnés dans un formalisme mathématique adéquat tel qu'un système de transition pour le modèle et une formule de logique temporelle pour la propriété.</P><p><p><P align="justify">Pour diverses raisons (le model-checking est indécidable pour cette classe de modèle ou le model-checking nécessite trop de ressources pour ce modèle) le model-checking peut être inapplicable. Pour des propriétés de sûreté (qui disent dans l'ensemble "il ne se produit rien d'incorrect"), une solution à ce problème recourt à un modèle simplifié pour lequel le model-checker peut terminer sans trop de ressources. Ce modèle simplifié, appelé modèle abstrait, surapproxime les comportements du modèle concret. Le modèle abstrait peut cependant être trop imprécis. En effet, si la propriété est vraie sur le modèle abstrait alors elle l'est aussi sur le modèle concret. En revanche, lorsque le modèle abstrait enfreint la propriété :soit l'infraction peut être reproduite sur le modèle concret et alors nous avons trouvé une erreur ;soit l'infraction ne peut être reproduite et dans ce cas le model-checker est dit non conclusif. Ceci provient de la surapproximation du modèle concret faite par le modèle abstrait. Un modèle précis aboutit donc à un model-checking conclusif mais son coût augmente avec sa précision.</P><p><P align="justify">Récemment, différents algorithmes d'abstraction raffinement ont été proposés. Ces algorithmes calculent automatiquement des modèles abstraits qui sont progressivement raffinés jusqu'à ce que leur model-checking soit conclusif. Dans la thèse, nous définissons un nouvel algorithme d'abstraction raffinement pour les propriétés de sûreté. Nous comparons notre algorithme avec les algorithmes d'abstraction raffinement antérieurs. A l'aide de preuves formelles, nous montrons les avantages de notre approche. Par ailleurs, nous définissons des extensions de l'algorithme qui intègrent d'autres techniques utilisées en model-checking comme les techniques d'accélérations.</P><p><P align="justify">Suivant une méthodologie rigoureuse, nous instancions ensuite notre algorithme pour une variété de modèles allant des systèmes de transitions finis aux systèmes de transitions infinis. Pour chacun des modèles nous établissons la terminaison de l'algorithme instancié et donnons des résultats expérimentaux préliminaires encourageants.</P><p><p> / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Ce travail de thèse s’inscrit dans le cadre de l’étude de l’Interaction mécanique Pastille-Gaine (IPG) se produisant dans les crayons combustibles des réacteurs à eau pressurisée. Ce mémoire porte sur le développement de méthodes de raffinement de maillage permettant de simuler plus précisément le phénomène d’IPG tout en conservant des temps de calcul et un espace mémoire acceptables pour des études industrielles. Une stratégie de raffinement automatique basée sur la combinaison de la méthode multi-grilles Local Defect Correction (LDC) et l’estimateur d’erreur a posteriori de type Zienkiewicz et Zhu est proposée. Cette stratégie s’appuie sur l’erreur fournie par l’estimateur pour détecter les zones à raffiner constituant alors les sous-grilles locales de la méthode LDC. Plusieurs critères d’arrêt sont étudiés afin de permettre de stopper le raffinement quand la solution est suffisamment précise ou lorsque le raffinement n’apporte plus d’amélioration à la solution globale.Les résultats numériques obtenus sur des cas tests 2D élastiques avec discontinuité de chargement permettent d’apprécier l’efficacité de la stratégie proposée.Le raffinement automatique de maillage dans le cas de problèmes de contact unilatéral est ensuite abordé. La stratégie proposée dans ce travail s’étend aisément au raffinement multi-corps à condition d’appliquer l’estimateur d’erreur sur chacun des corps séparément. Un post-traitement est cependant souvent nécessaire pour garantir la conformité des zones de raffinement vis-à-vis des frontières de contact. Une variété de tests numériques de contact entre solides élastiques confirme l’efficacité et la généricité de la stratégie proposée. / This Ph.D. work takes place within the framework of studies on Pellet-Cladding mechanical Interaction (PCI) which occurs in the fuel rods of pressurized water reactor. This manuscript focuses on automatic mesh refinement to simulate more accurately this phenomena while maintaining acceptable computational time and memory space for industrial calculations. An automatic mesh refinement strategy based on the combination of the Local Defect Correction multigrid method (LDC) with the Zienkiewicz and Zhu a posteriori error estimator is proposed. The estimated error is used to detect the zones to be refined, where the local subgrids of the LDC method are generated. Several stopping criteria are studied to end the refinement process when the solution is accurate enough or when the refinement does not improve the global solution accuracy anymore.Numerical results for elastic 2D test cases with pressure discontinuity shows the efficiency of the proposed strategy.The automatic mesh refinement in case of unilateral contact problems is then considered. The strategy previously introduced can be easily adapted to the multibody refinement by estimating solution error on each body separately. Post-processing is often necessary to ensure the conformity of the refined areas regarding the contact boundaries. A variety of numerical experiments with elastic contact (with or without friction, with or without an initial gap) confirms the efficiency and adaptability of the proposed strategy.

L'hyperdéformation est une technique efficace pour transformer la microstructure des métaux en une structure de grain de taille inférieure au micron ou même en nanostructure (<100 nm). Cette très petite taille de grain confère d'excellentes propriétés mécaniques au matériau. Dans ce travail de thèse, deux techniques d'hyperdéformation récemment développées, appelées High Pressure Tube Twisting (HPTT) and Cyclic Expansion and Extrusion (CEE) ont été appliquées à température ambiante sur différents matériaux métalliques. La fragmentation de la microstructure ainsi que le développement de la texture cristallographique ont été analysés en détails par la diffraction d'électrons rétrodiffusés (EBSD), par microscopie électronique en transmission (TEM), par transmission Kikuchi diffraction (TKD) ainsi que par diffraction des rayons X (XRD). Le gradient de déformation de cisaillement dans l'épaisseur des tubes d'aluminium déformés par HPTT a été déterminé par une méthode de mesure locale du cisaillement. Ce gradient de cisaillement induit une hétérogénéité aussi bien de microstructure que de texture dans les échantillons d'aluminium et de magnésium purs ainsi que dans l'alliage Al-4%Mg en solution solide. La micro-dureté et la taille de grain dans différentes zones ont été mesurées et analysées en fonction du taux cisaillement local. Les tailles de grain limites atteintes de façon stationnaire pour ces différents matériaux produit par HPTT sont respectivement de 700 nm, 900 nm et 100 nm. L'évolution de texture du magnésium pur après HPTT jusqu'à un cisaillement de 16 a été simulée par cisaillement simple par le model auto-cohérent (VPSC), le résultat de simulation a montré de bons accords avec les mesures de texture obtenues par XRD. Sur la base des mesures de distribution de désorientation dans l'aluminium déformé par HPTT, une nouvelle technique de détermination du taux de cisaillement local dans les procédés d'hyper déformation a été proposée. Cette nouvelle technique a été appliquée sur deux échantillons d'aluminium produit par twist extrusion (TE) et par torsion à extrémités libres. Les échantillons d'aluminium et de cuivre ont été déformés intensément par CEE. Les évolutions de texture et de microstructures ont été mesurées par EBSD, montrant un gradient du centre à la périphérie des échantillons cylindriques. L'évolution de texture dans le cuivre déformé par CEE a été simulée par le modèle VPSC en utilisant un modèle de ligne de courant pour décrire la déformation dans le procédé. Les résultats de simulation confirment les caractéristiques de la texture expérimentale observées après CEE. Le comportement en traction du cuivre pré-déformé par grande déformation en torsion a ensuite été testé. En dépit du gradient de cisaillement existant dans la barre, une technique a été proposée pour obtenir la courbe contrainte-déformation pour ce type de matériau. / Severe plastic deformation (SPD) is an efficient technique to transform the microstructure of bulk metals into ultra fine grained structure with grain sizes less than 1 µm or even into nanostructure with nano-grains of less than 100 nm in diameter. The very small grain size attributes excellent mechanical properties to the material. In present thesis work, two recently developed SPD techniques, namely, High Pressure Tube Twisting (HPTT) and Cyclic Expansion and Extrusion (CEE) were performed on different metallic materials at room temperature. Details of fragmentation of microstructure and metallographic texture evolution were investigated by electron backscattered diffraction (EBSD), transmission electron microscopy (TEM), transmission kikuchi diffraction (TKD) and X-ray diffraction (XRD). Shear strain gradient across the thickness of the HPTT deformed Al tube sample was found by a local shear measurement method. This shear strain gradient induced the inhomogeneity of microstructure and texture in HPTT deformed pure Al, solid solution alloy Al-4%Mg and pure Mg. The microhardness and average grain size in different zones as a function of shear strain were measured. The limiting steady grain sizes in the steady state for these different materials produced by HPTT were 700 nm, 100 nm and 900 nm, respectively. The texture evolution of pure Mg in HPTT up to a shear strain of 16 was simulated in simple shear using the self-consistent (VPSC) polycrystal model and showed good agreements with the experimental results measured by XRD. Based on the measured disorientation distribution function in HPTT deformed Al, a new technique for the magnitude of local shear strain in SPD was proposed. This new technique was applied to a protrusion produced in twist extrusion (TE) and to an Al sample deformed in free-end torsion. Cu and pure Al samples were intensively deformed by the CEE SPD technique. The microstructure and texture evolutions were measured by EBSD, showing a gradient from the center-zone to the edge part of the rod sample. The texture evolution of CEE deformed Cu was simulated by the VPSC polycrystal model using a flow line function. The simulation results confirmed the experimental texture features observed in the CEE process. The tensile testing behavior of large strain torsion pre-processed Cu was examined. In spite of the shear strain gradient existing in the bar, a technique was proposed to obtain the tensile stress-strain curve of such gradient material.

L’adaptation de maillage est un outil puissant pour l’obtention de simulations aérodynamiques précises à coût limité. Dans le cas particulier des simulations visant au calcul de fonctions aérodynamiques (efforts, moments, rendements...), plusieurs méthodes dites de raffinement ciblé (ou, en anglais, « goal-oriented ») basées sur le vecteur adjoint de la fonction d’intérêt ont été proposées. L’objectif de la thèse est l’extension d’une méthode de ce type basée sur la dérivée totale dJ/dX de la grandeur aérodynamique d’intérêt, J, par rapport aux coordonnées du maillage volumique, X. Les trois méthodes usuelles de calcul de gradient discret – la méthode de différentiation directe, la méthode adjointe-"paramètres" et la méthode adjointe-"maillage" évaluant dJ/dX – ont tout d’abord été étudiées et codées dans le logiciel elsA de l’ONERA pour des maillages non-structurés, pour des écoulements compressibles de fluide parfait et des écoulements laminaires. La seconde étape du travail a consisté à créer un senseur local θ basé sur dJ/dX qui identifie les zones du maillage volumique où la position des nœuds a une forte incidence sur l’évaluation de la fonction J. Ce senseur sert d’indicateur pour l’adaptation de différents maillages, pour différents régimes d’écoulement (subsonique, transsonique, supersonique), pour des configurations d’aérodynamique interne (aube et tuyère) et externe (profil d’aile). La méthode proposée est comparée à une méthode de raffinement ciblée très populaire (Venditti et Darmofal, 2001) et à une méthode de raffinement basée sur les caractéristiques de l’écoulement (ou, en anglais, « feature-based ») ; elle conduit à des résultats très satisfaisants. / Mesh adaptation is a powerful tool to obtain accurate aerodynamic simulations with limited cost. In the specific case of computation of aerodynamic functions (forces, moments, efficiency ...), goal-oriented methods based on the adjoint vector have been proposed. The aim of the thesis is the extension of a method of this type based on the total derivative dJ/dX of the aerodynamic output of interest, J, with respect to the volume mesh coordinates, X. The three common methods for calculating discrete gradient – the direct differentiation method, the parameter-adjoint method and mesh-adjoint method evaluating dJ/dX – have been studied first and coded in the elsA ONERA software for unstructured grids, for compressible inviscid and laminar flows. The second part of this work was has been to define a local sensor θ based on dJ/dX in order to identify zones where the volume mesh nodes position has a strong impact on the evaluation of the function J. This sensor is the selected indicator for different mesh adaptations for different flow regimes (subsonic, transonic, supersonic) for internal (blade and nozzle) and external (wing profile) aerodynamic configurations. The proposed method is compared to a well-known goal-oriented method (Darmofal and Venditti, 2001) and to a feature-based method ; it leads to very consistent results. very consistent results.

L'imagerie de perfusion permet un accès non invasif à la micro-vascularisation tissulaire. Elle apparaît comme un outil prometteur pour la construction de biomarqueurs d'imagerie pour le diagnostic, le pronostic ou le suivi de traitement anti-angiogénique du cancer. Cependant, l'analyse quantitative des séries dynamiques de perfusion souffre d'un faible rapport signal sur bruit (SNR). Le SNR peut être amélioré en faisant la moyenne de l'information fonctionnelle dans de grandes régions d'intérêt, qui doivent néanmoins être fonctionnellement homogènes. Pour ce faire, nous proposons une nouvelle méthode pour la segmentation automatique des séries dynamiques de perfusion en régions fonctionnellement homogènes, appelée DCE-HiSET. Au coeur de cette méthode, HiSET (Hierarchical Segmentation using Equivalence Test ou Segmentation hiérarchique par test d'équivalence) propose de segmenter des caractéristiques fonctionnelles ou signaux (indexées par le temps par exemple) observées discrètement et de façon bruité sur un espace métrique fini, considéré comme un paysage, avec un bruit sur les observations indépendant Gaussien de variance connue. HiSET est un algorithme de clustering hiérarchique qui utilise la p-valeur d'un test d'équivalence multiple comme mesure de dissimilarité et se compose de deux étapes. La première exploite la structure de voisinage spatial pour préserver les propriétés locales de l'espace métrique, et la seconde récupère les structures homogènes spatialement déconnectées à une échelle globale plus grande. Etant donné un écart d'homogénéité $\delta$ attendu pour le test d'équivalence multiple, les deux étapes s'arrêtent automatiquement par un contrôle de l'erreur de type I, fournissant un choix adaptatif du nombre de régions. Le paramètre $\delta$ apparaît alors comme paramètre de réglage contrôlant la taille et la complexité de la segmentation. Théoriquement, nous prouvons que, si le paysage est fonctionnellement constant par morceaux avec des caractéristiques fonctionnelles bien séparées entre les morceaux, HiSET est capable de retrouver la partition exacte avec grande probabilité quand le nombre de temps d'observation est assez grand. Pour les séries dynamiques de perfusion, les hypothèses, dont dépend HiSET, sont obtenues à l'aide d'une modélisation des intensités (signaux) et une stabilisation de la variance qui dépend d'un paramètre supplémentaire $a$ et est justifiée a posteriori. Ainsi, DCE-HiSET est la combinaison d'une modélisation adaptée des séries dynamiques de perfusion avec l'algorithme HiSET. A l'aide de séries dynamiques de perfusion synthétiques en deux dimensions, nous avons montré que DCE-HiSET se révèle plus performant que de nombreuses méthodes de pointe de clustering. En terme d'application clinique de DCE-HiSET, nous avons proposé une stratégie pour affiner une région d'intérêt grossièrement délimitée par un clinicien sur une série dynamique de perfusion, afin d'améliorer la précision de la frontière des régions d'intérêt et la robustesse de l'analyse basée sur ces régions tout en diminuant le temps de délimitation. La stratégie de raffinement automatique proposée est basée sur une segmentation par DCE-HiSET suivie d'une série d'opérations de type érosion et dilatation. Sa robustesse et son efficacité sont vérifiées grâce à la comparaison des résultats de classification, réalisée sur la base des séries dynamiques associées, de 99 tumeurs ovariennes et avec les résultats de l'anapathologie sur biopsie utilisés comme référence. Finalement, dans le contexte des séries d'images 3D, nous avons étudié deux stratégies, utilisant des structures de voisinage des coupes transversales différentes, basée sur DCE-HiSET pour obtenir la segmentation de séries dynamiques de perfusion en trois dimensions. (...) / Dynamical contrast enhanced (DCE) imaging allows non invasive access to tissue micro-vascularization. It appears as a promising tool to build imaging biomarker for diagnostic, prognosis or anti-angiogenesis treatment monitoring of cancer. However, quantitative analysis of DCE image sequences suffers from low signal to noise ratio (SNR). SNR may be improved by averaging functional information in large regions of interest, which however need to be functionally homogeneous. To achieve SNR improvement, we propose a novel method for automatic segmentation of DCE image sequence into functionally homogeneous regions, called DCE-HiSET. As the core of the proposed method, HiSET (Hierarchical Segmentation using Equivalence Test) aims to cluster functional (e.g. with respect to time) features or signals discretely observed with noise on a finite metric space considered to be a landscape. HiSET assumes independent Gaussian noise with known constant level on the observations. It uses the p-value of a multiple equivalence test as dissimilarity measure and consists of two steps. The first exploits the spatial neighborhood structure to preserve the local property of the metric space, and the second recovers (spatially) disconnected homogeneous structures at a larger (global) scale. Given an expected homogeneity discrepancy $\delta$ for the multiple equivalence test, both steps stop automatically through a control of the type I error, providing an adaptive choice of the number of clusters. Parameter $\delta$ appears as the tuning parameter controlling the size and the complexity of the segmentation. Assuming that the landscape is functionally piecewise constant with well separated functional features, we prove that HiSET will retrieve the exact partition with high probability when the number of observation times is large enough. In the application for DCE image sequence, the assumption is achieved by the modeling of the observed intensity in the sequence through a proper variance stabilization, which depends only on one additional parameter $a$. Therefore, DCE-HiSET is the combination of this DCE imaging modeling step with our statistical core, HiSET. Through a comparison on synthetic 2D DCE image sequence, DCE-HiSET has been proven to outperform other state-of-the-art clustering-based methods. As a clinical application of DCE-HiSET, we proposed a strategy to refine a roughly manually delineated ROI on DCE image sequence, in order to improve the precision at the border of ROIs and the robustness of DCE analysis based on ROIs, while decreasing the delineation time. The automatic refinement strategy is based on the segmentation through DCE-HiSET and a series of erosion-dilation operations. The robustness and efficiency of the proposed strategy are verified by the comparison of the classification of 99 ovarian tumors based on their associated DCE-MR image sequences with the results of biopsy anapathology used as benchmark. Furthermore, DCE-HiSET is also adapted to the segmentation of 3D DCE image sequence through two different strategies with distinct considerations regarding the neighborhood structure cross slices. This PhD thesis has been supported by contract CIFRE of the ANRT (Association Nationale de la Recherche et de la Technologie) with a french company INTRASENSE, which designs, develops and markets medical imaging visualization and analysis solutions including Myrian®. DCE-HiSET has been integrated into Myrian® and tested to be fully functional.

Software tools are being used by experts in a variety of domains. There are numerous software modeling environments tailored to a specific domain expertise. However, there is no consistent approach to generically synthesize a product line of such modeling environments that also take into account the user interaction and experience adapted to the domain. The focus of my thesis is the proposal of a solution to explicitly model user interfaces and interaction of modeling environments so that they can be tailored to the habits and preferences of domain experts. We extend current model-driven engineering techniques that synthesize graphical modeling environments to also take interaction models into account. The formal semantics of our language framework is based on statecharts. We define a development process for generating such modeling environments to maximize reuse through a novel statechart refinement technique. / Les outils logiciels sont utilisés par des experts dans une variété de domaines. Il existe de nombreux environnements de modélisation logicielle adaptés á une expertise spécifique. Cependant, il n’existe pas d’approche cohérente pour synthétiser génériquement une ligne de produits de tels environnements de modélisation qui prennent également en compte l’interaction et l’expérience utilisateur adaptées au domaine. L’objectif de ma thése est la proposition d’une solution pour modéliser explicitement les interfaces utilisateur et l’interaction des environnements de modélisation afin qu’ils puissent étre adaptés aux habitudes et aux préférences des experts du domaine. Nous étendons les techniques d’ingénierie actuelles pilotées par un modéle qui synthétisent des environnements de modélisation graphique pour prendre également en compte les modèles d’interaction. La sémantique formelle de notre cadre linguistique est basée sur des statecharts. Nous définissons un processus de développement pour générer de tels environnements de modélisation afin de maximiser la réutilisation à travers une nouveau technique de raffinement de statecharts.

Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande échelle, ce qui pose deux questions : sait-on les programmer de façon simple et modulaire ? sait-on ensuite exécuter ces programmes efficacement ? Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sûreté des programmes dans le langage étendu. Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.

La méthode d'intégration produit a été proposée pour résoudre des équations linéaires de Fredholm de deuxième espèce singulières dont la solution exacte est régulière, au moins continue. Dans ce travail on adapte cette méthode à des équations dont la solution est juste intégrable. On étudie également son extension au cas non linéaire posé dans l'espace des fonctions intégrables. Ensuite, on propose une autre manière de mettre en oeuvre la méthode d'intégration produit : on commence par linéariser l'équation par une méthode de type Newton puis on discrétise les itérations de Newton par la méthode d'intégration produit / The product integration method has been proposed for solving singular linear Fredholm equations of the second kind whose exact solution is smooth, at least continuous. In this work, we adapt this method to the case where the solution is only integrable. We also study the nonlinear case in the space of integrable functions. Then, we propose a new version of the method in the nonlinear framework : we first linearize the eqaution by a Newton type method and then discretize the Newton iterations by the product integration method