Le but de cette étude est d'améliorer les performances, en termes d'espace mémoire et de temps de calcul, des simulations actuelles de l'Interaction mécanique Pastille-Gaine (IPG), phénomène complexe pouvant avoir lieu lors de fortes montées en puissance dans les réacteurs à eau sous pression. Parmi les méthodes de raffinement de maillage, méthodes permettant de simuler efficacement des singularités locales, une approche multi-grille locale a été choisie car elle présente l'intérêt de pouvoir utiliser le solveur en boîte noire tout en ayant un faible nombre de degrés de liberté à traiter par niveau. La méthode Local Defect Correction (LDC), adaptée à une discrétisation de type éléments finis, a tout d'abord été analysée et vérifiée en élasticité linéaire, sur des configurations issues de l'IPG, car son utilisation en mécanique des solides est peu répandue. Différentes stratégies concernant la mise en oeuvre pratique de l'algorithme multi-niveaux ont également été comparées. La combinaison de la méthode LDC et de l'estimateur d'erreur a posteriori de Zienkiewicz-Zhu, permettant d'automatiser la détection des zones à raffiner, a ensuite été testée. Les performances obtenues sur des cas bidimensionnels et tridimensionnels sont très satisfaisantes, l'algorithme proposé se montrant plus performant que des méthodes de raffinement h-adaptatives. Enfin, l'algorithme a été étendu à des problèmes mécaniques non linéaires. Les questions d'un raffinement espace/temps mais aussi de la transmission des conditions initiales lors du remaillage ont entre autres été abordées. Les premiers résultats obtenus sont encourageants et démontrent l'intérêt de la méthode LDC pour des calculs d'IPG. / The aim of this study is to improve the performances, in terms of memory space and computational time, of the current modelling of the Pellet-Cladding mechanical Interaction (PCI),complex phenomenon which may occurs during high power rises in pressurised water reactors. Among the mesh refinement methods - methods dedicated to efficiently treat local singularities - a local multi-grid approach was selected because it enables the use of a black-box solver while dealing few degrees of freedom at each level. The Local Defect Correction (LDC) method, well suited to a finite element discretisation, was first analysed and checked in linear elasticity, on configurations resulting from the PCI, since its use in solid mechanics is little widespread. Various strategies concerning the implementation of the multilevel algorithm were also compared. Coupling the LDC method with the Zienkiewicz-Zhu a posteriori error estimator in orderto automatically detect the zones to be refined, was then tested. Performances obtained on two-dimensional and three-dimensional cases are very satisfactory, since the algorithm proposed is more efficient than h-adaptive refinement methods. Lastly, the LDC algorithm was extended to nonlinear mechanics. Space/time refinement as well as transmission of the initial conditions during the remeshing step were looked at. The first results obtained are encouraging and show the interest of using the LDC method for PCI modelling.

