Résumé: Les propriétés que l'on souhaite exprimer sur les applications système d'information ne peuvent se restreindre aux propriétés statiques, dites propriétés d'invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l'état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l'efficacité pour le domaine des systèmes d'information est plutôt réduite à cause de l'explosion combinatoire de l'espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d'autant plus que ces dernières ne sont pas outillées. Pour pallier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d'atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d'obligations de preuve permettant de les prouver. Une propriété d'atteignabilité permet d'exprimer qu'il existe au moins une exécution du système qui permet d'atteindre un état cible à partir d'un état initial donné. Par contre, la propriété de précédence permet de s'assurer qu'un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l'utilisateur de la tâche de génération d'obligations de preuve qui peut être longue et fastidieuse.||Abstract: The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties , that depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks.

In the automotive, railway and aerospace industries, interior noise is an important consideration in design and operation. Among the available technologies to reduce the structure-borne vibration and noise, the use of Metal-Polymer Sandwich (MPS) panels is attracting more interest from Original Equipment Manufacturers (OEMs). As for constrained-layer damping (CLD) treatments, besides developing more accurate models (theoretical and finite element) to simulate the vibroacoustic performance, it is very important to 'accurately identify the properties of the constituent materials of an MPS. Since the core materials in MPS exhibit viscoelastic properties which vary significantly with temperature and frequency, it is necessary to develop experimental and/or optimization methods to characterize the dynamic properties so that they may be well matched to specific noise and vibration control applications. This is the objective of this thesis.In this thesis, a simple free-free beam based setup, together with an identification algorithm has been developed to identify the dynamic properties of core materials from the measured frequency response functions. The setup involved circumventing some drawbacks of the traditional clamped-free setup.In particular, a new optimization method is brought' forward wherein a four-parameter fractional derivative model plus a three-parameter Williams-Landel-Ferry (WLF) equation are used to describe the temperature and frequency dependent behaviour of core materials. Therefore, few parameters are optimized for the temperature and frequency dependent properties. The objective function in the optimization is based on the so-called amplitude correlation coefficient which can be calculated directly by the frequency response functions. The normal mode superposition method taking the added mass into account, as well as Ross-Kerwin-Ungar (RKU) equations, as a solver, is used to calculate the predicted frequency response functions. The Pattern Search algorithm is used to find the best values of design parameters. This algorithm is a global optimization algorithm and is less sensitive to the initial values of design parameters. Numerical examples and tests on several MPS panels were used to validate the free-free setup and optimization method by systematic comparison with the ASTM E756-04 Standard and with DMA when the latter is possible. However, with some MPS panels, the proposed method failed to provide satisfactory results. It was further postulated that the manufacturing process of these MPS panels may somehow have modified the properties or the constitutive law of the polymer itself.

Les propriétés que l’on souhaite exprimer sur les applications système d’information ne peuvent se restreindre aux propriétés statiques, dites propriétés d’invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l’état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l’efficacité pour le domaine des systèmes d’information est plutôt réduite à cause de l’explosion combinatoire de l’espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d’autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d’atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d’obligations de preuve permettant de les prouver. Une propriété d’atteignabilité permet d’exprimer qu’il existe au moins une exécution du système qui permet d’atteindre un état cible à partir d’un état initial donné. Par contre, la propriété de précédence permet de s’assurer qu’un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l’utilisateur de la tâche de génération d’obligations de preuve qui peut être longue et fastidieuse / The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties, which depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks

