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.

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.

Thesis (Ph. D.)--University of Sussex, 1990. / Includes bibliographical references (p. 265-271) and index.

Cette thèse a pour cadre scientifique la décomposition formelle des spécifications centrali- sées Event-B appliquée aux systèmes distribués BIP. Elle propose une démarche descendante de développement des systèmes distribués corrects par construction en combinant judicieu- sement Event-B et BIP. La démarche proposée comporte trois étapes : Fragmentation, Dis- tribution et Génération de code BIP. Les deux concepts clefs Fragmentation et Distribution, considérés comme deux sortes de raffinement automatique Event-B paramétrées à l'aide de deux DSL appropriés, sont introduits par cette thèse. Cette thèse apporte également une contribution au problème de la génération de code à partir d'un modèle Event-B issu de l'étape de distribution. Nous traitons aussi bien les aspects architecturaux que comportemen- taux. Un soin particulier a été accordé à l'outillage et l'expérimentation de cette démarche. Pour y parvenir, nous avons utilisé l'approche IDM pour l'outillage et l'application Hôtel à clés électroniques pour l'expérimentation. / The scientific framework of this thesis is the formal decomposition of the centralized specifications Event-B applied to distributed systems based on the BIP (Behavior, Interaction, Priority) component framework. It suggets a top-down approach to the development of correct by construction distributed systems by judiciously combining Event-B and BIP. The proposed approach consists in three steps : Fragmentation, Distribution and Generation of BIP code. We introduce two key concepts, Fragmentation and Distribution, which are considered as two kinds of automatic refinement of Event-B models. They are parameterized using two appropriate DSL. This thesis also contributes to the problem of code generation from Event- B models resulting from the Distribution step. Accordingly, we deal with both architectural and behavioral aspects. A special care has been devoted to the implementation and the experimentation of this approach. To achieve this, we have used the IDM approach for tooling and the Electronic Hotel Key System for experimentation.

Depuis le début du millénaire, la simulation numérique directe est apparue comme un outil précieux capable d'étudier l’atomisation d’une goutte isolée par un écoulement à grande vitesse. L’atomisation peut être divisée en deux phases distinctes : l'éclatement se produit d'abord sous la forme d'aplatissement de la goutte, formant également des filaments, puis il se poursuit via l'obtention d'une multitude de gouttes de tailles réduites ce qui complète le processus d’atomisation. Les principaux objectifs pour le présent travail étaient donc d’établir un modèle et une méthode numérique capables d’étudier au mieux ces phénomènes. L'atomisation d’une goutte isolée est présentée et est accompagnée d’une comparaison avec l’expérience qui confirme les capacités du modèle et de la méthode à simuler numériquement les différents processus physiques mis en jeu. Des informations essentielles quant aux mécanismes d’atomisation, non exploitables avec l’expérience, sont décrites et l’objectif d’obtenir des gouttes de tailles réduites est atteint. / Only at the beginning of the millennium, direct numerical simulation has emerged as a valuable tool capable of studying the atomization of an isolated droplet by a high-speed flow. The atomization can be divided into two distinct phases: the aerobreakup occurs first in the form of flattening of the droplet, also forming filaments, and then it continues via the obtaining of a multitude of reduced sizes droplets what completes the process of atomization. The main objectives of this work were therefore to establish a model and a numerical method able to study these phenomena as well as possible. The atomization of an isolated droplet is presented and is accompanied by a comparison with the experiment which confirms the capacities of the model and the method to numerically simulate the different physical processes involved. Essential information on atomization mechanisms, which cannot be exploited with experiments, is described and the objective of obtaining droplets of reduced sizes is achieved.