Malgré l'efficacité informatique et la faible dissipation numérique de la méthode de Boltzmann sur réseau (LBM) classique reposant sur un algorithme de propagation-collision, cette méthode est limitée aux maillages cartésiens uniformes. L'adaptation de l'étape de discrétisation à différentes échelles de la mécanique des fluides est généralement réalisée par des schémas LBM à échelles multiples, dans lesquels le domaine de calcul est décomposé en plusieurs sous-domaines uniformes avec différentes résolutions spatiales et temporelles. Pour des raisons de connectivité, le facteur de résolution des sous-domaines adjacents doit être un multiple de deux, introduisant un changement abrupt des échelles spatio-temporelles aux interfaces. Cette spécificité peut déclencher des instabilités numériques et produire des sources de bruit parasite rendant l'exploitation de simulations à finalités aéroacoustiques impossible. Dans la présente thèse, nous avons d'abord élucidé le sujet du raffinement de maillage dans la LBM classique en soulignant les défis et les sources potentielles d'erreur. Par la suite, une méthode de Boltzmann sur réseau hybride (HLBM) est proposée, combinant l'algorithme de propagation-collision avec un algorithme de flux au sens eulérien obtenu à partir d'une discrétisation en volumes finis des équations de Boltzmann à vitesse discrète. La HLBM combine à la fois les avantages de la LBM classique et une flexibilité géométrique accrue. La HLBM permet d'utiliser des maillages cartésiens non-uniformes. La validation de la méthode hybride sur des cas tests 2D à finalité aéroacoustique montre qu'une telle approche constitue une alternative viable aux schémas Boltzmann sur réseau à échelles multiples, permettant de réaliser des raffinements locaux en H. Enfin, un couplage original, basé sur l'algorithme de propagation-collision et une formulation isotherme des équations de Navier-Stokes en volumes finis, est proposé. Une telle tentative présente l'avantage de réduire le nombre d'équations du solveur volumes finis tout en augmentant la stabilité numérique de celui-ci, en raison d'une condition CFL plus favorable. Les deux solveurs sont couplés dans l'espace des moments, où la solution macroscopique du solveur Navier-Stokes est injectée dans l'algorithme de propagation-collision à l'aide de la collision des moments centrés. La faisabilité d'un tel couplage est démontrée sur des cas tests 2D, et les résultas obtenus sont comparés avec la HLBM. / Despite the inherent efficiency and low dissipative behaviour of the standard lattice Boltzmann method (LBM) relying on a two step stream and collide algorithm, a major drawback of this approach is the restriction to uniform Cartesian grids. The adaptation of the discretization step to varying fluid dynamic scales is usually achieved by multi-scale lattice Boltzmann schemes, in which the computational domain is decomposed into multiple uniform subdomains with different spatial resolutions. For the sake of connectivity, the resolution factor of adjacent subdomains has to be a multiple of two, introducing an abrupt change of the space-time discretization step at the interface that is prone to trigger instabilites and generate spurious noise sources that contaminate the expected physical pressure signal. In the present PhD thesis, we first elucidate the subject of mesh refinement in the standard lattice Boltzmann method and point out challenges and potential sources of error. Subsequently, we propose a novel hybrid lattice Boltzmann method (HLBM) that combines the stream and collide algorithm with an Eulerian flux-balance algorithm that is obtained from a finite-volume discretization of the discrete velocity Boltzmann equations. The interest of a hybrid lattice Boltzmann method is the pairing of efficiency and low numerical dissipation with an increase in geometrical flexibility. The HLBM allows for non-uniform grids. In the scope of 2D periodic test cases, it is shown that such an approach constitutes a valuable alternative to multi-scale lattice Boltzmann schemes by allowing local mesh refinement of type H. The HLBM properly resolves aerodynamics and aeroacoustics in the interface regions. A further part of the presented work examines the coupling of the stream and collide algorithm with a finite-volume formulation of the isothermal Navier-Stokes equations. Such an attempt bears the advantages that the number of equations of the finite-volume solver is reduced. In addition, the stability is increased due to a more favorable CFL condition. A major difference to the pairing of two kinetic schemes is the coupling in moment space. Here, a novel technique is presented to inject the macroscopic solution of the Navier-Stokes solver into the stream and collide algorithm using a central moment collision. First results on 2D tests cases show that such an algorithm is stable and feasible. Numerical results are compared with those of the previous HLBM.