Le diagramme des phases stables et métastables de l'eau reste une énigme depuis des décennies. De nombreuses interprétations ont été proposées pour expliquer les divergences apparentes de certaines propriétés thermodynamiques et de transport, de l'eau surfondue. Mais une description unifiée manque encore, essentiellement parce que la température où apparaissent diverger ces propriétés est située en dessous de la température limite de cristallisation, dans une région, qualifiée de no-man's land, entre l'eau surfondue et la glace amorphe. Nous avons, pour la première fois, mesuré les propriétés dynamiques de l'eau liquide et surfondue par diffusion inélastique du rayonnement synchrotron ultraviolet et par diffusion de lumière visible. En analysant les spectres obtenus à l'aide d'un formalisme de fonction mémoire, nous avons trouvé un bon accord avec les simulations de dynamique moléculaire et avec la théorie du couplage de modes, qui attribue une origine dynamique aux singularités observées dans le no-man's land de l'eau. Nous avons aussi mesuré la dynamique de la solution LiCl-6H2O par diffusion inélastique de la lumière visible et du rayonnement synchrotron dans la gamme des ultraviolets et des rayons X. Cette investigation est un premier pas dans le no man's land de l'eau par parce que la dilution progressive de solutions aqueuses constitue une méthode indirecte pour obtenir des informations sur l'eau pure en dessous de la température de nucléation homogène des cristaux. Nous avons observé au cours du refroidissement de la solution, une relaxation, qui possède des caractéristiques similaires à celles de la relaxation structurale de l'eau pure, mais qui se divise en une relaxation structurale et une relaxation secondaire, autour de la température où les propriétés de l'eau pure semblent diverger. Selon des expériences et des théories récentes et sur la dynamique et le diagramme de phase de l'eau et des solutions ioniques diluées à basse température et à pression élevée, laséparation des dynamiques que nous observons pourrait éventuellement être reliée au début d'une hypothétique transition de phase liquide-liquide qui apparaît à des pressions beaucoup plus élevées que celles étudiées. D'autres investigations en fonction de la pression, et à des concentrations en sel plus faibles, sont souhaitables pour clarifier ces coïncidences fascinantes.

Les propriétés que l'on souhaite exprimer sur les applications système d'information ne peuvent se restreindre aux propriétés statiques, dites propriétés d'invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l'état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l'efficacité pour le domaine des systèmes d'information est plutôt réduite à cause de l'explosion combinatoire de l'espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d'autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d'atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d'obligations de preuve permettant de les prouver. Une propriété d'atteignabilité permet d'exprimer qu'il existe au moins une exécution du système qui permet d'atteindre un état cible à partir d'un état initial donné. Par contre, la propriété de précédence permet de s'assurer qu'un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l'utilisateur de la tâche de génération d'obligations de preuve qui peut être longue et fastidieuse

Les polysaccharides sont l'une des principales options à retenir pour progresser dans l'utilisation ou la conception de polymères renouvelables. Depuis les années cinquante, le développement industriel de ce type de polymères s'était considérablement réduit du fait de l'avènement des polymères synthétiques. Cependant, cet intérêt a cru considérablement ces dernières années en raison de la sensibilisation du public sur la limite des ressources fossiles. Ces biopolymères sont donc devenus un sujet d'importance, tant sur le plan industriel que sur celui de la recherche fondamentale. Toutefois, les systèmes à base de polysaccharides sont le plus souvent transformés via l'utilisation d'importantes quantités de solvants (y compris l'eau), ce qui globalement pénalise le procédé associé en l'affligeant d'une charge environnementale supplémentaire. Par la voie ‘fondue', le développement de polymères thermoplastiques à base de dérivés de la cellulose est un véritable défi, qui concerne autant le mode de transformation de ces systèmes que le niveau des propriétés du matériau final. Pour exemple, la température de dégradation de l'acétate de cellulose (CA) (dont le degré de substitution 2,5 est développé par le Groupe Solvay) est si proche de sa température de fusion que son procédé de mise en oeuvre ne peut être envisagé qu'avec l'ajout d'une quantité importante de plastifiants externes (entre 20 et 30 en poids selon le type d'additif). Le comportement d'un mélange CA-plastifiant est principalement régi par un «réseau» de très fortes interactions polaires, dont la force et la densité dépendent de 3 paramètres spécifiques: le degré de substitution de CA, la typologie de plastifiant et la quantité de plastifiant. Pour expliquer les différents mécanismes de plastification, il est donc important pour nous d'étudier et de comprendre les propriétés dynamiques (en ce qui concerne les phénomènes de relaxation) de ce type de systèmes et comment les trois leviers que nous avons identifiés peuvent influencer ou moduler les différentes interactions échangées dans les mélanges / Polysaccharides are one of the main options to the on-going move towards the use of renewable polymers. The industrial interest in this type of polymers drastically shrunk by the advent of synthetic polymers in the fifties, but is currently reviving due to the public awareness on the limit of fossil resources. These biopolymers are nowadays offering a challenging and industrially profitable playground for researchers. However, current polysaccharides based materials are mostly processed with extensive use of solvents (including water) making the total process an environmental burden despite the advantage of the starting material. Development of thermoplastic cellulose-based materials is very challenging regarding both final material properties and polymer processing. The degradation temperature of Cellulose Acetate (CA) (degree of substitution 2.5) is so close to its melting temperature that it can only be processed with a significant amount of external plasticizers (between 20 et 30 wt.% depending on the type of the additive). Behavior of a CA-plasticizer blend is mainly governed by a ‘network’ of high polar interactions, the strength and the density of which clearly depend of 3 specific parameters: the CA’s degree of substitution, the typology of the plasticizer, the amount of plasticizer. In an attempt to explain the different plasticization mechanisms, it is thus of utmost importance for us to study and understand the dynamic properties (regarding the relaxation phenomena) of this kind of systems and how the three levers that we identified can influence or modulate the different interactions exchanged within the blends