Dans cette thèse, nous présentons des approches formelles permettant de simplifier la modélisation et la preuve du calcul distribué. Un système distribué est défini par une collection d’entités de calcul autonomes,qui communiquent ensemble pour accomplir une tâche commune. Chaque entité exécute localement son calcul et ne peut interagir qu’avec ses voisins.Le développement et la preuve du calcul distribué est un défi qui nécessite l’utilisation de méthodes et outils avancés. Dans nos travaux de thèse,nous étudions quelques problèmes fondamentaux du distribués, en utilisant Event-B, et nous proposons des schémas de preuve basés sur une approche“correct-par-construction”. Nous considérons un système distribué défini par réseau fiable, de processus anonymes et avec un modèle de communication basé sur l’échange de messages. Dans certains cas, nous faisons abstraction du modèle de communications en utilisant le modèle des calculs locaux. Nous nous focalisons d’abord sur le problème de détection de terminaison du calcul distribué. Nous proposons un patron formel permettant de transformer des algorithmes “avec détection de terminaison locale” en des algorithmes“avec détection de terminaison globale”. Ensuite, nous explicitons les preuves de correction d’un algorithme d’énumération. Nous proposons un développement formel qui servirait de point de départ aux calculs qui nécessitent l’hypothèse d’identification unique des processus. Enfin, nous étudions le problème du snapshot et du calcul d’état global. Nous proposons une solution basée sur une composition d’algorithmes existants. / In this work, we propose formal approaches for modeling andproving distributed algorithms. Such computations are designed to run oninterconnected autonomous computing entities for achieving a common task :each entity executes asynchronously the same code and interacts locally withits immediate neighbors. Correctness of distributed algorithms is a difficulttask and requires advancing methods and tools. In this thesis, we focus onsome basic problems of distributed computing, and we propose Event-B solutionsbased on the ”correct-by-construction” approach. We consider reliablesystems. We also assume that the network is anonymous and processes communicatewith asynchronous messages. In some cases, we refer to local computationsmodel to provide an abstraction of the distributed computations.We propose a formal framework enhancing the termination detection propertyof distributed algorithms. By relying on refinement and composition,we show that an algorithm specified with “local termination detection”, canbe reused in order to compute the same algorithm with “global terminationdetection”. We then focus on the enumeration problem : we start with anabstract initial specification of the problem, and we enrich it gradually bya progressive and incremental refinement. The computed result constitutesbasic initial steps of others distributed algorithms which assume that processeshave unique identifiers. We therefore focus on snapshot problems, andwe propose to investigate how existing algorithms can be composed, withrefinement, in order to compute a global state in an anonymous network.

Les systèmes informatiques sont construits par composition de plusieurs sous-systèmes répartis. La manière dont communiquent ces entités, ou pairs, joue un rôle clé dans la bonne marche du système composé. L'étude détaillée de ces interactions est donc essentielle dans le cadre de la vérification et du développement formel de tels systèmes. Ces interactions se décomposent en deux catégories: la communication synchrone et la communication asynchrone. La communication synchrone admet une transmission instantanée de l'information, le message, entre deux entités. La communication asynchrone, en revanche, prend en compte le découplage de la transmission du message en une opération d'envoi puis de réception avec la possibilité que des événements s'intercalent entre les deux donnant ainsi lieu à des variations de comportement, désirables ou non, des systèmes. Souvent considérée comme une entité monolithique duale du monde synchrone, le monde asynchrone se décline en réalité en de multiples modèles qui peuvent induire sur la communication une grande variété de propriétés qu'il convient de caractériser et comparer. Cette thèse se focalise sur les modèles de communication qui orchestrent l'ordre de délivrance des messages : par exemple les modèles dits FIFO qui assurent que certains messages sont reçus dans l'ordre dans lequel ils ont été émis. Nous considérons des modèles de communication classiques de la littérature ainsi que des variations de ces modèles dont nous explicitons les différences parfois négligées. Dans un premier temps nous proposons une formalisation logique abstraite et homogène des modèles de communication considérés et nous les hiérarchisons en étendant des résultats existants. Nous proposons dans un second temps une approche opérationnelle sous forme d'un outil de vérification de compositions de pairs que nous mécanisons à l'aide du langage de spécification TLA+ et du vérificateur de modèles TLC. Cet outil permet de spécifier des pairs communicants et des propriétés temporelles à vérifier pour les différents modèles de communication de façon modulaire. Pour cela, nous apportons un ensemble de spécifications uniformes et opérationnelles des modèles de communication basé sur la notion d'histoires de messages. Nous identifions et prouvons les conditions de leur conformité aux définitions logiques et validons ainsi la pertinence de notre outil. Dans un troisième temps nous considérons des spécifications concrètes de nos modèles de communication, semblables à nombre de celles présentes dans la littérature. Nous disposons donc d'une hiérarchisation des modèles selon les propriétés d'ordre qu'ils garantissent mais également d'une autre hiérarchisation pour un modèle donné entre sa définition logique abstraite et ses implantations concrètes. Ces deux dimensions correspondent à deux dimensions du raffinement. Nous introduisons graduellement par raffinement la notion de communication asynchrone point à point et prouvons, grâce à la méthode Event-B, tous les liens de raffinement entre les différents modèles de communication et leurs déclinaisons. Nous offrons ainsi une cartographie détaillée des modèles pouvant être utilisée pour en développer de nouveaux ou identifier les modèles les plus adaptés à des besoins donnés. Enfin, nous proposons des pistes d'extension de nos travaux à la communication par diffusion où un message peut être envoyé simultanément à plusieurs destinataires. En particulier, nous montrons les différences induites dans la hiérarchie des modèles et les adaptations à effectuer sur notre outil de vérification pour prendre en compte ce mode de communication / Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. An in-depth study of these interactions makes sense in the context of the formal development and verification of such systems. The interactions fall in two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. Asynchronous communication, on the other hand, splits the transmission in a send operation and a receive operation. This make the interleaving of other events possible and lead to new behaviours that may or may not be desirable. The asynchronous world is often viewed as a monolithic counterpart of the synchronous world. It actually comes in multiple models that provide a wide range of properties that can be studied and compared. This thesis focuses on communication models that order the delivery of messages: for instance, the "FIFO" models ensure that some messages are received in the order of their emission. We consider classic communication models from the literature as well as a few variations. We highlight the differences that are sometimes overlooked. First, we propose an abstract, logical, and homogeneous formalisation of the communication models and we establish a hierarchy that extends existing results. Second, we provide an operational approach with a tool that verifies the compatibility of compositions of peers. We mechanise this tool with the TLA+ specification language and its model checker TLC. The tool is designed in a modular fashion: the commmunicating peers, the temporal compatibility properties, and the communication models are specified independently. We rely on a set of uniform operational specifications of the communication models that are based on the concept of message history. We identify and prove the conditions under which they conform to the logical definitions and thus show the tool is trustworthy. Third, we consider concrete specifications of the communication models that are often found in the literature. Thus, the models are classified in terms of ordering properties and according to the level of abstraction of the different specifications. The concept of refinement covers these two aspects. Thus, we model asynchronous point-to-point communication along several levels of refinement and then, with the Event-B method, we establish and prove all the refinements between the communication models and the alternative specifications of each given model. This work results in a detailed map one can use to develop a new model or find the one that best fits given needs. Eventually we explore ways to extend our work to multicast communication that consists in sending messages to several recipients at once. In particular, we highlight the differences in the hierarchy of the models and how we modify our verification tool to handle this communication paradigm.