Nous explorons les propriétés structurales de nanoparticules cœur-coquille, avec un cœur de ferrite MFe2O4 (M = Mn et Co) ou de ferrite mixte Mn-Zn. Ces nanoparticules sont obtenues par co-précipitation hydrothermique et sont dispersées en milieu acide par un traitement de surface empirique au nitrate ferrique, protégeant les nanograins contre une dissociation chimique par une fine couche superficielle de maghémite. La fraction volumique du cœur, de la coquille et l’épaisseur de la couche superficielle sont déterminées par dosage chimique. Nous suivons les changements structurels des nanocristaux de MnFe2O4 et CoFe2O4, pendant la durée du traitement de surface, tandis que ceux des nanoparticules de ferrite mixte Mn-Zn sont étudiés en fonction de leur teneur en zinc. Diffraction de rayons-x et de neutrons sont utilisées pour déterminer les paramètres de structure, en particulier la diffusion de cations dans les interstices de la ferrite spinelle. Pour un haut degré de fiabilité, des raffinements de Rietveld sont réalisés. Les distances inter-atomiques, l’état d’oxydation moyen et le degré d’inversion sont déterminés par spectroscopie d’absorption des rayons-x. Morphologie, cristallinité et taille des nanoparticules de ferrite mixte Mn-Zn sont étudiées par TEM/HRTEM et par diffraction des électrons. Dans les nanoparticules MnFe2O4 et de ferrite mixte Mn-Zn, on constate la présence de cations Mn3+ en environnement octaédrique, responsables de déformations anisotropes (effet Jahn-Teller). Le degré d’inversion obtenu ici diffère de celui du bulk en raison de la réduction à l’échelle nanométrique et de l'augmentation du rapport surface/volume pendant le processus de synthèse. / Structural properties of core-shell ferrite nanoparticles MFe2O4 (M = Mn and Co) and Mn-Zn ferrite nanoparticles are here investigated. The nanoparticles are synthesized by hydrothermal co-precipitation and are dispersed in acid medium thanks to an empirical surface treatment by ferric nitrate, which prevents the chemical dissociation by a thin maghemite layer incorporated at the surface of the nano-grains. Chemical titrations allow us to calculate volume fractions of core and shell, as well as the surface-layer thickness. Structural changes induced by the surface treatment are followed as a function of treatment duration in MnFe2O4 and CoFe2O4 nanocrystals. Whereas structural changes in Mn-Zn ferrite nanoparticles are investigated as a function of zinc content. X-ray and Neutron diffractions are used to determine the structural parameters, in particular cationic distribution in the spinel ferrite sites. Precise structural information with high degree of reliability is obtained by Rietveld refinements. To investigate the local structure of these materials, X-ray Absorption Spectroscopy measurements are performed, allowing determining interatomic distances, mean oxidation state and inversion degree. Morphology, crystallinity and size of mixed-ferrite nanoparticles are investigated by TEM/HRTEM and electron diffraction. In Mn-Zn ferrite nanoparticles, the presence of Mn3+ in octahedral environment is responsible for anisotropic distortions, known as Jahn-Teller effect. The inversion degree obtained in this work diverges from the bulk values due to the reduction to nanoscale and to the increase of the surface/volume ratio, associated to the synthesis process.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L’approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l’industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d’étude, qui s’inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d’une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d’écrire des programmes structurés en composants. L’introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d’alias, on risque de ne plus pouvoir garantir la validité de l’invariant de données d’une structure. Nous interdisons, alors l’aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s’inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d’obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d’obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s’apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu’aucun invariant de données n’est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l’affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d’un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires. / The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise between the complexe methods that exist in the literature and what is used in industry, reconciling lightness annotations and restrictions on the alias. We define, firstly, a language study, based on the C language, in which the only type of mutable data allowed is the type of structures, which can be accessed only through pointers. In order to structure our programs, we bring our language with a module notion and concepts issue from a refinement theory such as abstract variables that we formalize by model fields and gluing invariants. This allows us to write programs structured by components. Introducing invariants in our language raises issues related to aliasing. Indeed, in presence of alias, we might not be able to guarantee the validity of the invariant data structure. We forbid then the aliasing in our language. To control memory access, we define a type system based on the concept of regions. This contribution is based on the theory and refinement. It aims to make programs as modular as possible and proofs as automatic as possible. We define on this language, a mechanism for generation of proof obligations by proposing a weakest precondition calculus incorporating refinement. Next we prove the correction of this proof obligations generation mechnaism by an original method based on the concept of blocking semantic, which is similar to a proof of type soundness, and consists therefore, to proove the preservation and the progress of the defined calculus. Secondly, we extend our language by, partially, lifting the restrictions related to aliasing. We allow, in particular, sharing when no invariant is associated to the referenced data structure. In addition, we introduce the type of arrays, global variables, and assignment that are not part of the core language. For each of the extensions mentioned above, we extend the definition and correctness proof of the weakest precondition calculus accordingly. Finally, we propose an implementation of this approach as a Frama-C plugin(http ://frama-c.com/). We experimente our implantation on examples of modules implementing complex data structures, especially the challenges from the challenge VACID0 (http ://vacid. Codeplex.com /), namely sparse srrays and binary heaps.

La majorité des algorithmes de reconstruction de surface sont optimisés pour s'appliquer à des données de haute qualité. Les résultats obtenus peuvent alors être inutilisables si les données proviennent de solutions d'acquisition bon marché. Notre première contribution est un algorithme de reconstruction de surfaces à partir de données de stéréo vision. Il combine les informations liées aux points 3D avec les images calibrées afin de combler l'imprécision des données. L'algorithme construit une soupe de triangles 3D à l'aide des images calibrées et à l'issue d'une phase de prétraitement du nuage de points. Pour épouser au mieux la surface de la scène, on contraint cette soupe de triangle 3D à respecter des critères de visibilité et de photo-consistance. On calcule ensuite un maillage à partir de la soupe de triangles à l'aide d'une technique de reconstruction qui combine les triangulations de Delaunay contraintes et le raffinement de Delaunay. Notre seconde contribution est un algorithme qui construit, à partir d'un nuage de points 3D échantillonnés sur une surface, un maillage de surface qui représente fidèlement les arêtes vives. Cet algorithme génère un bon compromis entre précision et complexité du maillage. Dans un premier temps, on extrait une approximation des arêtes vives de la surface sous-jacente à partir du nuage de points. Dans un deuxième temps, on utilise une variante du raffinement de Delaunay pour générer un maillage qui combine les arêtes vives extraites avec une surface implicite obtenue à partir du nuage de points. Notre méthode se révèle flexible, robuste au bruit; cette méthode peut prendre en compte la résolution du maillage ciblé et un champ de taille défini par l'utilisateur. Nos deux contributions génèrent des résultats efficaces sur une variété de scènes et de modèles. Notre méthode améliore l'état de l'art en termes de précision.