L'objectif de ce travail est d'apporter un éclairage nouveau à la compréhension des mécanismes physico-chimiques qui contrôlent la croissance des trois oxydes d'Aluminium, de Zirconium, de Hafnium. Ces matériaux sont considérés comme les meilleurs candidats pour remplacer la silice en tant qu'oxyde de grille dans le futur composant MOS. La précision et la fiabilité de la méthode DFT associé à la fonctionnelle B3LYP, ont été testées à l'aide des résultats expérimentaux et des méthodes ab initio les plus précis telles que CCSD(T) et CISD(T), en utilisant différents ensembles des fonctions de bases. Nos résultats montrent que et la méthode hybride DFT peut prédire de façon précise les propriétés statistiques et dynamiques de la famille d'organométalliques (AlxCyHzOt) et des systèmes moléculaires à base de métaux de transition (Zr/HfxClyOzHt). Les premières études systématiques des surfaces d'énergie potentielle de TMA ont été présentes et les caractéristiques des rotors constitués des groups méthyles ont été rapportées avec une grande précision. Les mécanismes réactionnels, à plusieurs étapes, entre les molécules précurseurs de trois oxydes et les molécules d'eau résiduelle phase gazeuse ont été étudies en détail. Les mouvements internes fortement anharmoniques, des espèces moléculaires présentes touts au long du processus d'hydrolyse ont été déterminés. Les effets qualitatifs sur les cinétiques des réactions ont été discutés. La forte exothermicité de la réaction TMA/H2O a été démontrée, alors que la réaction avec les tétrachlorures de Zirconium et Hafnium ont montré un caractère plutôt endothermique. Nous avons aussi étudié les mécanismes réactionnels de la vapeur d'eau avec d'espèces moléculaires chimisorbés en surface. Les réactions interviennent dans les cycles initiales d'ALD sur en substrat de Si(001)-2x1 légèrement oxydé. Les mécanismes que nous proposons sont qualitativement proches des mécanismes d'hydrolyse discutés dans la phase gaz euse : confirmation de la forte réactivité exothermique avec les hydroxyméthyliques d'Aluminium, endothermicité des réactions avec hydroxychlorures de Zirconium et Hafnium. Les composés avec le Zirconium et le Hafnium ont des comportements similaires. Enfin, les effets de coopérativité, à la fois au niveau des molécules de vapeur d'eau, qu'au niveau des complexes en surface, sur les réactions ont été mis en évidence et discutés. Ils montrent des comportements tout à fait intéressants dans le cas des hydroxychlorures des Zirconium et Hafnium. Par contre, ces effets sont de moindre importance dans les cas de l'oxyde d'aluminium, qui est actuellement considéré comme le matériau le plus compatible avec la croissance par ALD