Pour la conception des cœurs de réacteurs de 4ème génération, une précision accrue est requise pour les calculs des différents paramètres neutroniques. Les ressources mémoire et le temps de calcul étant limités, une solution consiste à utiliser des méthodes de raffinement de maillage afin de résoudre l'équation de transport des neutrons. Le flux neutronique, solution de cette équation, dépend de l'énergie, l'angle et l'espace. Les différentes variables sont discrétisées de manière successive. L'énergie avec une approche multigroupe, considérant les différentes grandeurs constantes sur chaque groupe, l'angle par une méthode de collocation, dite approximation Sn. Après discrétisation énergétique et angulaire, un système d'équations hyperboliques couplées ne dépendant plus que de la variable d'espace doit être résolu. Des éléments finis discontinus sont alors utilisés afin de permettre la mise en place de méthodes de raffinement dite hp. La précision de la solution peut alors être améliorée via un raffinement en espace (h-raffinement), consistant à subdiviser une cellule en sous-cellules, ou en ordre (p-raffinement) en augmentant l'ordre de la base de polynômes utilisée.Dans cette thèse, les propriétés de ces méthodes sont analysées et montrent l'importance de la régularité de la solution dans le choix du type de raffinement. Ainsi deux estimateurs d'erreurs permettant de mener le raffinement ont été utilisés. Le premier, suppose des hypothèses de régularité très fortes (solution analytique) alors que le second utilise seulement le fait que la solution est à variations bornées. La comparaison de ces deux estimateurs est faite sur des benchmarks dont on connaît la solution exacte grâce à des méthodes de solutions manufacturées. On peut ainsi analyser le comportement des estimateurs au regard de la régularité de la solution. Grâce à cette étude, une stratégie de raffinement hp utilisant ces deux estimateurs est proposée et comparée à d'autres méthodes rencontrées dans la littérature. L'ensemble des comparaisons est réalisé tant sur des cas simplifiés où l'on connaît la solution exacte que sur des cas réalistes issus de la physique des réacteurs.Ces méthodes adaptatives permettent de réduire considérablement l'empreinte mémoire et le temps de calcul. Afin d'essayer d'améliorer encore ces deux aspects, on propose d'utiliser des maillages différents par groupe d'énergie. En effet, l'allure spatiale du flux étant très dépendante du domaine énergétique, il n'y a a priori aucune raison d'utiliser la même décomposition spatiale. Une telle approche nous oblige à modifier les estimateurs initiaux afin de prendre en compte le couplage entre les différentes énergies. L'étude de ce couplage est réalisé de manière théorique et des solutions numériques sont proposées puis testées. / The different neutronic parameters have to be calculated with a higher accuracy in order to design the 4th generation reactor cores. As memory storage and computation time are limited, adaptive methods are a solution to solve the neutron transport equation. The neutronic flux, solution of this equation, depends on the energy, angle and space. The different variables are successively discretized. The energy with a multigroup approach, considering the different quantities to be constant on each group, the angle by a collocation method called Sn approximation. Once the energy and angle variable are discretized, a system of spatially-dependent hyperbolic equations has to be solved. Discontinuous finite elements are used to make possible the development of $hp-$refinement methods. Thus, the accuracy of the solution can be improved by spatial refinement (h-refinement), consisting into subdividing a cell into subcells, or by order refinement (p-refinement), by increasing the order of the polynomial basis.In this thesis, the properties of this methods are analyzed showing the importance of the regularity of the solution to choose the type of refinement. Thus, two error estimators are used to lead the refinement process. Whereas the first one requires high regularity hypothesis (analytical solution), the second one supposes only the minimal hypothesis required for the solution to exist. The comparison of both estimators is done on benchmarks where the analytic solution is known by the method of manufactured solutions. Thus, the behaviour of the solution as a regard of the regularity can be studied. It leads to a hp-refinement method using the two estimators. Then, a comparison is done with other existing methods on simplified but also realistic benchmarks coming from nuclear cores.These adaptive methods considerably reduces the computational cost and memory footprint. To further improve these two points, an approach with energy-dependent meshes is proposed. Actually, as the flux behaviour is very different depending on the energy, there is no reason to use the same spatial discretization. Such an approach implies to modify the initial estimators in order to take into account the coupling between groups. This study is done from a theoretical as well as from a numerical point of view.