Cette thèse est consacrée à l'étude de certains aspects numériques et mathématiques liés à la simulation d'écoulements incompressibles triphasiques à l'aide d'un modèle à interfaces diffuses de type Cahn-Hilliard/Navier-Stokes. La discrétisation spatiale est effectuée par éléments finis. La présence d'échelles très différentes dans le système suggère l'utilisation d'une méthode de raffinement local adaptatif. La procédure mise en place permet de tenir compte implicitement des non conformités des maillages générés, pour produire in fine des espaces d'approximation conformes. Nous montrons, en outre, qu'il est possible d'exploiter cette méthode pour construire des préconditionneurs multigrilles. Concernant la discrétisation en temps, notre étude a commencé par celle du système de Cahn-Hilliard. Pour remédier aux problèmes de convergence de la méthode de Newton utilisée pour résoudre ce système (non linéaire), nous proposons un schéma semi-implicite permettant de garantir la décroissance de l'énergie. Nous montrons l'existence et la convergence des solutions discrètes. Nous poursuivons ensuite cette étude en donnant une discrétisation en temps inconditionnellement stable du modèle complet Cahn-Hilliard/Navier-Stokes ne couplant pas fortement les deux systèmes. Nous montrons l'existence des solutions discrètes et, dans le cas où les trois fluides ont la même densité, nous montrons leur convergence. Nous étudions, pour terminer cette partie, diverses problématiques liées à l'utilisation de la méthode de projection incrémentale. Enfin, la dernière partie présente plusieurs exemples de simulations numériques, diphasiques et triphasiques, en deux et trois dimensions.

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

Cette thèse traite des problèmes des concentrations de contraintes locales, en particularité des effets des bords libres dans des structures stratifiés. À l'interface entre deux couches avec des propriétés élastiques différentes, les contraintes ont un comportement singulier dans le voisinage du bord libre en supposant un comportement de matériau élastique linéaire. Par conséquent, ils sont essentiels pour promouvoir le délaminage. Via Formulation unifiée de la Carrera (CUF) différents modèles cinématiques sont testés dans le but de capter les concentrations de contraintes. Dans la première partie de ce travail, les approches de modélisation dimensionnelle réduits sont comparées. Deux classe principale sont présentés: la couche équivalent (ESL) et l'approche par couche, LW. Par la suite leurs capacités à capter les singularités sont comparées. En utilisant une fonction a priori singulière, via une expression exponentielle, une mesure des contraintes singulières est introduite. Seulement deux paramètres décrivent pleinement les composantes des contraintes singulières au voisinage du bord libre. Sur la base des paramètres obtenus les modèles sont comparés et aussi les effets sous des charges d'extension et de flexion et pour différents stratifiés. Les résultats montrent une nécessité des modèles complexes dans le voisinage du bord libre. Cependant loin des bords libres, dans le centre de plaques composite, aucune différence significative ne peut être noté pour les modèles plutôt simples. La deuxième partie de ce travail est donc dédiée au couplage de modèles cinématique incompatibles. Modèles complexes et coûteux sont utilisés seulement dans des domaines locaux d'intérêt, tandis que les modèles économiques simples seront modéliser le domaine global. La eXtended Variational Formulation (XVF) est utilisé pour coupler les modèles de dimensionnalité homogènes mais de cinématique hétérogènes. Ici pas de recouvrement de domaine est présent. En outre, le XVF offre la possibilité d'adapter les conditions imposées à l'interface en utilisant un paramètre scalaire unique. On montre que, pour le problème de dimensionnalité homogène, que deux conditions différentes peuvent être imposées par ce paramètre. Un correspondant à des conditions fortes des Multi Point Constraints (MPC) et un second fournir des conditions faibles. La dernière offre la possibilité de réduire extrêmement le domaine qui utilise le modèle cinématique complexe, sans perte de précision locale. Comme il s'agit de la première application de la XVF vers les structures composites, le besoin d'un nouvel opérateur de couplage a été identifié. Un nouveau formulaire est proposé, testé et sa robustesse sera évaluée. / This work considers local stress concentrations, especially the free-Edge effects of multilayered structures. At the interface of two adjacent layers with different elastic properties, the stresses can become singular in the intermediate vicinity of the free edge. This is valid while assuming a linear elastic material behaviour. As a consequence this zones are an essential delamination trigger. Via the Carrera Unified Formulation (CUF), different kinematical models are testes in order to obtain the correct local stress concentration. In the first part of this work, the reduced dimensional modelling approaches are compared. Two main class are presented: Equivalent Single Layer (ESL) models treating the layered structure like one homogenous plate of equal mechanical proper- ties, and the Layer Wise approach, treating each layer independently. Subsequently their capabilities to capture the appearing singularities are compared. In order to have a comparable measurement of those singularities, the obtained stress distributions will be expressed via a power law function, which has a priori a singular behaviour. Only two parameters fully describe therefore the singular stress components in the vicinity of the free edge. With the help of these two parameters not only the different models capabilities will be compared, but also the free edge effect itself will be measured and compared for different symmetrical laminates and the case of extensional and uniform bending load. The results for all laminates under both load cases confirm the before stated need for rather complex models in the vicinity of the free edge. However far from the free edges, in the composite plates centre, no significant difference can be noted for rather simple models. The second part of this work is therefore dedicated to the coupling of kinematically incompatible models. The use of costly expensive complex models is restricted to local domains of interest, while economic simple models will model the global do- main. The Extended Variational Formulation (XVF) is identified as the most suitable way to couple the kinematically heterogenous but dimensional homogenous models. As it uses a configuration with one common interface without domain overlap, the additional efforts for establishing the coupling are limited. Further the XVF offers the possibility to adapt the conditions imposed at the interface using a single scalar parameter. It will be shown that for the homogenous dimensional problem under consideration only two different conditions can be imposed by this parameter. One matching the strong conditions imposed by the classical Multi Point Constrains (MPC) and a second one providing a weak condition. The last one is shown to provide the possibility to reduce further the domain using the complex kinematical model, without the loss of local precision. As this is the first application of the XVF towards composite structures, the need for a new coupling operator was identified. A new form is proposed, tested and its robustness will be evaluated.

Un des défis majeurs pour le développement des Systèmes Multi-Agents (SMA) auto-organisateurs est de garantir la convergence du système vers la fonction globale attendue par un observateur externe et de garantir que les agents sont capables de s'adapter face aux perturbations. Dans la littérature, plusieurs travaux se sont basés sur la simulation et le model-checking pour analyser les SMA auto-organisateurs. La simulation permet aux concepteurs d'expérimenter plusieurs paramètres et de créer certaines heuristiques pour faciliter la conception du système. Le model-checking fournit un support pour découvrir les blocages et les violations de propriétés. Cependant, pour faire face à la complexité de la conception des SMA auto-organisateurs, le concepteur a également besoin de techniques qui prennent en charge non seulement la vérification, mais aussi le processus de développement lui-même. En outre, ces techniques doivent permettre un développement méthodique et faciliter le raisonnement sur divers aspects du comportement du système à différents niveaux d'abstraction. Dans cette thèse, trois contributions essentielles ont été apportées dans le cadre du développement et la vérification formelle des SMA auto-organisateurs: une formalisation à l'aide du langage B-événementiel des concepts clés de ces systèmes en trois niveaux d'abstraction (micro, méso et macro), une expérimentation d'une stratégie de raffinement descendante pour le développement des SMA auto-organisateurs et la proposition d'un processus de raffinement ascendant basé sur des patrons de raffinement. / A major challenge for the development of self-organizing MAS is to guarantee the convergence of the system to the overall function expected by an external observer and to ensure that agents are able to adapt to changes. In the literature, several works were based on simulation and model-checking to study self-organizing MAS. The simulation allows designers to experiment various settings and create some heuristics to facilitate the system design. Model checking provides support to discover deadlocks and properties violations. However, to cope with the complexity of self-organizing MAS, the designer also needs techniques that support not only verification, but also the development process itself. Moreover, such techniques should support disciplined development and facilitate reasoning about various aspects of the system behavior at different levels of abstraction. In this thesis, three essential contributions were made in the field of formal development and verification of self-organizing MAS: a formalization with the Event-B language of self-organizing MAS key concepts into three levels of abstraction, an experimentation of a top-down refinement strategy for the development of self-organizing MAS and the definition of a bottom-up refinement process based on refinement patterns.