L’analyse isogéométrique pour la résolution de problèmes de la mécanique du solide suscite de vifs intérêts depuis une dizaine d’année. En effet, cette méthode de discrétisation autorise la description exacte des géométries étudiées permettant ainsi de supprimer les erreurs dues à une mauvaise description du domaine spatial étudié. Cependant elle pose un problème théorique de propagation de raffinement lors de la localisation de maillage. Des méthodes pour contourner ce problème ont été proposée dans la littérature mais complexifient grandement la mise en œuvre de cette stratégie de résolution. Cette thèse propose une stratégie de raffinement localisé adaptatif en espace pour les problèmes de statique et en espace temps pour les problèmes de dynamique transitoire dans le cadre de l’analyse isogéométrique. Pour cela une méthode de localisation pour l’analyse isogéométrique en statique basée sur une résolution multigrille est tout d’abord développée pour des problèmes en deux dimensions. Elle présente l’avantage de contourner la problématique de propagation de raffinement de maillage due à l’analyse isogéométrique tout en étant plus simple à mettre en œuvre que les méthodes déjà existantes. De plus, l’utilisation de l’analyse isogéométrique permet de simplifier les procédures de raffinement lors de l’adaptation de maillage qui peuvent être complexes lors de l’utilisationd’éléments finis classiques. Une méthode de raffinement adaptatif espace temps basée sur une résolution multigrille est ensuite développée pour des problèmes en une dimension. Une étude sur la structure des opérateurs est proposée afin de choisir un intégrateur temporel adapté. Les performances de cette stratégies sont mises en évidence, puis une modification de la méthode de résolution est proposée afin de diminuer significativement les coûts de calculs associées à cette résolution. La méthode de raffinement adaptatif espace temps est appliquée à quelques exemples académiques afin de valider son bon comportement lors de la localisation. / Isogeometric analysis applied to structural mechanics problems is a topic of intense concerns for a decade. Indeed, an exact description of geometries studied is allowed by this discretization method suppressing errors due to a bad description of the spatial domain considered. However, a theoretical problem of refinement propagation appears during mesh localization. Local refinement methods for isogeometric analysis has been developed and implied a complexification of the implementation of such a resolution strategy. This PhD thesis expose a space adaptative refinement strategy for linear elastic problems and a space-time one for transient dynamic using isogeometric analysis. For this purpose, a localization method for isogeometric analysis based on a multigrid resolution is developed for 2D linear elastic problems. This method allow to circumvent mesh refinement propagation inherent to isogeometric analysis, and is easier to implement than existing methods. Moreover, the use of isogeometric analysis simplifies refinement procedures occuring during mesh adaptation and which can be really complex using classical finite element analysis. Then, a space-time adaptative refinement based on a multigrid resolution is developed for one dimensional in space problems. A study on operators structure is exposed in order to choose a well suited time integrator. This strategy's performances are highlighted, then an evolution of this method is set up in order to lower computational costs. The space-time adaptaptive refinement is applied to some academical examples to show it good behavior during localization.