Les systèmes sur puces intègrent aujourd’hui sur le même substrat des parties analogiques et des unités de traitement numérique. Tandis que la complexité de ces systèmes s’accroissait, leur temps de mise sur le marché se réduisait. Une conception descendante globale et coordonnée du système est devenue indispensable de façon à tenir compte des interactions entre les parties analogiques et les partis numériques dès le début du développement. Dans le but de répondre à ce besoin, cette thèse expose un processus de raffinement progressif et méthodique des parties analogiques, comparable à ce qui existe pour le raffinement des parties numériques. L'attention a été plus particulièrement portée sur la définition des niveaux analogiques les plus abstraits et à la mise en correspondance des niveaux d’abstraction entre parties analogiques et numériques. La cohérence du raffinement analogique exige de détecter le niveau d’abstraction à partir duquel l’utilisation d’un modèle trop idéalisé conduit à des comportements irréalistes et par conséquent d’identifier l’étape du raffinement à partir de laquelle les limitations et les non linéarités aux conséquences les plus fortes sur le comportement doivent être introduites. Cette étape peut être d’un niveau d'abstraction élevé. Le choix du style de modélisation le mieux adapté à chaque niveau d'abstraction est crucial pour atteindre le meilleur compromis entre vitesse de simulation et précision. Les styles de modélisations possibles à chaque niveau ont été examinés de façon à évaluer leur impact sur la simulation. Les différents modèles de calcul de SystemC-AMS ont été catégorisés dans cet objectif. Les temps de simulation obtenus avec SystemC-AMS ont été comparés avec Matlab Simulink. L'interface entre les modèles issus de l'exploration d'architecture, encore assez abstraits, et les modèles plus fin requis pour l'implémentation, est une question qui reste entière. Une bibliothèque de composants électroniques complexes décrits en SystemC-AMS avec le modèle de calcul le plus précis (modélisation ELN) pourrait être une voie pour réussir une telle interface. Afin d’illustrer ce que pourrait être un élément d’une telle bibliothèque et ainsi démontrer la faisabilité du concept, un modèle d'amplificateur opérationnel a été élaboré de façon à être suffisamment détaillé pour prendre en compte la saturation de la tension de sortie et la vitesse de balayage finie, tout en gardant un niveau d'abstraction suffisamment élevé pour rester indépendant de toute hypothèse sur la structure interne de l'amplificateur ou la technologie à employer. / Systems on Chip (SoC) embed in the same chip analogue parts and digital processing units. While their complexity is ever increasing, their time to market is becoming shorter. A global and coordinated top-down design approach of the whole system is becoming crucial in order to take into account the interactions between the analogue and digital parts since the beginning of the development. This thesis presents a systematic and gradual refinement process for the analogue parts comparable to what exists for the digital parts. A special attention has been paid to the definition of the highest abstracted analogue levels and to the correspondence between the analogue and the digital abstraction levels. The analogue refinement consistency requires to detect the abstraction level where a too idealised model leads to unrealistic behaviours. Then the refinement step consist in introducing – for instance – the limitations and non-linearities that have a strong impact on the behaviour. Such a step can be done at a relatively high level of abstraction. Correctly choosing a modelling style, that suits well an abstraction level, is crucial to obtain the best trade-off between the simulation speed and the accuracy. The modelling styles at each abstraction level have been examined to understand their impact on the simulation. The SystemC-AMS models of computation have been classified for this purpose. The SystemC-AMS simulation times have been compared to that obtained with Matlab Simulink. The interface between models arisen from the architectural exploration – still rather abstracted – and the more detailed models that are required for the implementation, is still an open question. A library of complex electronic components described with the most accurate model of computation of SystemC-AMS (ELN modelling) could be a way to achieve such an interface. In order to show what should be an element of such a library, and thus prove the concept, a model of an operational amplifier has been elaborated. It is enough detailed to take into account the output voltage saturation and the finite slew rate of the amplifier. Nevertheless, it remains sufficiently abstracted to stay independent from any architectural or technological assumption.