Les procédés d’hyper-déformations (SPD) peuvent imposer de très grandes déformations à un métal et en transformer les propriétés métallurgiques de la matière en introduisant une forte densité de dislocations et un important affinement de la microstructure. Dans ce travail de thèse présenté, des expériences en torsion à haute pression (HPT) ont été réalisées pour la consolidation des différentes poudres de fer de taille à l’échelle nano et micrométrique. Ces expériences ont été effectuées avec succès à la température ambiante aboutissant à la fois à un faible niveau de porosité résiduelle et l'affinement significatif de la taille de grain, grâce à une importante déformation en cisaillement et à de la pression hydrostatique appliquée au procédé HPT. La compression a été faite en deux étapes: d'abord une compression axiale, puis déformation en cisaillement en tournant la partie inférieure de la filière HPT tout en maintenant constante la force axiale. L'homogénéité de la déformation en cisaillement à travers l'épaisseur du disque a été examinée par une mesure de déformation locale, qui montre une distribution du gradient. L'analyse par diffraction à rayons X a été réalisée sur des échantillons consolidés qui ont révélé une proportion peu importante d’oxydes. L'effet de la déformation en cisaillement sur la microstructure et la texture a été étudié par microscopie électronique à balayage et EBSD. La micro-dureté et la porosité moyenne des échantillons en fonction de la déformation en cisaillement, à pression hydrostatique constante, ont également été mesurées. Une trame de modélisation mise en œuvre dans le modèle de Taylor a été développée pour simuler l'effet du glissement aux joints de grains pour l'évolution de la texture cristallographique. Le principal effet constaté est un décalage des orientations idéales dans les conditions de cisaillement simple, ce qui a été vérifié expérimentalement. Le procédé de consolidation par HPT a été simulé numériquement en utilisant la méthode des éléments finis pour un modèle de plasticité des poudres. La simulation de ce dernier a permis de confirmer la porosité résiduelle moyenne observée expérimentalement et les différents gradients de la déformation plastique. La distribution de la densité locale a également été modélisée / Severe plastic deformation (SPD) processes can impose extremely large strains to a metal and transforming the metallurgical state of the material by introducing high dislocation density and high level of microstructure refinement. In the present thesis work High Pressure Torsion (HPT) experiments were performed for consolidation of different powders including Nano- and Micro- scaled iron powders. The experiments were carried out successfully at room temperature, achieving both low level of residual porosity and significant grain refinement, thanks to the intense shear strain and hydrostatic pressure applied in HPT. The compaction was done in two steps: first axial compaction, then shear deformation by rotating the bottom part of the HPT die while maintaining the axial force constant. The homogeneity of shear strain across the thickness of the disk was examined by local strain measurement, showing a gradient distribution. X-ray diffraction analysis was carried out on the consolidated samples which revealed no significant proportion of oxides. The effect of shear deformation on the microstructure and texture was investigated by metallographic scanning electron microscopy and electron backscattered diffraction (EBSD). The micro-hardness and average porosity of the samples as a function of shear strain at constant hydrostatic pressure were also measured. A modeling frame implemented into the Taylor model was developed to simulate the effect of Grain Boundary Sliding (GBS) on the evolution of crystallographic texture. The main effect found is a shift of the ideal orientations under simple shear conditions, which was verified experimentally. The consolidation process by HPT was simulated numerically using the finite element method together with a powder plasticity model. The simulation of the consolidation process permitted to confirm the experimentally observed average residual porosity and the different gradients in the plastic strain. The local density distribution was also modeled